The tableau-based theorem prover 3 T A P Version 4.0

DOI10.1007/3-540-61511-3_95zbMath1412.68207OpenAlexW1720975781MaRDI QIDQ4647529

Martin Sulzmann, Bernhard Beckert, Peter Oel, Reiner Hähnle

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_95

Mathematics Subject Classification ID

Related Items (5)

Free variable tableaux for propositional modal logics ⋮ Ordered tableaux: Extensions and applications ⋮ The tableau-based theorem prover 3 T A P Version 4.0 ⋮ Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis ⋮ JGXYZ: an ATP system for gap and glut logics

Uses Software

• TPTP
• 3TAP
• HARP

Cites Work

• Controlled integration of the cut rule into connection tableau calculi
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• lean\(T^ AP\): Lean tableau-based deduction
• A Beginner's Further Guide to Mathematical Logic
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Incremental theory reasoning methods for semantic tableaux
• The tableau-based theorem prover 3 T A P Version 4.0
• The TPTP problem library
• A completion-based method for mixed universal and rigid E-unification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The tableau-based theorem prover 3 T A P Version 4.0