otter stable port information

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
UseMaxBuildJobs: false
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.
<<