Modal Tableau Systems with Blocking and Congruence Closure (Q3455760): Difference between revisions

@@ Property / describes a project that uses @@
+KL-ONE
@@ Property / describes a project that uses: KL-ONE / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-319-24312-2_4
+Normal rank
@@ Property / OpenAlex ID @@
+W2242840523
@@ Property / OpenAlex ID: W2242840523 / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+An overview of tableau algorithms for description logics
+Normal rank
@@ Property / cites work @@
+Abstract congruence closure
@@ Property / cites work: Abstract congruence closure / rank @@
+Normal rank
@@ Property / cites work @@
+Blocking and Other Enhancements for Bottom-Up Model Generation Methods
+Normal rank
@@ Property / cites work @@
+Semantic tableaux with equality
@@ Property / cites work: Semantic tableaux with equality / rank @@
+Normal rank
@@ Property / cites work @@
+Termination for Hybrid Tableaus
@@ Property / cites work: Termination for Hybrid Tableaus / rank @@
+Normal rank
@@ Property / cites work @@
+Q3817018
@@ Property / cites work: Q3817018 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751362
@@ Property / cites work: Q2751362 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition-based equality handling for analytic tableaux
+Normal rank
@@ Property / cites work @@
+Q2753601
@@ Property / cites work: Q2753601 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid Tableaux for the Difference Modality
@@ Property / cites work: Hybrid Tableaux for the Difference Modality / rank @@
+Normal rank
@@ Property / cites work @@
+A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Fast congruence closure and extensions
@@ Property / cites work: Fast congruence closure and extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Synthesis of Tableau Calculi
@@ Property / cites work: Automated Synthesis of Tableau Calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Using tableau to decide description logics with full role negation and identity
+Normal rank