Almost Certain Termination for $$\mathcal {ALC}$$ Weakening

Concept refinement operators have been introduced to describe and compute generalisations and specialisations of concepts, with, amongst others, applications in concept learning and ontology repair through axiom weakening. We here provide a probabilistic proof of almost-certain termination for iterated refinements, thus for an axiom weakening procedure for the fine-grained repair of ALC ontologies. We determine the computational complexity of refinement membership, and discuss performance aspects of a prototypical implementation, verifying that almost-certain termination means actual termination in practice.