Sutcliffe, G; Melville, S
(South African Computer Society (SAICSIT), 1996)
In the process of resolution based Automatic Theorem Proving, problems expressed in First Order Form (FOF) are transformed by a clausifier to Clause Normal Form (CNF). This research examines and compares clausifiers. ...