ASP-based Axiom Pinpointing for Description Logics

Axiom pinpointing is the task of identifying the axiomatic causes for a consequence to follow from an ontology. Different approaches have been proposed in the literature for finding one or all justifications: the subset-minimal subontologies that preserve a description logic consequence. We propose an approach that leverages the capabilities of answer set programming - through minimal unsatisfiable subset enumeration - for transparent axiom pinpointing. Our approach is general in that it allows one to seamlessly specify the ontology and the reasoning rules, thus being applicable to different logics without modification to the core method. We showcase this generality by introducing methods for ϵL and for Horn-ALC, and explaining how to apply it to other logics. A preliminary experiment shows the practicality of the approach.