SETHEO: A high-performance theorem prover
From MaRDI portal
Publication:1189726
DOI10.1007/BF00244282zbMath0759.68080OpenAlexW2084894656MaRDI QIDQ1189726
Publication date: 27 September 1992
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00244282
Related Items
Mark Stickel: his earliest work ⋮ Controlled integration of the cut rule into connection tableau calculi ⋮ A new methodology for query answering in default logics via structure-oriented theorem proving ⋮ KoMeT ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ Octopus: combining learning and parallel search ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ ILF-SETHEO ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Craig interpolation with clausal first-order tableaux ⋮ Near-Horn Prolog and the ancestry family of procedures ⋮ 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 ⋮ 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 ⋮ Unnamed Item ⋮ Connection tableaux with lazy paramodulation ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Knowledge-based proof planning ⋮ 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 ⋮ An automatic proof of Gödel's incompleteness theorem ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ Model elimination without contrapositives ⋮ Detecting non-provable goals ⋮ Semantic tableaux with ordering restrictions ⋮ 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 ⋮ SETHEO goes software engineering: Application of ATP to software reuse ⋮ Automatic verification of cryptographic protocols with SETHEO ⋮ A uniform procedure for converting matrix proofs into sequent-style systems ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ Evaluating general purpose automated theorem proving systems ⋮ Towards the qualitative, plan-based simulation of international crises
Uses Software
