OTTER 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; VAMPIRE; Mace4; SPASS; E Theorem Prover; SETHEO; Prover9; Coq; Mizar; Isabelle/HOL; SATCHMO; Waldmeister; HOL; Isabelle; DISCOUNT; Nuprl; Mathematica; Bliksem; PVS; MPTP 0.2 Cited in: 324 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Automatic theorem proving and OTTER. Zbl 0965.03011Amor Montaño, José Alfredo; Miranda Perea, Favio Ezequiel 1998 all top 5 Cited by 343 Authors 30 Wos, Larry 20 McCune, William W. 14 Bonacina, Maria Paola 12 Padmanabhan, Ranganathan 11 Urban, Josef 10 Fitelson, Branden 10 Kinyon, Michael K. 10 Veroff, Robert 9 Blanchette, Jasmin Christian 9 Colton, Simon 9 Kunen, Kenneth 9 Sutcliffe, Geoff 8 Plaisted, David Alan 7 Meier, Andreas 7 Paulson, Lawrence Charles 7 Tourret, Sophie 7 Voronkov, Andrei 6 Beeson, Michael J. 6 de Nivelle, Hans 6 Schulz, Stephan 6 Sorge, Volker 6 Weidenbach, Christoph 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 Slaney, John K. 4 Vojtěchovský, Petr 3 Akbarpour, Behzad 3 Cadoli, Marco 3 Furbach, Ulrich 3 Grabowski, Adam 3 Hustadt, Ullrich 3 Iwanuma, Koji 3 Kaliszyk, Cezary 3 Lusk, Ewing L. 3 Ohlbach, Hans Jürgen 3 Pieper, Gail W. 3 Quaife, Art 3 Suttner, Christian B. 3 Temperini, Marco 3 Vukmirović, Petar 3 Waldmann, Uwe 3 Zhang, Yang 2 Asperti, Andrea 2 Bachmair, Leo 2 Baumgartner, Peter 2 Bentkamp, Alexander 2 Caferra, Ricardo 2 Coghetto, Roland 2 Cruanes, Simon 2 de Moura, Leonardo 2 Ebner, Gabriel 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 Korovin, Konstantin 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 Nummelin, Visa 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 Robillard, Simon 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 ...and 243 more Authors all top 5 Cited in 59 Serials 69 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 ACM Transactions on Computational Logic 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 all top 5 Cited in 23 Fields 284 Computer science (68-XX) 127 Mathematical logic and foundations (03-XX) 25 Group theory and generalizations (20-XX) 8 Order, lattices, ordered algebraic structures (06-XX) 7 General algebraic systems (08-XX) 7 Geometry (51-XX) 4 General and overarching topics; collections (00-XX) 4 History and biography (01-XX) 4 Algebraic geometry (14-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Number theory (11-XX) 3 Operations research, mathematical programming (90-XX) 2 Commutative algebra (13-XX) 2 Statistics (62-XX) 1 Combinatorics (05-XX) 1 Associative rings and algebras (16-XX) 1 General topology (54-XX) 1 Numerical analysis (65-XX) 1 Mechanics of deformable solids (74-XX) 1 Biology and other natural sciences (92-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) 1 Mathematics education (97-XX) Citations by Year