Automated Reasoning with Analytic Tableaux and Related Methods

DOI10.1007/11554554zbMath1142.03331OpenAlexW2486590071MaRDI QIDQ5479281

Jens Otten

Publication date: 7 July 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11554554

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Aligning concepts across proof assistant libraries ⋮ The ILTP problem library for intuitionistic logic ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ A Non-clausal Connection Calculus ⋮ Proof Search for the First-Order Connection Calculus in Maude ⋮ Machine learning guidance for connection tableaux ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ Bayesian ranking for strategy scheduling in automated theorem provers

Uses Software

• SETHEO
• TPTP
• Nuprl
• leanCoP
• ileanCoP
• JProver

This page was built for publication: Automated Reasoning with Analytic Tableaux and Related Methods