Makalah ini mempresentasikan hasil penelitian tentang pembuatan aplikasi yang dapat melakukan konversi formula proposisi ke formula lain yang ekuivalen secara logis. Konversi dilakukan dengan menggunakan hukum-hukum ekuivalensi dan dilakukan secara bertahap. Setiap tahap, aplikasi akan menentukan hukum-hukum yang bisa diterapkan pada formula yang diperoleh pada tahapan ini serta subformula yang akan dikenai hukum tersebut. Selain itu, aplikasi ini juga dapat mengecek apakah sebuah formula sudah dalam bentuk CNF. Dalam implementasinya, aplikasi ini menggunakan tipe data abstrak pohon biner untuk merepresentasikan sebuah formula proposisi.