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 119 articles , 1 standard article )
Showing results 1 to 20 of 119.
Sorted by year (- Loveland, Donald W.: Mark Stickel: his earliest work (2016)
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
- Furbach, Ulrich: First-order tableaux in applications (extended abstract) (2011)
- 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: \textitTheorema: 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)
- Miller, Swaha; Plaisted, David A.: The space efficiency of OSHL (2005)
- Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
- Denney, Ewen; Fischer, Bernd; Schumann, Johann: Using automated theorem provers to certify auto-generated aerospace software (2004)
- 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)