An Overview of Tableau Algorithms for Description Logics

By Franz Baader, U. Sattler. Studia Logica: An International Journal for Symbolic Logic, 2001

496 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems

View Paper: https://www.semanticscholar.org/paper/7657a33a7e9d9617b317e71066f4de119bec77b7

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

Citations in the corpus

Computing the Least Common Subsumer w.r.t. a Background Terminology (2004, background): “Since the usual tableau-based subsumption algorithms [12] in principle try to generate finite countermodels to subsumption relationships, they can usually be extended such that they yield such an object in case the subsumption relationship does not hold.”
Reasoning on UML class diagrams (2005, methodology): “These algorithms are based on tableaux techniques [43] and, although not optimal from the computational complexity point of view, are highly optimized and exhibit good average case performance [44].”
Description Logics as Ontology Languages for the Semantic Web (2005, background): “Description logics (DLs) [7, 24] are a family of knowledge representation languages that can be used to represent the knowledge of an application domain in a structured and formally well-understood way.”
Hypertableau Reasoning for Description Logics (2009, methodology): “To the best of our knowledge, this problem was first identified by Baader and Sattler (2001), and it is commonly known as a “yo-yo.””
A Tableaux Decision Procedure for SHOIQ (2005, methodology): “8 For example, this effect led to the introduction of “fork elimination” in (Baader and Hanschke, 1991) and is described in detail in (Baader and Sattler, 2001).”
Bridging the gap between OWL and relational databases (2007, background): “Namely, reasoning in description logics is typically performed by tableau algorithms [5], whereas the state-ofthe-art reasoning technique in relational databases is chase [1].”
HermiT: An OWL 2 Reasoner (2014, background): “At least in their unoptimised form [3], tableau calculi transform such axioms into negation-normal form and then apply them to all individuals occurring in a derivation.”
Pellet: A practical OWL-DL reasoner (2007, background): “cess when a “cycle” that can cause infinite expansion is detected [ 14 ].”