A Bottom-Up Approach to Clausal Tableaux

DOI10.1007/978-3-540-73099-6_16MaRDI QIDQ5434490zbMATH OpenOpenAlexFDO

Authors Nicolas Peltier

Publication date 4 January 2008

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

Full work available at URL https://doi.org/10.1007/978-3-540-73099-6_16

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• Bottom-up Construction of Semantic Tableaux
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Clausal intuitionistic logic II. tableau proof procedures
• Publication:4860661
• Hyper tableaux

Cited in

(10)

• Depth-first proof search without backtracking for free-variable clausal tableaux
• A tableaux calculus for reducing proof size
• A-ordered tableaux
• Bottom-up Construction of Semantic Tableaux
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Clausal intuitionistic logic II. tableau proof procedures
• scientific article; zbMATH DE number 834573 (Why is no real title available?)
• A more efficient tableaux procedure for simultaneous search for refutations and finite models
• A First Order Extension of Stålmarck’s Method
• scientific article; zbMATH DE number 5661162 (Why is no real title available?)

This page was built for publication: A Bottom-Up Approach to Clausal Tableaux

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