OTTER
Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter’s inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP. Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. We recommend using Otter/Mace2’s successor Prover9/Mace4 instead.
Keywords for this software
References in zbMATH (referenced in 201 articles , 1 standard article )
Showing results 1 to 20 of 201.
Sorted by year (- Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
- Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
- Furbach, Ulrich; Pelzer, Björn; Schon, Claudia: Automated reasoning in the wild (2015)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Stojanović {\Dj}urđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
- Beeson, Michael; Wos, Larry: OTTER proofs in Tarskian geometry (2014)
- Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014)
- Grandi, Umberto; Endriss, Ulle: First-order logic formalisation of impossibility theorems in preference aggregation (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo: On deciding satisfiability by theorem proving with speculative inferences (2011)
- Kinyon, Michael: Ken Kunen: algebraist. (2011)
- Akbarpour, Behzad; Paulson, Lawrence Charles: MetiTarski: An automatic theorem prover for real-valued special functions (2010)
- Lyaletski, Alexander; Verchinine, Konstantin: Evidence algorithm and system for automated deduction: a retrospective view. (In honor of 40 years of the EA announcement) (2010)
- Björk, Magnus: First order St\aalmarck. Universal lemmas through branch merges (2009)
- Cadoli, Marco; Patrizi, Fabio: On the separability of subproblems in Benders decompositions (2009)
- Höfner, Peter; Struth, Georg; Sutcliffe, Geoff: Automated verification of refinement laws (2009)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Akbarpour, Behzad; Paulson, Lawrence C.: MetiTarski: An automatic prover for the elementary functions (2008)
- Hommersom, Arjen; Lucas, Peter J.F.; van Bommel, Patrick: Checking the quality of clinical guidelines using automated reasoning tools (2008)
- Kinyon, Michael K.; Phillips, J.D.; Vojtěchovský, Petr: When is the commutant of a Bol loop a subloop? (2008)