Modal tableau systems with blocking and congruence closure

DOI10.1007/978-3-319-24312-2_4MaRDI QIDQ3455760zbMATH OpenOpenAlexFDO

Authors Renate A. Schmidt, Uwe Waldmann

Publication date 11 December 2015

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

Full work available at URL https://doi.org/10.1007/978-3-319-24312-2_4

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Recommendations

• Symmetric blocking
• TABLEAUX: A general theorem prover for modal logics
• Dealing with Symmetries in Modal Tableaux
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
• First-order modal tableaux

Cites work

• A refined tableau calculus with controlled blocking for the description logic \(\mathcal{SHOI}\)
• Abstract congruence closure
• An overview of tableau algorithms for description logics
• Automated synthesis of tableau calculi
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Equality reasoning in sequent-based calculi
• Fast congruence closure and extensions
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 4088977 (Why is no real title available?)
• Hybrid tableaux for the difference modality
• Semantic tableaux with equality
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Superposition-based equality handling for analytic tableaux
• Tableau methods for modal and temporal logics
• Term Rewriting and All That
• Termination for Hybrid Tableaus
• Using tableau to decide description logics with full role negation and identity

Cited in

(5)

• Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
• Deciding the word problem for ground identities with commutative and extensional symbols
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Refined tableau systems for some modal logics of confluence
• Symmetric blocking

Describes a project that uses

Uses Software

• MetTeL
• KL-ONE

This page was built for publication: Modal tableau systems with blocking and congruence closure

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