Otter 3.3/Mace 2.2

Otter is a resolution-style theorem-proving program for first-order logic with equality. Otter includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy. Mace2 is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland- Logeman procedure decides the propositional problem, and any models found are translated to first-order models. Mace2 is a useful complement to the theorem prover Otter, with Otter searching for proofs and Mace2 looking for countermodels. Otter and Mace2 are coded in ANSI C, are free, and are portable to many different kinds of computer.

Click here to get the file