Link keys allow for generating links across data sets expressed in different ontologies. But they can also be thought of as axioms in a description logic. As such, they can contribute to infer ABox axioms, such as links, or terminological axioms and other link keys. Yet, no reasoning support exists for link keys. Here we extend the tableau method designed for ALC to take link keys into account. We show how this extension enables combining link keys with classical terminological reasoning with and without ABox and TBox and generate non trivial link keys.
Part of the added value of linked data lies in the links between entities denoting the same individual in data sets issued by different sources as it allows for making inferences across data sets. For instance, links may identify the same books and articles in different bibliographical data sources. So finding the manifestation of the same entity across several data sets is an important task of linked data.
One way of identifying entities is to use link keys which generalise keys usually
found in data bases to the case of different data sets. A link key [
fhauteur; creatori; htitre; titleig linkkey hLivre; Booki stating that whenever an instance of the class Livre has the same values for properties auteur and titre as an instance of class Book has for properties creator and title, then they denote the same entity. Such keys are slightly more complex than those of databases because, in RDF, properties are not necessarily functional (they may have several values) and their values may be other objects.
One further difference is that RDF data, together with ontologies expressed in the OWL or RDFS languages, are logic theories. In such a context, a link key is a statement as any other logical statement. As such, it may contribute deducing other statements. Indeed, the above link key entails:
fhauteur; creatori; htitre; titlei; héditeur; publisherig linkkey hLivre; Booki or
fhauteur; creatori; htitre; titleig linkkey hLivre; Noveli whenever Novel is subsumed by Book.
Hence, it is possible to reason on link keys in different ways: – deducing link keys from OWL statements, – deducing link keys from link keys, – deducing OWL statements from link keys.
Our goal is to study reasoning procedures for link keys. For that purpose, we define a preliminary extension of the tableau method for ALC dealing with link keys and we provide examples for each of the inference types above.
In the following, we first discuss related work (§2) and define more precisely the problem (§3). Then we present a tableau extensions allowing for ABox reasoning with link keys (§4) and for reducing link key inference to that ABox reasoning (§5). 2
Data interlinking is a very active area [
This work belongs to the logic-based approach. It uses a generalisation of keys in relational databases, called link keys, for expressing the condition for identifying resources across different ontologies. Keys in databases indicate that a set of properties uniquely identifies individuals. Relational properties are functional (have only one value) and concrete (the value comes from a data type).
RDF data differ from relational data in their properties, which are not functional,
and their values, which may be resources. Hence, keys have been generalised to cope
with this problem [
Keys may be introduced in description logics either as global constraints in a
specific KBox [7; 10], or as a new concept constructor [
Keys identify objects within a single data source with a single schema. Link keys
have been designed for coping with heterogeneous data sources [
Link keys raise two distinct problems: the first one is to extract link keys from data
sets [
Here we tackle a third problem (not unrelated to the second one): reasoning with link keys, i.e., infering links, ontological and assertional statements as well as other link keys. We define this problem more precisely below. 3
Data interlinking is the process of generating links across data sets that can help finding
equivalent resources representing the same entity on the web for linked data. These
links are usually owl:sameAs statements between two resources across different RDF
data sets. We will consider that these data sets are description logic knowledge bases
(KB = hT; Ai) made of a TBox T and an ABox A. Description logics [
We decided to extend the tableau method used for checking entailment in the ALC family of description logics for several reasons: – ALC is a subset of OWL; – The tableau method is extensible, so it is possible to add rules for dealing with more expressive logics. We could have started with procedure specific to less expressive logics (E L, DL-Lite, OWL-RL), but we could barely extend them.
An ALC TBox is a set of general concept inclusion axioms of the form C v C0. Concepts are defined by:
C = Aj?j>jC u C0jC t C0j:Cj8R:Cj9R:C and roles are simply atomic roles (R = r).
The ABox is made of assertions of the form C(a) and r(a; b). We will use two specific statements a = b and 6= b which are interpreted as usual. These two predicates are the transcription of owl:sameAs and owl:differentFrom.
The semantics of such logics is defined by interpretations I = h I ; I i such that I is a non empty set and I is a function such that: aI 2 I , CI I , and rI I I with: (:C)I =
I n CI (C u C0)I = CI \ C0I (C t C0)I = CI [ C0I ?I = ? >I =
I (8r:C)I = f 2 (9r:C)I = f 2
I j8 0; h ; 0i 2 rI )
0 2 CI g I j9 0 2 CI ; h ; 0i 2 rI g An interpretation satisfies an axiom (denoted by I j= ) in the following conditions: I j= C(a) iff aI 2 CI
I j= a = b iff aI = bI I j= C v C0 iff CI
C0I
I j= r(a; b) iff haI ; bI i 2 rI I j= a 6= b iff aI 6= bI
A model of a knowledge base KB is an interpretation satisfying all its axioms and an assertion is entailed by a knowledge base (denoted by KB j= ) if it is satisfied by all the models of KB.
We extend description logics with a KBox K which contains link keys instead of simple keys. The KBox is a set of link keys: fhpi; qiigi2I linkkeyiwn hC; Di with C and D two classes coming from different data sets and pi and qi roles, from the data sets of C and D respectively, indexed by a finite set of indices I. Since we concentrate specifically on weak in-link keys, we use the keyword linkkeyiwn.
The semantics of description logics is extended to cover link keys: An interpretation I satisfies (fhpi; qiigi2I linkkeyiwn hC; Di) iff, for any 2 CI and 2 DI , ^(9zi 2 i2I
I ; h ; zii 2 piI ^ h ; zii 2 qiI ) ) = Any key fpigi2I keyF or C is equivalent to the link key fhpi; piigi2I linkkey hC; Ci. In this paper, we only consider hierarchical KBoxes, i.e., KBoxes in which there cannot be circular dependencies between link keys.
It is possible, to establish entailment rules for link keys considered as assertions: fhpi; qiigi2I linkkeyiwn hC; Di j= fhpi; qiigi2I[J linkkeyiwn hC; Di fhpi; qiigi2I linkkeyiwn hC; Di; C0 v C j= fhpi; qiigi2I linkkeyiwn hC0; Di fhpi; qiigi2I linkkeyiwn hC t C0; Di j= fhpi; qiigi2I linkkeyiwn hC; D u D0i Proving all such rules one by one is tedious, so an inference procedure for doing this would be useful. 4
The basic way of applying link keys is to start with two datasets A and A0 described by two ontologies T and T 0 and a set K of link keys across these ontologies and to generate links, i.e., statements of the form a = b with a and b from each data set.
We consider this problem more widely as that of reasoning in a knowledge base1 KB = hT [ T 0; K; A [ A0i. We will consider more precisely the decision problem of checking the entailment of any ABox axiom from such a knowledge base.
INSTANCE: – A knowledge base KB = hT; K; Ai – An ABox assertion .
QUESTION: Does KB j= ? 4.1 The tableau method is the classical technique to reason with ALC. Explaining the method is out of the scope of this paper (see [4; 5]). To summarise, this method attempts to find a model of a knowledge base KB = hT; Ai in negation normal form. 1 We assume no unwanted name conflicts, i.e., the same name or URI in both data sets must have the same interpretation.
For that purpose, it starts with a representation of the ABox A and applies rules (see
Appendix) guided by T until no rule is applicable [
In order to tackle the ABox Axiom entailment problem within the tableau method we introduce the Linkkey-rule:
Condition: fhpi; qiigi2I linkkeyiwn hC; Di 2 K, 9x; y, not blocked, such that C 2 L(x), D 2 L(y), and 8i 2 I, 9zi, such that pi 2 L(hx; zii) and qi 2 L(hy; zii) Action: L(x) := L(x) [ L(y)
Replace y by x in all edges starting from or ending at y
Suppress node y
This rule is sound, i.e., any model has to satisfy it, as it strictly follows the semantics
of link keys. It generalises rule T14 in [
The use of this rule for checking a link a = b can be illustrated on the straightforward Example 1: For proving the entailment of a = b, we proceed by refutation, i.e., we prove that it is not possible to create a model satisfying the antecedents and the negation of the consequence (a 6= b). A representation of such a model is created and the rules are applied on it. The Linkkey-rule merges the two nodes satisfying the link key condition which makes them fall under the 6=-clash.
Example 1 (Simple link generation). fCg
fDg p 6= 6= fg
q p; q fC; Dg fg Linkkey-rule
hp; qi linkkeyiwn hC; Di; C(a); D(b); p(a; v); q(b; v) j= a = b?
A = fC(a); D(b); p(a; v); q(b; v); a 6= bg Example 2 shows the use of these rules for chaining the use of two link keys. However, it may be used in any ABox reasoning development.
Example 2 (Chaining link generation). fCg 6= fDg fEg fCg p q p 6= r
fF g s fg
Linkkey-rule 6=
r fE; F g q; s fg
fDg Linkkey-rule fC; Dg p; r fE; F g q; s fg 6=-clash
hp; ri linkkeyiwn hC; Di, hq; si linkkeyiwn hE; F i, C(a); p(a; c); E(c); q(c; v); D(b); r(b; d); F (d); s(d; v) j= a = b?
K = fhp; ri linkkeyiwn hC; Di; hq; si linkkeyiwn hE; F ig A = fC(a); p(a; c); E(c); q(c; v);
D(b); r(b; d); F (d); s(d; v); a 6= bg
Solving the ABox entailment problem may not be the most efficient way to generate links from RDF especially if the size of the considered ABox is very large. A more interesting use of such reasoning is for checking link key entailment. 5
The link key entailment problem aims at checking if a link key is entailed by a knowledge base. Because this resorts to the terminological level, i.e., without regard to a particular ABox, it is defined only on a knowledge base made of a TBox and a KBox. Indeed, some link keys may be entailed from terminological axioms, some others from other link keys of a mix of this.
INSTANCE: – A knowledge base KB = hT; Ki – A link key .
QUESTION: Does KB j= ? 5.1
The tableau method cannot be directly used for refuting a link key axiom because there is no negation for link keys: a link key is an axiom of our logic, the negation of a link key is not.
Other authors have considered expressing keys as simple concept constructors [
C v key(fpigi2I )
hC; Di v linkkeyiwn (fhpi; qiigi2I ) such statements would solve half of the problem as it is possible to negate the subsumption statements, but this would lead to strange statements as they concern pairs of classes. They would also be stronger than, and not equivalent to, our actual link key statements.
Adding the negation of a link key to the logic is another solution to this problem. However, since its only use would be for the decision procedure, we preferred to avoid this solution.
We choose a simpler method given that our goal is simply to have negated link keys as the statement to refute: we use a set of ABox statements as witness of the unsatisfiability of a link key. This set is given by the function :
(fhpi; qiigi2I linkkeyiwn hC; Di) = fC(x); D(y); x 6= yg [ fpi(x; vi); qi(y; vi)gi2I Checking the entailment of a link key by a knowledge base h?; T; Ki can be reduced to checking the satisfiability of the knowledge base KB = hT; K; ( )i. Any model in which the link key is not valid satisfies ( ). Hence, if KB is satisfiable, then is not entailed.
Example 3 (Link key inference from other link keys and TBox).
Problem: hp; qi linkkeyiwn hC; Di; C0 v C j= hp; qi linkkeyiwn hC0; Di?
T = fC0 v Cg K = fhp; qi linkkeyiwn hC; Dig
A = fC0(a); D(b); p(a; v); q(b; v); a 6= bg fC0; :C0; :C0 t Cg
6= p fDg fC0; C; :C0 t Cg fDg fC0; :C0 t Cg p p fC0g q fg 6= q q fg fDg fDg
For instance, one of the example given in Section 3 is a link key entailed from another link key and terminological axioms. Example 3 shows how this is performed without introducing any new rule or clash in the tableau procedure.
This shows the importance of being able to reason with the ABox, since the refutation of the KB is mostly carried out by reasoning in the ABox even if the problem does not have an ABox. It also shows that link key rules can be adequately interleaved with ALC rules. This suggests that extensions can properly work in the same way. Some other link keys may only be entailed by terminological axioms. We illustrate this by the counter-intuitive Example 4. This inference is of little use, but it shows that the method indeed proves this valid link key.
Example 4 (Link key inference from TBox alone).
C v 8p:? j= hp; qi linkkeyiwn hC; Di ?
T = fC v 8p:?g K = fg A = fC(a); p(a; v); D(b); q(b; v); a 6= bg fCg p p fC; :C t 8p:?g 6= 6= q q fg fDg fDg fDg fDg fg 8-rule f?g
It is noteworthy that Example 4 does not use the Linkkey-rule; it only relies on the encoding of the problem and classical ALC reasoning.
The use of the tableau method allows both to check inference rules and to determine minimal logics in which they hold. Example 4 shows that the given entailment holds in any description logic, with ALC-style models, which accepts subsumption axioms (v), universal quantification (8) and the empty concept (?). 6
Link keys are very useful for generating links from data sources, but they can be studied independently from data sources as axioms. In order to prove when a particular knowledge base, eventually with link keys, entails a particular link key, we proposed extensions of the tableau method for ALC enabling the interpretation of link keys. We showed that these extensions also allow for checking link key entailment.
We considered the tableau method because it is well-adapted to ALC and thus to OWL as a whole. Weaker fragments of OWL (E L, DL-Lite, OWL-RL) are supported efficiently by other reasoning methods. It would be interesting to investigate the opportunity to reason with and about link keys in this context.
This work is preliminary and many developments may be undertaken from here. We discuss a few of them.
First, we need to determine the properties of the proposed extension. We have yet no formal proof to offer, but basic arguments for these. Although correctness of rules and clash independently seems to be straightforward, proving the completeness of the designed procedure with various logics must be considered. Termination can be guaranteed with a blocking mechanisms and because no rule erases any other rule condition (the Linkkey-rule merges nodes, but preserves the constraints on these nodes). Finally, the current link key rule should not increase the complexity of existing tableau methods since the rule does not introduce branches. The Linkkey-rule may offer new development opportunities by merging nodes but (i) this process is bounded, and (ii) new tableau developments should not go beyond current complexity.
Then, we want to implement these extensions. This would allow us to check automatically the link key inference rules that we designed. It would also be interesting, in a further step, to develop techniques to generate (specific) entailed assertions in a forward deduction style.
Finally, it would be worth considering the other type of link key conditions (eqlink keys). However, this may not be easy to integrate with the open world aspect of description logic semantics.
A ALC+Linkkey rules We provide the full set of rules for helping the reader to read the examples.
u-rule
Condition: C u D 2 L(x), x is not blocked; fC;Dg 6 L(x) Action: L(x) := L(x) [ fC;Dg t-rule
Condition: C t D 2 L(x), x is not blocked; C 62 L(x), D 62 L(x) Action: L(x) := L(x) [ fCg, or L(x) := L(x) [ fDg
Condition: 9r:C 2 L(x), x is not blocked; 6 9y;r(x;y) ^ C 2 L(y) Action: create a new node y with L(hx;yi) = frg and L(y) = fCg
Condition: 8r:C 2 L(x), x is not blocked; 9y;r(x;y) ^ C 62 L(y) Action: L(y) := L(y) [ fCg v-rule
Condition: C v D 2 T, x is not blocked, :C t D 2= L(x) Action: L(x) := L(x) [ f:C t Dg
Condition: fhpi;qiigi2I linkkeyiwn hC;Di 2 K, 9x;y, not blocked, such that C 2 L(x), D 2 L(y), and 8i 2 I, 9zi, such that pi 2 L(hx;zii) and qi 2 L(hy;zii) Action: L(x) := L(x) [ L(y)
Replace y by x in all edges starting from or ending at y Suppress node y
:-clash : 9x;fC;:Cg L(x) ?-clash : 9x;? 2 L(x) 6=-clash : 9hx;xi;6=2 L(hx;xi)