Package otter-3.3f-1

This package contains OTTER, MACE, and ANLDP, three programs developed at Argonne National Labs for first-order theorem proving and model generation. 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. MACE 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. MACE is a useful complement to the theorem prover OTTER, with OTTER searching for proofs and MACE looking for countermodels. ANLDP is a model generation program based on the Davis-Putnam method for solving the propositional satisfiability problem.