OTTER 3.3 Reference Manual

Preprint English OPEN
McCune, William;
(2003)
  • Subject: Computer Science - Mathematical Software | Computer Science - Symbolic Computation | F.4.1
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES

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-o... View more
Share - Bookmark