Practical reasoning for very expressive description logics

DOI10.1093/jigpal/8.3.239zbMath0967.03026OpenAlexW2109003533MaRDI QIDQ4487262

Ian Horrocks, Stephan Tobies, Ulrike Sattler

Publication date: 28 August 2001

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.1064

zbMATH Keywords

modal logiccomputational experimentsautomated reasoningknowledge representationdecidabilitysatisfiabilitydescription logictableaux algorithm

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Logics of knowledge and belief (including belief change) (03B42) Knowledge representation (68T30) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35)

Related Items

Towards World Identification in Description Logics ⋮ Tractable approximate deduction for OWL ⋮ Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies ⋮ 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 ⋮ The two‐variable fragment with counting and equivalence ⋮ A universal approach to guarantee data privacy ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ PS\textsc{pace} tableau algorithms for acyclic modalized \({\mathcal{ALC}}\) ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited ⋮ Semantic characterization of rational closure: from propositional logic to description logics ⋮ Decidable Description Logics of Context with Rigid Roles ⋮ Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics ⋮ Deciding expressive description logics in the framework of resolution ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ Foundations of Onto-Relational Learning ⋮ Reasoning in description logics by a reduction to disjunctive datalog ⋮ Reasoning and Query Answering in Description Logics ⋮ Reasoning with Uncertain and Inconsistent OWL Ontologies ⋮ Algorithms for reasoning in very expressive description logics under infinitely valued Gödel semantics ⋮ Inductive Logic Programming in Databases: From <scp>Datalog</scp> to ⋮ A loop-free decision procedure for modal propositional logics K4, S4 and S5 ⋮ Unification in the Description Logic $\mathcal{EL}$ without the Top Concept ⋮ Automated Reasoning in $\mathcal{ALCQ}$ via SMT ⋮ Ontology Integration Using ε-Connections ⋮ Composing Modular Ontologies with Distributed Description Logics ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ A Correspondence between Temporal Description Logics ⋮ BDD-based decision procedures for the modal logic K ★ ⋮ Fuzzy description logics with general t-norms and datatypes ⋮ EXPtime tableaux for ALC ⋮ \({\mathcal E}\)-connections of abstract description systems ⋮ On the undecidability of logics with converse, nominals, recursion and counting