An overview of tableau algorithms for description logics

Cited In (44)

A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
Blocking and other enhancements for bottom-up model generation methods
HermiT: an OWL 2 reasoner
Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach
Title not available (Why is that?)
A polynomial space construction of tree-like models for logics with local chains of modal connectives
A new methodology for developing deduction methods
Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics
Efficient TBox Reasoning with Value Restrictions using the wer Reasoner
Representing ontologies using description logics, description graphs, and rules
Title not available (Why is that?)
Title not available (Why is that?)
On the decidability status of fuzzy $\mathcal {A}\mathcal {L}\mathcal {C}$ with general concept inclusions
Description Logics
Reasoning on UML class diagrams
Modal Tableau Systems with Blocking and Congruence Closure
Converse-PDL with regular inclusion axioms: a framework for MAS logics
Data complexity of query answering in expressive description logics via tableaux
Hybrid logics and ontology languages
Using tableau to decide description logics with full role negation and identity
A tableau decision procedure for $\mathcal{SHOIQ}$
A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases
Combining Description Logics, Description Graphs, and Rules
Ontology Integration Using ε-Connections
Experimental analysis of some computation rules in a simple parallel reasoning system for the ALC description logic
An Optimized KE-Tableau-Based System for Reasoning in the Description Logic $${\mathcal {DL}}_{{\mathbf {D}}}^{4,\!\times }$$
On the Undecidability of Fuzzy Description Logics with GCIs and Product T-norm
Consistency reasoning in lattice-based fuzzy description logics
A hybrid reasoning system for terminologies and first-order clauses in knowledge bases
Automata-based axiom pinpointing
Lightweight hybrid tableaux
Optimizing terminological reasoning for expressive description logics
Ontologies and Databases: The DL-Lite Approach
Computing the least common subsumer w.r.t. a background terminology
A Tableau Calculus for Regular Grammar Logics with Converse
Title not available (Why is that?)
ExpTime tableaux for $\mathcal {ALC}$ using sound global caching
PS\textsc{pace} tableau algorithms for acyclic modalized ${\mathcal{ALC}}$
Title not available (Why is that?)
ExpTime tableau decision procedures for regular grammar logics with converse
Automata-Based Axiom Pinpointing
Automata can show PSpace results for description logics
ExpTime tableaux with global caching for hybrid PDL
A Modal Supervaluation Description Logic for Characterization of Vague Concepts: its semantics and a tableau algorithm for it

Uses Software

FaCT++
KL-ONE
ICOM

   Recommendations

Title not available (Why is that?) 👍 👎
Title not available (Why is that?) 👍 👎
Title not available (Why is that?) 👍 👎
Title not available (Why is that?) 👍 👎
Practical reasoning for very expressive description logics 👍 👎

This page was built for publication: An overview of tableau algorithms for description logics

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