SETHEO swMATH ID: 707 Software Authors: Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W. Description: SETHEO: A high-performance theorem prover. The paper deals with a theoretical background and practical knowledge of the implementation of the interesting system SETHEO — a theorem prover for first order logic. The system is based on the connection method and is proved to be sound and complete. SETHEO can be used as an interpreter for the programming language LOP (under development). The inference machine of the system is implemented using Prolog technology, but there are some special characteristics differing SETHEO from common Prolog systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure is realized as a WAM, factorization, lemma generation and the application of proof schemata are offered as options. The entire system is implemented in the language \(C\) and is running on several machines. The important feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips. Homepage: http://www2.tcs.ifi.lmu.de/~letz/TU/setheo/ Keywords: model elimination; abstract machine technology; first order logic; connection method; Prolog; preprocessing Related Software: TPTP; PTTP; OTTER; SPASS; VAMPIRE; E-SETHEO; SATCHMO; METEOR; leanCoP; PARTHEO; Nuprl; PROTEIN; leanTAP; KoMeT; HARP; DISCOUNT; Bliksem; Waldmeister; PARTHENON; Mace4 Cited in: 122 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year PIL/SETHEO: A tool for the automatic analysis of authentication protocols. Zbl 1046.68526Schumann, Johann 1999 all top 5 Cited by 118 Authors 10 Schumann, Johann M. Ph. 9 Letz, Reinhold 7 Baumgartner, Peter 7 Beckert, Bernhard 7 Bibel, Wolfgang 6 Brüning, Stefan 6 Otten, Jens 5 Furbach, Ulrich 5 Hähnle, Reiner 5 Kreitz, Christoph 5 Suttner, Christian B. 5 Wolf, Andreas 4 Bonacina, Maria Paola 4 Fischer, Bernd 4 Fuchs, Dirk 4 Stenz, Gernot 4 Voronkov, Andrei 3 Fuchs, Marc 3 Loveland, Donald W. 3 Schaub, Torsten H. 3 Schmitt, Stephan 3 Sutcliffe, Geoff 3 Wernhard, Christoph 2 Almulla, Mohammed 2 Benzmüller, Christoph Ewald 2 Dahn, Bernd Ingo 2 Geisler, Tim 2 Goré, Rajeev Prabhakar 2 Ibens, Ortrun 2 Kaliszyk, Cezary 2 Newborn, Monroe M. 2 Posegga, Joachim 2 Reif, Wolfgang 2 Schellhorn, Gerhard 2 Schmitt, Peter H. 2 Schütz, Heribert 2 Sorge, Volker 1 Ahrendt, Wolfgang 1 Ammon, Kurt 1 Astrachan, O. L. 1 Bachmair, Leo 1 Balzer, Wolfgang 1 Bayerl, Stephan H. A. 1 Blohm, Antje 1 Brandt, Christoph 1 Brown, Marianne S. 1 Buchberger, Bruno 1 Choi, Seungyeob 1 Crǎciun, Adrian 1 Dahn, Ingo 1 Denney, Ewen 1 Draeger, Joachim 1 Dyckhoff, Roy 1 Egly, Uwe 1 Ertel, Wolfgang 1 Färber, Michael 1 Fronhöfer, Bertram 1 Ganzinger, Harald 1 Gehne, Jürgen 1 Goller, Christoph 1 Harrison, John R. 1 Hodas, Joshua S. 1 Honigmann, Th. 1 Horton, Joseph D. 1 Hsiang, Jieh 1 Iwanuma, Koji 1 Jamnik, Mateja 1 Jebelean, Tudor 1 Jürjens, Jan 1 Kerber, Manfred 1 Klingenbeck, Stefan 1 Kovács, Laura Ildikó 1 Kutsia, Temur 1 Mayr, Klaus 1 McCune, William W. 1 Meier, Andreas 1 Melis, Erica 1 Menzel, Wolfram 1 Miller, Swaha 1 Nakagawa, Koji 1 Newborn, Monty 1 Nicolas, Pascal 1 Nie, Xumin 1 Pape, Christian 1 Paskevich, Andrei 1 Petermann, Uwe 1 Pfalzgraf, Jochen 1 Piroi, Florina 1 Plaisted, David Alan 1 Popov, Nikolaj 1 Prokosch, Thomas 1 Rath, Thomas 1 Reed, David W. 1 Riazanov, Alexandre 1 Robu, Judit 1 Rosenkranz, Markus 1 Sander, Jörg 1 Schulz, Stephan 1 Segre, Alberto Maria 1 Shults, Benjamin ...and 18 more Authors all top 5 Cited in 18 Serials 17 Journal of Automated Reasoning 8 Artificial Intelligence 6 Journal of Symbolic Computation 3 Information and Computation 3 Annals of Mathematics and Artificial Intelligence 2 Studia Logica 2 Journal of Applied Logic 1 Theoretical Computer Science 1 The Journal of Logic Programming 1 Journal of Logic and Computation 1 European Journal of Operational Research 1 International Journal of Computer Mathematics 1 The Journal of Artificial Intelligence Research (JAIR) 1 Fundamenta Informaticae 1 Journal of Universal Computer Science 1 The Journal of Logic and Algebraic Programming 1 Lecture Notes in Computer Science 1 Applied Logic Series all top 5 Cited in 9 Fields 114 Computer science (68-XX) 40 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 2 Operations research, mathematical programming (90-XX) 1 History and biography (01-XX) 1 Commutative algebra (13-XX) 1 Numerical analysis (65-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year