Whereof One Cannot Explain, Thereof One Must Invent:Definitorial Abduction in AℒCℐ via Strong Forgetting

Signature-based abduction in description logics (DLs) seeks the weakest sufficient hypothesis, formulated over a designated signature, that together with a background ontology explains a given observation. When no informative hypothesis is expressible within the allowed signature, existing methods based on weak forgetting inevitably produce rationally unacceptable results such as A ⊆ ⊥. We formalize definitorial abduction, which returns a pair 〈ℋ, χ 〉 of a hypothesis ℋ respecting the signature restriction, and a definitorial extension χ introducing fresh concept names anchored to the original ontology through conservative definitorial axioms. Standard signature-based abduction is the special case when χ = �

. To realize definitorial abduction, we develop a sound, complete, and terminating Ackermann-style strong forgetting calculus for acyclic AℒCℐ ontologies. The key technical contribution is the ∃-surfacing rule, which resolves a fundamental incompleteness of the Ackermann framework when a concept name to be eliminated occurs under existential restrictions in both polarities. The unnamed concept names that this rule introduces are precisely the fresh symbols that definitorial abduction exploits. An evaluation of the approach on 547 real-world ontologies shows: 20–29% of instances require unnamed concept names, confirming the practical prevalence of cases where standard abduction degenerates; our prototype is 36% faster on average than the only existing baseline.