The recent quest for tractable logic-based languages arising from the field of bio-medical ontologies has raised a lot of attention on lightweight (i.e. less expressive but tractable) description logics, εL like and its family. To this extent, automated reasoning techniques in these logics have been developed for computing not only concept subsumptions, but also to pinpoint the set of axioms causing each subsumption. In this paper we build on previous work from the literature and we propose and investigate a simple and novel approach for axiom pinpointing for the logic εL . The idea is to encode the classification of an ontology into a Horn propositional formula, and to exploit the power of Boolean Constraint Propagation and Conflict Analysis from modern SAT solvers to compute concept subsumptions and to perform axiom pinpointing. A preliminary empirical evaluation confirms the potential of the approach. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Sebastiani, R., & Vescovi, M. (2009). Axiom pinpointing in lightweight description logics via horn-sat encoding and conflict analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5663 LNAI, pp. 84–99). https://doi.org/10.1007/978-3-642-02959-2_6
Mendeley helps you to discover research relevant for your work.