Package: otter Version: 3.3f Description: Tools for first-order models and theorems Revision: 1 Maintainer: Jesse Alama Homepage: http://www-unix.mcs.anl.gov/AR/otter/ Source: http://www-unix.mcs.anl.gov/AR/otter/dist33/%n-%v.tar.gz Source-MD5: 795711b307cc1316e08d3d4f46c998c9 DocFiles: README.first README README.Ivy Legal documents/otter33.pdf documents/mace2.pdf documents/anldp.pdf License: Public Domain CompileScript: << make all << InstallScript: << mkdir -p %i/bin install -m 755 bin/otter %i/bin install -m 755 bin/mace2 %i/bin install -m 755 bin/anldp %i/bin << DescDetail: << 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. <<