Ordered tableaux: Extensions and applications

DOI10.1007/BFb0027413zbMath1412.68230OpenAlexW1503268616MaRDI QIDQ4610325

Reiner Hähnle, Christian Pape

Publication date: 15 January 2019

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

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

Mathematics Subject Classification ID

Related Items (1)

Depth-first proof search without backtracking for free-variable clausal tableaux

Uses Software

• SETHEO
• OTTER
• TPTP
• 3TAP
• HARP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Simple LPO constraint solving methods
• SETHEO: A high-performance theorem prover
• Resolution methods for the decision problem
• A-ordered tableaux
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• The tableau-based theorem prover 3 T A P Version 4.0
• Model elimination without contrapositives
• The TPTP problem library
• Semantic tableaux with ordering restrictions
• Mechanical Theorem-Proving by Model Elimination

This page was built for publication: Ordered tableaux: Extensions and applications