Deciding expressive description logics in the framework of resolution

DOI10.1016/j.ic.2007.11.006zbMath1146.68456OpenAlexW2119177810MaRDI QIDQ924723

Boris Motik, Ullrich Hustadt, Ulrike Sattler

Publication date: 19 May 2008

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:a2969f65-bf29-487f-9d71-472f0238015d

zbMATH Keywords

description logicsbasic superpositionresolution decision procedure

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (10)

Tableau reasoning for description logics and its extension to probabilities ⋮ Unnamed Item ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ First-Order Resolution Methods for Modal Logics ⋮ On the finite controllability of conjunctive query answering in databases under open-world assumption ⋮ Incremental classification of description logics ontologies ⋮ Top-\(k\) retrieval for ontology mediated access to relational databases ⋮ Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach ⋮ Prolog Based Description Logic Reasoning

Uses Software

• Racer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A structure-preserving clause form translation
• Propositional dynamic logic of regular programs
• Modal languages and bounded fragments of predicate logic
• Resolution methods for the decision problem
• EXPtime tableaux for ALC
• Loosely guarded fragment of first-order logic has the finite model property
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• Complexity of the two-variable fragment with counting quantifiers
• Splitting through New Proposition Symbols
• Ordered chaining calculi for first-order theories of transitive relations
• On the efficiency of subsumption algorithms
• Resolution Strategies as Decision Procedures
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Practical reasoning for very expressive description logics
• Resolution-based methods for modal logics
• Complexity Results for First-Order Two-Variable Logic with Counting
• Automated Reasoning
• A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
• Logic for Programming, Artificial Intelligence, and Reasoning
• Automated Deduction – CADE-19

This page was built for publication: Deciding expressive description logics in the framework of resolution