Modal Tableau Systems with Blocking and Congruence Closure
From MaRDI portal
Publication:3455760
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
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
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