Complexity Results and Practical Algorithms for Logics in Knowledge Representation
arXiv:cs/0106031
Abstract
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.
Ph.D. Thesis
References in corpus (1)
Cited by in corpus (20)
- The DL-Lite Family and Relations
- Hypertableau Reasoning for Description Logics
- Conjunctive Query Answering for the Description Logic SHIQ
- Reasoning with Very Expressive Fuzzy Description Logics
- Type-elimination-based reasoning for the description logic SHIQbs using decision diagrams and disjunctive datalog
- Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics
- ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
- The decision problem of modal product logics with a diagonal, and faulty counter machines
- Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
- Reasoning for ALCQ extended with a flexible meta-modelling hierarchy
- Extract ABox Modules for Efficient Ontology Querying
- ExpTime Tableaux with Global Caching for the Description Logic SHOQ
- A Rational Entailment for Expressive Description Logics via Description Logic Programs
- On two-variable guarded fragment logic with expressive local Presburger constraints
- Reasoning in Infinitely Valued G-IALCQ
- Open Answer Set Programming with Guarded Programs
- Conservative Extensions in Horn Description Logics with Inverse Roles
- Evidence-based lean logic profiles for conceptual data modelling languages
- On Decidability of Expressive Description Logics with Composition of Roles in Number Restrictions
- Combining Existential Rules and Description Logics (Extended Version)