# zbMATH — the first resource for mathematics

Semantically guided evolution of $$\mathcal{SHI}$$ ABoxes. (English) Zbl 1401.68315
Galmiche, Didier (ed.) et al., Automated reasoning with analytic tableaux and related methods. 22nd international conference, TABLEAUX 2013, Nancy, France, September 16–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40536-5/pbk). Lecture Notes in Computer Science 8123. Lecture Notes in Artificial Intelligence, 134-148 (2013).
Summary: This paper presents a method for the evolution of $$\mathcal{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.
For the entire collection see [Zbl 1272.68020].
##### MSC:
 68T30 Knowledge representation 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68T27 Logic in artificial intelligence
E-KRHyper
Full Text: