Modal Tableau Systems with Blocking and Congruence Closure

DOI10.1007/978-3-319-24312-2_4zbMath1471.03018OpenAlexW2242840523MaRDI QIDQ3455760

Uwe Waldmann, Renate A. Schmidt

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

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

Related Items (3)

Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ 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

Uses Software

• MetTeL
• KL-ONE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast congruence closure and extensions
• Superposition-based equality handling for analytic tableaux
• Abstract congruence closure
• Semantic tableaux with equality
• A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
• Solving SAT and SAT Modulo Theories
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Fast Decision Procedures Based on Congruence Closure
• Term Rewriting and All That
• Hybrid Tableaux for the Difference Modality
• Using tableau to decide description logics with full role negation and identity
• Termination for Hybrid Tableaus
• Automated Synthesis of Tableau Calculi
• An overview of tableau algorithms for description logics

This page was built for publication: Modal Tableau Systems with Blocking and Congruence Closure