From: Ed Catmur <e.j.catmur@sms.ed.ac.uk>
Date: 8 February 2006 23:39:07 GMT
To: michael.fourman@ed.ac.uk
Subject: CNF conversion

The attached files are my solution to the CNF conversion assignment.

prop.sml defines the structures used.
cnf_test.sml implements naive CNF conversion.
cnf_label.sml implements labelling CNF conversion.
cnf_imp.sml implements improved CNF conversion.
eval.sml contains functions for testing: formula evaluation by
substituting and swallowing truth values; equivalence testing by
checking that satisfying assignments on one side extend to satisfying
assignments on the other side; and formula deserialisation from large
integers.