@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@F Name: Otter 3.0 Keywords: first-order, batch-mode/automated, resolution/paramodulation Description: Semantics: first-order logic with equality Deductive machinery: binary resolution, hyperresolution, UR-resolution, paramodulation Dynamics: ?? Persistence: ?? Upon input first-order formulas are translated to clausal form. Clauses are stored in three sets: axioms, set-of-support, and demodulators. Options are provided for choosing inferences rules, restricting application of rules, handling equality, controlling search. Contact persons: William McCune mccune@mcs.anl.gov User group: ?? Pragmatics: good for Horn clause theories, has difficulty with iff definitions Documentation: "Otter 3.0 Reference Manual and Guide", by W. McCune, Report ANl-94/6, Argonne National Laboratory (1994). Applications: Abstract algebra. Resource requirements: Implemented in C, highly portable Where-to-get-it: See ftp://info.mcs.anl.gov/pub/Otter/README http://www.mcs.anl.gov/home/mccune/ar/otter/ W. McCune MCS-221 Argonne National Laboratory Argonne, IL 60439-4844 otter@mcs.anl.gov Sources: From: mccune@antares.mcs.anl.gov (William McCune) 95 july