H ? « ‹ ← → › »

Language peer sets for Otter:
United States↑
United States/1988↑
Designed 1988 ↑
1980s languages ↑
Fifth generation↑
Late Cold War↑

Otter (3666/ott002)

 Otter logo
alternate simple view
Country: United States
Designed 1988

for Organized Techniques for Theorem-proving and Effective Research

Resolution-based theorem prover

W. McCune Argonne National Laboratory


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 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, and Knuth-Bendix completion.

Places
Related languages
AURA → Otter   Based on
References:
  • Quaife, A. (1989) Quaife, A. "Automated development of Tarski?s geometry". J. Automated Reasoning, 5(1):97?118, 1989
  • Quaife, A. (1990) Quaife, A. "Automated Development of Fundamental Mathematical Theories". PhD thesis, University of California at Berkeley, 1990.
  • Quaife, Art (1992) Quaife, Art "Automated Development of Fundamental Mathematical Theories" Kluwer Acadamic Publishers 1992
  • McCune, W. and Padmanabhan, R. (1996) McCune, W. and Padmanabhan, R. "Automated Deduction in Equational Logic and Cubic Curves" Springer-Verlag LNCS #1095 1996 Abstract oNLINE PAGE
  • Wos, Larry (1996) Wos, Larry "The Automation of Reasoning: An Experimenter's Notebook with Otter Tutorial" Academic Press (1996). Abstract
  • Wiedijk, Freek (1998) Wiedijk, Freek "The Fifteen Provers of the World" Abstract
  • Larry Wos, with Gail Pieper, (2000) Larry Wos, with Gail Pieper, "A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning", World Scientific 2000 Abstract Online copy
  • Kalman, J. A. (2001) Kalman, J. A. "Automated Reasoning with Otter", Rinton Press (2001) Abstract Publisher page
  • McCune, William (2003) McCune, William "Otter 3.3 manual" Mathematics and Computer Science Division Technical Memorandum No. 263 Argonne National Laboratory Abstract Online copy
    Resources
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder