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

DOI10.1007/978-3-642-02959-2_6zbMath1250.68246OpenAlexW1540668801MaRDI QIDQ5191098

Michele Vescovi, Roberto Sebastiani

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

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

Related Items (7)

The Bayesian ontology language \(\mathcal {BEL}\) ⋮ Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing ⋮ Understanding the complexity of axiom pinpointing in lightweight description logics ⋮ Ontology-Mediated Query Answering with Data-Tractable Description Logics ⋮ Automated Reasoning in $\mathcal{ALCQ}$ via SMT ⋮ BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies ⋮ Efficient Reasoning for Inconsistent Horn Formulae

Uses Software

• MiniSat
• Chaff

Cites Work

• Unnamed Item
• Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
• Theory and Applications of Satisfiability Testing
• Axiom Pinpointing in General Tableaux

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