SETHEO
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.
Keywords for this software
References in zbMATH (referenced in 79 articles , 1 standard article )
Showing results 1 to 20 of 79.
Sorted by year (- Loveland, Donald W.: Mark Stickel: his earliest work (2016)
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Brandt, Christoph; Otten, Jens; Kreitz, Christoph; Bibel, Wolfgang: Specifying and verifying organizational security properties in first-order logic (2010)
- Jürjens, Jan: A domain-specific language for cryptographic protocols based on streams (2009)
- Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
- Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
- Paskevich, Andrei: Connection tableaux with lazy paramodulation (2008)
- Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
- Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, Wolfgang: \itTheorema: Towards computer-aided mathematical theory exploration (2006)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
- Bonacina, Maria Paola: Towards a unified model of search in theorem-proving: subgoal-reduction strategies (2005)
- Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Beckert, Bernhard: Depth-first proof search without backtracking for free-variable clausal tableaux (2003)
- Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
- Riazanov, Alexandre; Voronkov, Andrei: Limited resource strategy in resolution theorem proving (2003)
- Choi, Seungyeob: Towards semantic goal-directed forward reasoning in resolution (2002)
- Beckert, Bernhard; Goré, Rajeev: Free-variable tableaux for propositional modal logics (2001)
- Hodas, Joshua S.; Tamura, Naoyuki: lolliCoP -- a linear logic implementation of a lean connection-method theorem prover for first-order classical logic (2001)
- Letz, Reinhold; Stenz, Gernot: Model elimination and connection tableau procedures (2001)