Practical reasoning for very expressive description logics
Description Logics provide a formalization of knowledge representation languages. The formalization is based on the notion of concept (unary predicate) and role (binary predicate). Complex concepts and roles are constructed from atomic ones using some constructors. The language of a description logic, \({\mathcal A}{\mathcal L}{\mathcal C}\), is extended with transitive and inverse roles, role hierarchies, and functional restrictions. There is a relationship of this logic to the propositional (multi)modal logic \({\mathbf S4_{(m)}}\). An algorithm deciding the satisfiability of the extended language is presented. The fact that the algorithm deals only with transitive roles, instead of transitive closure, leads to a lower degree of indeterminism, and experiments indicate that the algorithm is well-suited for implementation. It is shown that the \({\mathcal A}{\mathcal L}{\mathcal C}\) extended with transitive and inverse roles is still in PSPACE. The algorithm uses an enhanced blocking technique. The technique seems to be useful from the viewpoint of efficient implementations of more expressive description logics. The limits of decidability for the considered family of description logics is investigated. It is shown that relaxing the constraints placed on the kinds of roles used in number restrictions leads to undecidability of all inference problems. Some optimization techniques are studied. The techniques are crucial in obtaining implementations of the decision procedures. Computational experiments with the implemented system are described in the concluding section of the paper.
- Practical reasoning for expressive description logics
- Reasoning with expressive description logics: Theory and practice
- Reasoning in expressive description logics
- scientific article; zbMATH DE number 1531967
- Reasoning in Description Logics: Basics, Extensions, and Relatives
- Reasoning and query answering in description logics
- Description Logics
- A logical semantics for description logic programs
- Fuzzy description logics with general t-norms and datatypes
- EXPtime tableaux for ALC
- Tractable reasoning using logic programs with intensional concepts
- A loop-free decision procedure for modal propositional logics K4, S4 and S5
- Blocking and other enhancements for bottom-up model generation methods
- Rational closure for all description logics
- Computing the least common subsumer w.r.t. a background terminology
- Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor
- A universal approach to guarantee data privacy
- Reasoning in description logics by a reduction to disjunctive datalog
- On the relative expressiveness of description logics and predicate logics
- Tableau algorithms for description logics
- Tractable approximate deduction for OWL
- Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies
- Beth definability in expressive description logics
- Decidable description logics of context with rigid roles
- Reasoning in expressive description logics under infinitely valued Gödel semantics
- The two-variable fragment with counting and equivalence
- How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- PS\textsc{pace} tableau algorithms for acyclic modalized \({\mathcal{ALC}}\)
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- Foundations of Onto-Relational Learning
- Inductive logic programming in databases: from Datalog to \(\mathcal {DL} + \text{LOG}^{\neg \vee}\)
- Ontology Integration Using ε-Connections
- Composing Modular Ontologies with Distributed Description Logics
- A Correspondence between Temporal Description Logics
- Second-order reasoning in description logics
- BDD-based decision procedures for the modal logic K ★
- scientific article; zbMATH DE number 67500 (Why is no real title available?)
- scientific article; zbMATH DE number 67503 (Why is no real title available?)
- Optimising propositional modal satisfiability for description logic subsumption
- A description logic with transitive and inverse roles and role hierarchies
- scientific article; zbMATH DE number 1735887 (Why is no real title available?)
- scientific article; zbMATH DE number 1149436 (Why is no real title available?)
- On expressive description logics with composition of roles in number restrictions
- Issues of decidability for description logics in the framework of resolution
- Description logics with inverse roles, functional restrictions, and n-ary relations
- Exploiting pseudo models for TBox and ABox reasoning in expressive description logics
- Reasoning and query answering in description logics
- Reasoning with uncertain and inconsistent OWL ontologies
- Practical reasoning for expressive description logics
- scientific article; zbMATH DE number 1400210 (Why is no real title available?)
- Algorithms for reasoning in very expressive description logics under infinitely valued Gödel semantics
- Unification in the description logic \(\mathcal{EL}\) without the top concept
- Automated reasoning in \(\mathcal{ALCQ}\) via SMT
- Reasoning about Multiple Aspects in Rational Closure for DLs
- Rough Pragmatic Description Logic
- LINEAR TIME IN HYPERSEQUENT FRAMEWORK
- A proof theory for description logics.
- Using tableau to decide description logics with full role negation and identity
- Towards World Identification in Description Logics
- OUP accepted manuscript
- Foundations of Information and Knowledge Systems
- An overview of tableau algorithms for description logics
- Semantic web
- Concrete domains meet expressive cardinality restrictions in description logics
- \({\mathcal E}\)-connections of abstract description systems
- On the undecidability of logics with converse, nominals, recursion and counting
- Semantic characterization of rational closure: from propositional logic to description logics
- Deciding expressive description logics in the framework of resolution
- Automata can show PSpace results for description logics
This page was built for publication: Practical reasoning for very expressive description logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4487262)
