Abstraction Refinement for Ontology Materialization

We present a new procedure for ontology materialization (computing all entailed instances of every atomic concept) in which reasoning over a large ABox is reduced to reasoning over a smaller “abstract” ABox. The abstract ABoxisobtainedastheresultofafixed-pointcomputationinvolvingtwostages: 1) abstraction: partition the individuals into equivalence classes based on told information and use one representative individual per equivalence class, and 2) refinement: iteratively split (refine) the equivalence classes, when new assertions are derived that distinguish individuals within the same class. We prove that the method Is complete for Horn ALCHOI ontologies, that is, all entailed instances will be derived once the fixed-point is reached. We implement the procedure in a new database-backed reasoning system and evaluate it empirically on existing ontologieswithlargeABoxes.WedemonstratethattheobtainedabstractABoxes are significantly smaller than the original ones and can be computed with few refinement steps.