From Schütte’s Formal Systems to Modern Automated Deduction

DOI10.1007/978-3-030-49424-7_13MaRDI QIDQ5013905

Jens Otten, Wolfgang Bibel

Publication date: 3 December 2021

Published in: The Legacy of Kurt Schütte (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-49424-7_13

Mathematics Subject Classification ID

03-XX: Mathematical logic and foundations

68-XX: Computer science

Related Items

Learning from Łukasiewicz and Meredith: investigations into proof structures, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics

Cites Work

• Linearity and regularity with negation normal form
• Liberalized variable splitting
• The ILTP problem library for intuitionistic logic
• Proof methods for modal and intuitionistic logics
• A structure-preserving clause form translation
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• Controlled integration of the cut rule into connection tableau calculi
• IeanCOP: lean connection-based theorem proving
• A vision for automated deduction rooted in the connection method
• Non-clausal connection calculi for non-classical logics
• Untersuchungen über das logische Schliessen. I
• An approach to a systematic theorem proving procedure in first-order logic
• nanoCoP: A Non-clausal Connection Prover
• The QMLTP Problem Library for First-Order Modal Logics
• A Non-clausal Connection Calculus
• MleanCoP: A Connection Prover for First-Order Modal Logic
• A proof procedure for quantification theory
• Ein System des Verknüpfenden Schliessens
• An improved proof procedure1
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Restricting backtracking in connection calculi
• Matings in matrices
• Theorem Proving via General Matings
• On Matrices with Connections
• A system of interaction and structure
• Automated Reasoning with Analytic Tableaux and Related Methods
• A Machine-Oriented Logic Based on the Resolution Principle
• Mechanical Theorem-Proving by Model Elimination
• A Mechanical Proof Procedure and its Realization in an Electronic Computer
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item