Abstract
We propose a novel approach to axiom pinpointing based on a reduction to the SAT task of minimal unsatisfiable subformula enumeration, allowing highly optimized algorithms and data structures developed for SAT solving in the last two decades to be used in this problem. Exploiting the specific properties of axiom pinpointing, we apply further optimizations resulting in considerable runtime improvements of several orders of magnitude. Our ideas are implemented in SATPin, a system capable of performing axiom pinpointing in large biomedical ontologies faster than other existing tools. While our paper focuses on a slight extension of EL, the presented approach directly generalizes to all ontology languages for which consequence-based reasoning methods are available.