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

DOI10.1007/3-540-61511-3_95zbMATH Open1412.68207OpenAlexW1720975781MaRDI QIDQ4647529FDOQ4647529

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

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

Cites Work

• lean\(T^ AP\): Lean tableau-based deduction
• Title not available (Why is that?)
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Title not available (Why is that?)
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Title not available (Why is that?)
• Title not available (Why is that?)
• A completion-based method for mixed universal and rigid \(E\)-unification
• Title not available (Why is that?)
• The TPTP problem library
• Controlled integration of the cut rule into connection tableau calculi
• Incremental theory reasoning methods for semantic tableaux
• Title not available (Why is that?)
• The tableau-based theorem prover 3 T A P Version 4.0
• A beginner's further guide to mathematical logic
• Title not available (Why is that?)

Cited In (5)

• JGXYZ: an ATP system for gap and glut 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
• Free variable tableaux for propositional modal logics

Uses Software

• TPTP
• 3TAP
• HARP

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647529)