From Schütte’s Formal Systems to Modern Automated Deduction
From MaRDI portal
Publication:5013905
DOI10.1007/978-3-030-49424-7_13OpenAlexW3048692132MaRDI QIDQ5013905
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
Related Items
The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures
Cites Work
- 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
- 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