Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement (the conjecture) is a theorem of a set of statements (the axioms). Automated Model Finding (AMF) deals with the development of computer programs that show that some set of statements (e.g., a set of axioms) is satisfiable. In ATP theoremhood may be (typically is, in contemporary ATP systems) established by "proof by contradiction", in which the set consisting of the axioms and the negation of the conjecture is shown to be unsatisfiable. Proof by contradiction is meaningful only if the axioms are satisfiable - if the axioms are unsatisfiable then everything is a theorem of the axioms (the conjecture is not a relevant theorem of the axioms). When formulating a problem for ATP it may not be known that the axioms are satisfiable, and it is appropriate to check the axioms for satisfiability before continuing on to attempt a proof by contradiction.
Ratify is a meta-ATP system that takes an ATP or AMF problem and attempts to establish the status of the axioms (if any, in an ATP problem) and the relationship to the conjecture (in an ATP problem). The result status of Ratify is one of:
The decision tree of Ratify is as shown in this figure:
For establishing the counter satisfiability of the axioms and conjecture, and for establishing the satisfibility of the axioms, Ratify uses MACE 2.0 and SPASS 2.1. For establishing that the conjecture is a theorem of the axioms, and for establishing the unsatisfiability of the axioms, Ratify uses SSCPA. Ratify calls these systems via the SystemOnTPTP interface.