# «The “Arbeitsberichte aus dem Fachbereich Informatik“comprise preliminary results which will usually be revised for subsequent publication. ...»

Semantically Guided Evolution of SHI ABoxes

Ulrich Furbach

Claudia Schon

Nr. 4/2013

Die Arbeitsberichte aus dem Fachbereich Informatik dienen der Darstellung

vorläufiger Ergebnisse, die in der Regel noch für spätere Veröffentlichungen

überarbeitet werden. Die Autoren sind deshalb für kritische Hinweise dankbar. Alle

Rechte vorbehalten, insbesondere die der Übersetzung, des Nachdruckes, des

Vortrags, der Entnahme von Abbildungen und Tabellen – auch bei nur

auszugsweiser Verwertung.

The “Arbeitsberichte aus dem Fachbereich Informatik“comprise preliminary results which will usually be revised for subsequent publication. Critical comments are appreciated by the authors. All rights reserved. No part of this report may be reproduced by any means or translated.

Arbeitsberichte des Fachbereichs Informatik ISSN (Print): 1864-0346 ISSN (Online): 1864-0850

**Herausgeber / Edited by:**

**Der Dekan:**

Prof. Dr. Grimm

**Die Professoren des Fachbereichs:**

Prof. Dr. Bátori, Prof. Dr. Burkhardt, Prof. Dr. Diller, Prof. Dr. Ebert, Prof. Dr. Frey, Prof. Dr. Furbach, Prof. Dr. Grimm, Prof. Dr. Hampe, Prof. Dr. Harbusch, jProf. Dr. Kilian, Prof. Dr. von Korflesch, Prof. Dr. Lämmel, Prof. Dr. Lautenbach, Prof. Dr. Müller, Prof. Dr. Oppermann, Prof. Dr. Paulus, Prof. Dr. Priese, Prof. Dr. Rosendahl, Prof. Dr. Schubert, Prof. Dr. Sofronie-Stokkermans, Prof. Dr.

Staab, Prof. Dr. Steigner, Prof. Dr. Strohmaier, Prof. Dr. Sure, Prof. Dr. Troitzsch, Prof. Dr. Wimmer, Prof. Dr. Zöbel Kontaktdaten der Verfasser Ulrich Furbach, Claudia Schon Institut für Informatik Fachbereich Informatik Universität Koblenz-Landau Universitätsstraße 1 D-56070 Koblenz E-Mail: uli@uni-koblenz.de, schon@uni-koblenz.de Semantically Guided Evolution of SHI ABoxes, Fachbereich Informatik Nr. 4/2013 Semantically Guided Evolution of SHI ABoxes Ulrich Furbach and Claudia Schon University of Koblenz-Landau, Germany, email:{uli,schon}@uni-koblenz.de

**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 equisatisﬁable knowledge base.

We use the result of this transformation to eﬃciently 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.

1 Introduction Description Logic knowledge bases consist of two parts: the TBox and the ABox.

The TBox contains the terminological knowledge and describes the world using so called concepts and roles. The ABox contains knowledge about individuals, stating to which concepts they belong to and via which roles they are connected. There is a considerable amount of work introducing update algorithms and mechanisms for Description Logic knowledge bases, which is of great interest to the Semantic Web community (see [10,15] for details). It is an indisputable fact, that in practice, knowledge bases are subject to frequent changes ([9]) and that even the construction of a knowledge base can be seen as an iterative process. On the other hand this abets inconsistencies in knowledge bases. Therefore the removal of inconsistencies from knowledge bases is of great interest as well ([12]). In this paper we are interested in an evolution of the knowledge base on the instance level. For this, we consider the TBox to be ﬁxed and consistent. We

**address three diﬀerent operations on the instance level of the knowledge base:**

deletion, insertion and repair. Instance-level deletion means the deletion of an instance assertion from the deductive closure or the knowledge base by removing as few assertions as possible. Instance-level insertion means adding an instance assertion to the knowledge base. In both cases it is important that the resulting knowledge base is consistent. For the task of ABox repair we are given an inconsistent knowledge base with consistent terminological part. The aim is to remove assertions from the ABox such that the resulting ABox together with the TBox is consistent. In all three tasks the changes performed should be minimal.

This corresponds to the goal of maintaining as much from the original ABox as possible. This view of minimal change corresponds to a formula based approach as opposed to a model based approach as investigated in [15]. In the model based

** Semantically Guided Evolution of SHI ABoxes, Fachbereich Informatik Nr. 4/2013**

approach the set of models of the knowledge base resulting form a change operation should be as close as possible to the set of models of the original knowledge base.

In [14], [7] and [5] instance level deletion, insertion and repair are addressed for DL-Lite knowledge bases. In [13] inconsistent DL-Lite ABoxes are considered.

[13] establishes inconsistency-tolerant semantics in order to be able to use those inconsistent ABoxes for query answering. [18] studies the complexity of reasoning under inconsistent-tolerant semantics. Algorithms for the calculation of minimal repair of DL-Lite ABoxes suggested in [13] test the satisﬁability of every single ABox assertion and every pair of ABox assertions w.r.t. the TBox. Since for DL-Lite the satisﬁability test is tractable, this approach is reasonable. However the ExpTime completeness of consistency testing of SHI ABoxes forbids such an approach. Further the algorithms suggested in [13] cannot be used for SHI

**ABoxes, because these algorithms exploit the following nice property of DL-Lite:**

as shown in [5], in DL-Lite the unsatisﬁability of an ABox w.r.t. a TBox is either caused by a single assertion or a pair of assertions. However in SHI an arbitrary number of assertions can cause unsatisﬁability w.r.t. a TBox.

Our approach is motivated by the observation that a consistent ABox can be seen as a (partial) model of the TBox, which can be used to guide the reasoning process, as proposed in [6]. In [3] this approach was used for model-based diagnosis, where an initial interpretation, which is very close to a model, was used to compute the deviations of a minimal model to this interpretation. In [1] the same approach was applied to view deletion in databases. In our case it is reasonable to assume, that the ABox is very close to a model of the TBox.

We use this assumption to semantically guide the construction of instance-based deletion, insertion and repair of ABoxes. As in [3], we gradually revise the assumption of the given ABox being a model for the TBox. This leads to a natural construction of minimal instance deletions/insertions and repairs of ABoxes.

The advantage of this approach is that there is no need to deﬁne new algorithms for updates and repair, which have to be proven correct. Instead we will use a static compilation of the knowledge base according to the update or repair requirement. We prove that this transformation preserves the necessary semantics. A theorem prover can be used to compute the necessary update and repair actions. A hypertableau-based theorem prover like E-KRHyper is very well suited for this task, because the transformation enables it to calculate only the deviation of the ABox. Since E-KRHyper has recently been extended to deal with knowledge bases given in SHIQ [4], we chose to use this theorem prover.

Our approach is related to axiom pinpointing. For a given consequence, axiom pinpointing is the task to ﬁnd the minimal subsets of the knowledge base under consideration, having this consequence. See [2] for details. In [11] laconic and precise justiﬁcations are introduced. Given an ontology and an entailment, a justiﬁcation is a minimal subset of that ontology such that the entailment still holds in the subset. Roughly spoken, laconic justiﬁcations are not allowed to contain superﬂuous parts. In contrast to axiom pinpointing and justiﬁcations, we calculate subsets of the ABox and not of the whole knowledge base. In [19] inco

<

** Semantically Guided Evolution of SHI ABoxes, Fachbereich Informatik Nr. 4/2013**

herent TBoxes, i.e. TBoxes containing an unsatisﬁable concept, are investigated.

[10] considers so called syntactic ABbox updates. Similar to our approach, assertions are added to or removed from the ABox. In contrast to our approach, it is neither guaranteed that the removed assertion is not contained in the deductive closure nor that the result of adding the assertion is consistent.

In Section 2 we give both syntax and semantics of the Description Logic SHI. In addition to that, we introduce the notion of DL-clauses as used in [16].

In Section 3 we give deﬁnitions for instance-level deletion, insertion and repair.

Section 4 introduces the so called K∗ -transformation which in Section 5 is used to calculate the instance-level deletion, insertion and repair. The K∗ -transformation is implemented and in Section 6 we present ﬁrst experimental results.

** SHI and DL-Clauses **

First, we introduce the Description Logic SHI. Given a set of atomic roles NR, the set of roles is deﬁned as NR ∪ {R− | R ∈ NR }, where R− denotes the inverse role corresponding to the atomic role R. Let further Inv be a function on the set of roles that computes the inverse of a role, with Inv(R) = R− and Inv(R− ) = R. A role inclusion axiom is an expression of the form R S, where R and S are atomic or inverse roles. A transitivity axiom is of the form Trans(S) for S an atomic or inverse role. An RBox R is a ﬁnite set of role inclusion axioms and transitivity axioms. ∗ denotes the reﬂexive, transitive closure of over {R S, Inv(R) Inv(S) | R S ∈ R}. A role R is transitive in R if there exists a role S such that S ∗ R, R ∗ S, and either Trans(S) ∈ R or Trans(Inv(S)) ∈ R. If no transitive role S with S ∗ R exists, R is called simple.

Let NC be the set of atomic concepts. The set of concepts is then deﬁned as the smallest set containing, ⊥, A, ¬C, C D, C D, ∃R.C and ∀R.C for A ∈ NC, C and D concepts and R a role.

A general concept inclusion (GCI) is of the form C D, and a TBox T is a ﬁnite set of GCIs.

Given a set of individuals NI, an ABox A is a ﬁnite set of assertions of the form A(a) and R(a, b), with A an atomic concept, R an atomic role and a, b individuals from NI. Note that in our setting, the ABox is only allowed to contain assertions about the belonging of individuals to atomic concepts and roles.

A knowledge base K is a triple (R, T, A) with signature Σ = (NC, NR, NI ).

The tuple I = (·I, ∆I ) is an interpretation for K iﬀ ∆I is a nonempty set and ·I assigns an element aI ∈ ∆I to each individual a, a set AI ⊆ ∆I to each atomic concept A, and a relation RI ⊆ ∆I × ∆I to each atomic role R. ·I then assigns values to more complex concepts and roles as described in Table 1. I is a model of K (I |= K) if it satisﬁes all axioms and assertions in R, T and A as shown in Table 1. A TBox T is called consistent, if there is an interpretation satisfying all axioms in T. A concept C is called satisﬁable w.r.t. R and T iﬀ there exists a model I of R and T with C I = ∅.

Semantically Guided Evolution of SHI ABoxes, Fachbereich Informatik Nr. 4/2013

** Table 1. Model-theoretic semantics of SHI.**

R+ is the transitive closure of R.

In the sequel we adapt the notion of DL-clauses introduced in [16] to the Description Logic SHI. These DL-clauses allow to use existent theorem provers which are based on the hypertableau calculus to compute models or to decide satisﬁability. DL-clauses are universally quantiﬁed implications of the form

**Vj ← Ui :**

Deﬁnition 1. ([16]) An atom is of the form B(s), R(s, t), ∃R.B(s) or ∃R.¬B(s) for B an atomic concept and s and t individuals or variables. An atom not containing any variables is called a ground atom. A DL-clause is of the form V1 ∨... ∨ Vn ← U1 ∧... ∧ Um with Vi atoms and Uj atoms of the form B(s) or R(s, t) and m ≥ 0 and n ≥ 0. If n = 0, we denote the left hand side (head) of the DL-clause by ⊥. If m = 0, we denote the right hand side (body) of the DL-clause by.