Complexity results and practical algorithms for logics in knowledge representation

By Stephan Tobies. arXiv.org, 2001

436 citations recorded by the source corpus.

Description Logics (DLs) are used in knowledge-based systems to represent and reason about terminological knowledge of the application domain in a semantically well-defined manner. In this thesis, we establish a number of novel complexity results and give practical algorithms for expressive DLs that provide different forms of counting quantifiers. We show that, in many cases, adding local counting in the form of qualifying number restrictions to DLs does not increase the complexity of the inference problems, even if binary coding of numbers in the input is assumed. On the other hand, we show that adding different forms of global counting restrictions to a logic may increase the complexity of the inference problems dramatically. We provide exact complexity results and a practical, tableau based algorithm for the DL SHIQ, which forms the basis of the highly optimized DL system iFaCT. Finally, we describe a tableau algorithm for the clique guarded fragment (CGF), which we hope will serve as the basis for an efficient implementation of a CGF reasoner.

Subfields: Artificial Intelligence

View Paper: https://www.semanticscholar.org/paper/63559889e182d75764a7490dc5278792e60a104f

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

Citations in the corpus

A Tableaux Decision Procedure for SHOIQ (2005, background): “, no goal directed procedure that is likely to perform well with realistic ontology derived problems [Tobies, 2001; Horrocks & Sattler, 2001].”
Query Answering for OWL-DL with Rules (2004, methodology): “For unary coding of numbers and assuming a bound on the arity of predicates in rules, our algorithm runs in deterministic exponential time, which makes it optimal since SHIQ is ExpTime-complete [21].”
The DL-Lite Family and Relations (2009, background): “Remark 5.21 It should be noted that role disjointness, symmetry, asymmetry and transitivity constraints can be added to any of the logics DL-LiteHFα and DL-Lite HN α , for α ∈ {core, krom, horn, bool}, without changing the combined complexity of their satisfiability problems (which, by Corollary 5.1”
From SHIQ and RDF to OWL: the making of a Web Ontology Language (2003, methodology): “OWL DL has a diﬃcult entailment problem, as inference in SHOIN ( D ) is of worst-case non-deterministic exponential time ( NExpTime ) complexity [36], and OWL DL should have the same complexity.”
Bridging the gap between OWL and relational databases (2007, background): “This, however, requires nominals in the DL language, which makes reasoning more difficult [25].”
Description Logics as Ontology Languages for the Semantic Web (2005, methodology): “However, according to the current state of the art, this procedures is more practical than the ExpTime automata-based procedure in [77].”
Reducing OWL Entailment to Description Logic Satisfability (2003, background): “As knowledge base satisfiability in )(&!$#&% is in EXPTIME [17] this means that entailment in OWL Lite can be computed in exponential time.”
OWL rules: A proposal and prototype implementation (2005, background): “18In some cases, the effects of transitive roles can be axiomatised in C2 [53].”
Conjunctive Query Answering for the Description Logic SHIQ (2007, methodology): “The proof is a straightforward extension of Lemma 6.19 by Tobies (2001).”
Combining answer set programming with description logics for the Semantic Web (2004, methodology): “We can show matching lower bounds by a generic reduction from Turing machinesM , exploiting the NEXP-hardness proof forACLQIO by Tobies (2001). The idea is to use a dl-atom to decide the result of the i-th oracle call made by a polynomial-time bounded M with access to a NEXP oracle, where the result”
Hypertableau Reasoning for Description Logics (2009, methodology): “For example, HT-clauses of the form R(x, y) ∧A(y)→ S(x, y) express a form of relativized role inclusions, and HT-clauses of the form R(x, y) ∧ S(y, x)→ U(x, y) ∨ T (y, x) capture safe role expressions (Tobies, 2001).”
OWL 2: The next step for OWL (2008, background): “OWL 1 DL Semantics The description logic SHOIN (D) has been extensively investigated in the literature, and its expressivity and computational properties are wellknown [36,19].”
Managing uncertainty and vagueness in description logics for the Semantic Web (2008, background): “Decision procedures are given in [143,57], and reasoning tools for SHOIN(D) are, e.”