Semantically Guided Evolution of $\mathcal{SHI}$ ABoxes

TL;DR

This paper introduces a semantically guided method for evolving SHI ABoxes by transforming them into an interpretation close to a model, enabling efficient deletion, insertion, and repair of assertions using a theorem prover.

Contribution

It presents a novel compilation-based approach for the evolution of SHI ABoxes, improving efficiency in managing assertions and ensuring consistency.

Findings

Efficient deletion of assertions from ABoxes.

Effective insertion and repair of ABoxes.

Use of E-KRHyper theorem prover for computation.

Abstract

This paper presents a method for the evolution of SHI ABoxes which is based on a compilation technique of the knowledge base. For this the ABox is regarded as an interpretation of the TBox which is close to a model. It is shown, that the ABox can be used for a semantically guided transformation resulting in an equisatisfiable knowledge base. We use the result of this transformation to efficiently delete assertions from the ABox. Furthermore, insertion of assertions as well as repair of inconsistent ABoxes is addressed. For the computation of the necessary actions for deletion, insertion and repair, the E-KRHyper theorem prover is used.