Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis

DOI10.1007/978-3-642-02959-2_6MaRDI QIDQ5191098zbMATH OpenOpenAlexFDO

Authors Roberto Sebastiani, Michele Vescovi

Publication date 28 July 2009

Published in Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL http://eprints.biblio.unitn.it/1576/1/014_v4_100309.pdf

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Recommendations

• Understanding the complexity of axiom pinpointing in lightweight description logics
• Pinpointing axioms in ontologies via ASP
• Complexity of Axiom Pinpointing in the DL-Lite Family of Description Logics
• Axiom Pinpointing in General Tableaux
• Axiom Pinpointing in General Tableaux

Cites work

• Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability
• Axiom Pinpointing in General Tableaux
• Lazy satisfiability modulo theories
• Theory and Applications of Satisfiability Testing

Cited in

(14)

• Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
• Complexity of Axiom Pinpointing in the DL-Lite Family of Description Logics
• Automated reasoning in \(\mathcal{ALCQ}\) via SMT
• Explanations for query answers under existential rules
• BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
• Ontology-Mediated Query Answering with Data-Tractable Description Logics
• Reasoning with ontologies
• Explaining reasoning results for description logic ontologies (invited paper)
• Understanding the complexity of axiom pinpointing in lightweight description logics
• Efficient reasoning for inconsistent Horn formulae
• The Bayesian ontology language \(\mathcal {BEL}\)
• Exploiting uncertainty for querying inconsistent description logics knowledge bases
• Classical algorithms for reasoning and explanation in description logics
• Enumerating justifications using resolution

Describes a project that uses

Uses Software

• Chaff
• MiniSat

This page was built for publication: Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5191098)