The Practice of Clausification in Automatic Theorem Proving Page 1

problems expressed in First Order Form (FOF) are transformed by a clausifier to Clause Normal Form (CNF). This research examines and compares clausifiers. The boundaries between clausification, simplification, and solution search are delineated, and common clausification and simplification operations are documented. Four known clausifiers are evaluated, thus providing insight into their relative performance, and also providing baseline data for future evaluation of clausifiers. Automatic Theorem Proving (ATP) is the study and development of computer programs that build proofs of theorems. These programs are called ATP systems. The inputs to an ATP system are axioms, hypotheses, and the theorem statement, and the output is a proof object that shows that the theorem statement is a logical consequence of the axioms and hypotheses. See any of [9, 2, 28] for an introduction to the topic