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.
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Let's plan it deductively!
- Prolog technology for default reasoning: proof theory and compilation techniques
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- SET-VAR
- Controlled integration of the cut rule into connection tableau calculi
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Non-Horn clause logic programming
- Computing answers with model elimination
- IeanCOP: lean connection-based theorem proving
- Evaluating general purpose automated theorem proving systems
- Towards the qualitative, plan-based simulation of international crises
- A uniform procedure for converting matrix proofs into sequent-style systems
- A new methodology for query answering in default logics via structure-oriented theorem proving
- lean\(T^ AP\): Lean tableau-based deduction
- Linear and unit-resulting refutations for Horn theories
- Near-Horn Prolog and the ancestry family of procedures
- Knowledge-based proof planning
- Machine learning guidance for connection tableaux
- Set of support, demodulation, paramodulation: a historical perspective
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Craig interpolation with clausal first-order tableaux
- scientific article; zbMATH DE number 1612568 (Why is no real title available?)
- Mark Stickel: his earliest work
- Specifying and verifying organizational security properties in first-order logic
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Large theory reasoning with SUMO at CASC
- scientific article; zbMATH DE number 3986666 (Why is no real title available?)
- scientific article; zbMATH DE number 4022667 (Why is no real title available?)
- scientific article; zbMATH DE number 517015 (Why is no real title available?)
- scientific article; zbMATH DE number 1765689 (Why is no real title available?)
- Free variable tableaux for propositional modal logics
- Ordered tableaux: extensions and applications
- Subgoal alternation in model elimination
- A framework for using knowledge in tableau proofs
- Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison
- T-string unification: unifying prefixes in non-classical proof methods
- SiCoTHEO: Simple competitive parallel theorem provers
- Optimizing proof search in model elimination
- Converting non-classical matrix proofs into sequent-style systems
- From Schütte’s Formal Systems to Modern Automated Deduction
- scientific article; zbMATH DE number 7455734 (Why is no real title available?)
- Model elimination without contrapositives
- Detecting non-provable goals
- Semantic tableaux with ordering restrictions
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- ILF-SETHEO
- SETHEO goes software engineering: application of ATP to software reuse
- Automatic verification of cryptographic protocols with SETHEO
- An automatic proof of Gödel's incompleteness theorem
- Controlled use of clausal lemmas in connection tableau calculi
- An examination of the prolog technology theorem-prover
- Automatic acquisition of search guiding heuristics
- Range-restricted and Horn interpolation through clausal tableaux
- Lemmas: generation, selection, application
- Deduction by combining semantic tableaux and integer programming
- Representing unification in a logical framework
- Investigations into proof structures
- Finding connections via satisfiability solving
- Theo: An interactive proof development system
- Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic
- Octopus: combining learning and parallel search
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Connection tableaux with lazy paramodulation
This page was built for publication: SETHEO: A high-performance theorem prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1189726)
