swMATH ID: 2904
Software Authors: Bill McCune; Amor Montano, Jose Alfredo; Miranda Perea, Favio Ezequiel
Description: 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.
Homepage: http://www.mcs.anl.gov/research/projects/AR/otter/
Programming Languages: ANSI C
Operating Systems: Unix-like systems, Windows
Dependencies: None
Keywords: classical logic; finitely described theory; predicate language with equality
Related Software: TPTP; Mace4; VAMPIRE; SPASS; E Theorem Prover; SETHEO; Prover9; Mizar; Coq; SATCHMO; Isabelle/HOL; HOL; Isabelle; Waldmeister; Nuprl; Mathematica; MPTP 0.2; PVS; Bliksem; METEOR
Referenced in: 302 Publications
all top 5

Referenced by 319 Authors

30 Wos, Larry
18 McCune, William W.
12 Bonacina, Maria Paola
12 Padmanabhan, Ranganathan
11 Urban, Josef
10 Fitelson, Branden
9 Colton, Simon
9 Kinyon, Michael K.
9 Kunen, Kenneth
9 Veroff, Robert
8 Plaisted, David Alan
8 Sutcliffe, Geoff
7 Meier, Andreas
7 Paulson, Lawrence Charles
7 Voronkov, Andrei
6 de Nivelle, Hans
6 Schulz, Stephan
6 Sorge, Volker
5 Beeson, Michael J.
5 Belinfante, Johan Gijsbertus Frederik
5 Dixon, Clare
5 Melis, Erica
5 Omodeo, Eugenio Giovanni
5 Siekmann, Jörg H.
4 Benzmüller, Christoph Ewald
4 Formisano, Andrea
4 Hsiang, Jieh
4 Jakubův, Jan
4 Riazanov, Alexandre
4 Vojtěchovský, Petr
4 Weidenbach, Christoph
3 Akbarpour, Behzad
3 Blanchette, Jasmin Christian
3 Cadoli, Marco
3 Furbach, Ulrich
3 Grabowski, Adam
3 Hustadt, Ullrich
3 Iwanuma, Koji
3 Kaliszyk, Cezary
3 Ohlbach, Hans Jürgen
3 Pieper, Gail W.
3 Quaife, Art
3 Slaney, John K.
3 Suttner, Christian B.
3 Temperini, Marco
3 Zhang, Yang
2 Asperti, Andrea
2 Baumgartner, Peter
2 Caferra, Ricardo
2 Coghetto, Roland
2 de Moura, Leonardo
2 Ernst, Zachary
2 Fehrer, Detlef
2 Fuchs, Matthias
2 Harris, Kenneth D. M.
2 Hillenbrand, Thomas
2 Hodgson, Kahlil
2 Janičić, Predrag
2 Kohlhase, Michael
2 Kovács, Laura Ildikó
2 Kutsia, Temur
2 Lyaletski, Alexander V.
2 Lynch, Christopher A.
2 Mancini, Toni
2 Miller, Swaha
2 Moore, J Strother
2 Nalon, Cláudia
2 Narboux, Julien
2 Newborn, Monty
2 Olšák, Miroslav
2 Otten, Jens
2 Peltier, Nicolas
2 Pelzer, Björn
2 Pollet, Martin
2 Rawson, Michael
2 Reger, Giles
2 Reif, Wolfgang
2 Sacerdoti Coen, Claudio
2 Schellhorn, Gerhard
2 Schmidt, Renate A.
2 Spinks, Matthew
2 Stickel, Mark E.
2 Tassi, Enrico
2 Ulrich, Dolph
2 Verchinine, Konstantin
2 Vyskočil, Jiří
2 Wiedijk, Freek
2 Zhang, Hantao
1 Abrial, Jean-Raymond
1 Adaricheva, Kira Vladislavovna
1 Agre, Keith M.
1 Almulla, Mohammed
1 Alves-Foss, James
1 Amir, Eyal
1 Ammon, Kurt
1 Amor Montaño, José Alfredo
1 Araújo, João
1 Autexier, Serge
1 Baader, Franz
1 Bachmair, Leo
...and 219 more Authors
all top 5

Referenced in 58 Serials

62 Journal of Automated Reasoning
16 Journal of Symbolic Computation
9 Artificial Intelligence
8 Annals of Mathematics and Artificial Intelligence
6 Computers & Mathematics with Applications
5 Journal of Applied Logic
4 Journal of Algebra
4 Lecture Notes in Computer Science
3 Notre Dame Journal of Formal Logic
3 Bulletin of the Section of Logic
2 Information Processing Letters
2 Algebra Universalis
2 Information Sciences
2 Journal of Philosophical Logic
2 Semigroup Forum
2 Studia Logica
2 Theoretical Computer Science
2 Transactions of the American Mathematical Society
2 Annales Societatis Mathematicae Polonae. Series IV
2 AI Communications
2 Journal of Formalized Reasoning
2 Formalized Mathematics
1 American Mathematical Monthly
1 Communications in Algebra
1 Houston Journal of Mathematics
1 Beiträge zur Algebra und Geometrie
1 Algebra and Logic
1 Applied Mathematics and Computation
1 Commentationes Mathematicae Universitatis Carolinae
1 Le Matematiche
1 Proceedings of the American Mathematical Society
1 Topology and its Applications
1 Annals of Pure and Applied Logic
1 Information and Computation
1 Computational Mechanics
1 Data & Knowledge Engineering
1 Annals of Operations Research
1 Machine Learning
1 JETAI. Journal of Experimental & Theoretical Artificial Intelligence
1 Journal of Logic and Computation
1 European Journal of Operational Research
1 Applicable Algebra in Engineering, Communication and Computing
1 International Journal of Human-Computer Studies
1 The Journal of Artificial Intelligence Research (JAIR)
1 Kuwait Journal of Science and Engineering
1 Logic Journal of the IGPL
1 Soft Computing
1 Data Mining and Knowledge Discovery
1 Quasigroups and Related Systems
1 Journal of Universal Computer Science
1 Theory and Practice of Logic Programming
1 Aportaciones Matemáticas. Comunicaciones
1 Automated Reasoning Series
1 Proceedings of the Steklov Institute of Mathematics
1 Oxford Texts in Logic
1 DISKI. Dissertationen zur Künstlichen Intelligenz
1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Distinguished Dissertations

Referencing Publications by Year