Beyond Asserted Axioms: Fine-Grain Justifications for OWL-DL Entailments
Aditya Kalyanpur, Bijan Parsia, Bernardo Cuenca Grau · 2006
The Ontology Engineering community widely agrees on the importance of helping the user understand the output of a DL reasoner. The most recent approaches to the problem [4] [3] are based on the notion of a Minimal Unsatisfiability Preserving Sub-TBoxes (MUPS). Roughly, a MUPS for an atomic concept A is a minimal fragment T ′ ⊆ T of a TBox T in which A is unsatisfiable. For example, given the TBox: 1: A ⊔ C ⊑ B ⊓ ∃R.D ⊓ E ⊓ ¬B, 2: C ⊑ F ⊔ ≥ 1.R