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 286 articles , 1 standard article )
Showing results 1 to 20 of 286.
Sorted by year (- Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: Proofwatch: watchlist guidance for large theories in E (2018)
- Beeson, Michael; Wos, Larry: Finding proofs in Tarskian geometry (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
- Coghetto, Roland; Grabowski, Adam: Tarski geometry axioms. III (2017)
- Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
- Rump, Wolfgang: Quantum B-algebras: their omnipresence in algebraic logic and beyond (2017)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
- Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
- Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\textK_ \textS\textP): a resolution-based prover for multimodal K (2016)
- Padmanabhan, Ranganathan; Zhang, Yang: Automated deduction in ring theory (2016)
- Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (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)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Stojanović Đ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)
- Demri, Stéphane (ed.); Kapur, Deepak (ed.); Weidenbach, Christoph (ed.): Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19--22, 2014. Proceedings (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)