The problem of reasoning over ontologies written in Description Logic (DL) [
This paper tries to tackle this issue by adapting a reasoning method that makes a
parsimonious usage of memory. The inference system proposed here is based on the
connection calculus [
The rest of the article is organized as follows. Section 2 defines one of the most
basic description logic languages, ALC (Attributive Concept Language with
Complements) [
An ontology or knowledge base in ALC is a set of axioms defined over the triple
( , , ) [
NC contains concepts (like Bird, Animal, etc) as well as other concept definitions as follows. If r is a role (r ∈ ) and C and D are concepts (C, D ∈ 0T18T) then the following definitions belong to the set of ALC concepts: (i) C ⊓ D (the intersection of two concepts); (ii) C ⊔ D (the union of two concepts); (iii) ¬0TC (the complement of a concept); (iv) ∀r.C (the universal restriction of a concept by a role); and (v) ∃r.C (the existential restriction of a concept by a role). Note that, in the definitions above, C and D can be inductively replaced by other complex concept expressions.
There are two axiom types allowed in ALC: (i) Assertional axioms, which are concept assertions C(a), or role assertions R(a,b), where C ∈ NC , r ∈ NR , a,b ∈ NO and (ii) Terminological axioms, composed of any finite set of GCIs (general concept inclusion) in one of the forms C ⊑ D or C ≡ D, the latter meaning C ⊑ D and D ⊑ C, C and D being concepts. An ontology or knowledge base (KB) is referred to as a pair (T,A), where T is the terminological box (or Tbox) which stores terminological axioms, and A is the assertional box (ABox) which stores assertional axioms. T may contain cycles, in case at least an axiom of the form C ⊑ D, D can be expanded to an expression that contains C.
There are two major ways of defining ALC semantics. The most frequently used
one relies on the definitions of interpretation, model, fixpoints, etc, over a domain ∆
[
Next, the ALC disjunctive normal form used by the inference system is presented.
Definition 1 (ALC disjunctive normal form (ALC DNF), clause). An ALC DNF formula is a disjunction of conjunctions, in the form C1 ∨ … ∨ Cn, where each Ci is a clause. Clauses are conjunctions of ALC predicates (ALC concepts or relations, instantiated or not), like L1 ∧ … ∧ Lm, also denoted as {L1, … , Lm}. ALC formulae can be also expressed in ALC disjunctive clausal form or ALC positive matrix form, as { 1, … , },. A formula stated this way is called an ALC matrix. In an ALC matrix, each clause occupies a column.
To reach this normal form, the first two actions to be made over the axioms are: (i)
splitting equivalence axioms of the form C ≡ D into two axioms C ⊑ D and D ⊑ C,
and (ii) converting all the axioms into a Negated Normal Form (NNF), in which
negations occurs only on literals [
Definition 3 (ALC pure disjunction). The set of ALC pure disjunctions is the smallest set where: (i) D0 ∈ for every literal D0; (ii) D0 ⊔ D1 ∈ , in case D0, D1 ∈ ; (iii) if D0 ∈ then ∀r. D0 ∈ . An element D ∈ is an ALC pure disjunction. An ALC non-pure disjunction is an ALC disjunction that is not pure. Definition 4 (ALC pure conjunction). The set of ALC pure conjunctions is the smallest set where: (i) C0 ∈ for every literal C0; (ii) C0 ⊓ C1 iff C0, C1 ∈ ; and (iii) if C0 ∈ then ∃r. C0 ∈ . An element C ∈ is an ALC pure conjunction. An ALC non-pure conjunction is an ALC conjunction that is not pure. Definition 5 (Impurity on a non-pure expression). Impurities on non-pure ALC DL expressions are either conjunctive expressions in a non-pure disjunction or disjunctive expressions in a non-pure conjunction. The set of impurities is called ALC impurity set, and is denoted by .
Example 1 (Impurities on non-pure expressions).
The expression (∀r. (D0 ⊔ … ⊔ Dn ⊔ (C0 ⊓ … ⊓ Cm) ⊔ (A0 ⊓ … ⊓ Ap)), a non-pure disjunction, contains two impurities: (C0 ⊓ … ⊓ Cm) and A0 ⊓ … ⊓ Ap . Definition 6 (Positive normal form). An ALC axiom is in positive normal form iff it is in one of the following forms: ( ) C ⊑ D; (ii) C ⊑ ∃r. C; and (iii) ∀r. D ⊑ C; where C is a concept name, C a pure conjunction and D a pure disjunction.
In [
With all axioms in the normal form defined just above, it is easy to map them to matrix form, by applying the rules given in Table 1. Table 2 brings the mapping treatment of recursive sub-cases of existential and universal restrictions, when they occur inside any of the the normal form C ⊑ D,. An improvement of the approach is, as the usual DL notation, variables are not needed, since all relations are binary and dash lines make for disambiguation, as soon will be seen.
Some important remarks must be stated at this point for the sake of clarity.
The first is that the whole knowledge base KB is negated during this
transformation. This is due to the fact that in order to prove the validity of KB ⊨ (
being a subsumption axiom) using a direct method, ¬KB ∨ must be proven a
tautology (coming from KB → , according to the Deduction Theorem [
C ⊑ D, where n i=1 C =
Ai ,
D = m j=1
A′j with Ai ∈ (pure conjunction) and A′j ∈ (pure disjunction)
FOL Positive NNF
mapping (C(x)∧ ¬r(x,f(x))) ∨ (C(x) ∧ ¬ 1(f(x))) ∨
...∨ (C(x) ∧ ¬ (f(x))) (¬r(x,f(x)) ∧ ¬C(x)) ∨ (¬ ′1((f(x)) ∧ ¬C(x))∨
...∨ (¬ ′ ((f(x)) ∧ ¬C(x)) 1(x) ∧ ...∧ (x)
∧ ¬ ′1(x) ∧ ...∧ ¬ ′ (x) C C ¬r ¬A1 ¬r A '1 ¬C ¬C
Matrix
C
¬An A 'm
¬C A1 An ¬A '1 ¬A 'n
The first consequence of that is that subsumption axioms of the form C ⊑ D, which are usually logically translated as C → D, because negated (¬(C → D), indeed), are now translated to C ∧ ¬D, instead of ¬C ∨ D. Moreover, to establish a uniform set of rules applicable over ALC formulae, ¬ is dealt with, instead of , so as to consider ALC axioms as ¬ 1∨ …∨ ¬ ∨ (coming from ¬ 1∨ …∨ ¬ ∨ ¬¬ ), where ∈T (axioms in the TBox). The translation rules are then applied over ¬ and all .
Another remark regards implicit skolemization. In the original CM, once the whole KB should be negated, universal quantifiers (∀) are skolemized instead of existential, and all variables in the resulting DNF are then (implicitly) existentially quantified. Aiming at keeping a close correspondence with the original CM, only the cases in which ALC axioms, when translated to FOL, contain Skolem functions need to solved. For instance, the axiom C ⊑ ∃r. B, negated, translates to FOL Skolem DNF as ∃x(A(x) ∧ ¬r(x,f(x))) ∨ (A(x) ∧ ¬B(f(x))) (coming from the skolemization of ∀y in ∃x (A(x) ∧ (∀y (¬r(x,y) ∧ ¬B(y)))). In such cases, vertical and horizontal dash lines are employed to stand for the relations in the matrix. Vertical dash lines represent existential restrictions (∃r.C), which are not skolemized, while horizontal dash lines represent universal restrictions (∀r. C), in which the qualifier concept corresponds to a skolemized concept. An example should makes things clearer.
Example 2 (Positive normal form, skolemization, clause, matrix). The query Animal ⊓ ∃hasPart.Bone ⊑ Vertebrate Bird ⊑ Animal ⊓ ∃hasPart.Bone ⊓ ∃hasPart.Feather ⊨Bird ⊑ Vertebrate reads in FOL as (∀w(Animal(w) ∧ (∃z (hasPart(w,z) ∧ Bone(z)) → Vertebrate(w))) ∧ (∀x(Bird(x)→Animal(x)∧ ∃y(hasPart(x,y)∧ Bone(y))∧ ∃v(hasPart(x,v) ∧ Feather(v))) → ∀t(Bird(t) → Vertebrate(t))) where the variables y and t were respectively skolemized by the function f(x) and the constant c. In positive matrix clausal form, the formula is represented by {{Bird(x) ,¬Animal(x)}, {Bird(x) ,¬hasPart(x,f(x))}, {Bird(x) ,¬Bone(f(x))}, {Bird(x) ,¬hasPart(x,g(x))}, {Bird(x) ,¬Feather(g(x))}, {Animal(w), hasPart(w,z), Bone(z), ¬Vertebrate(w)}, {¬Bird(c)}, {Vertebrate(c))}}. Figure 1 shows it as a matrix. Bird Bird Bird Bird Bird ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
The vertical line connecting the symbols hasPart and Bone in the antepenultimate column has the function of denoting that the concept Bone has implicitly in FOL as argument the variable that is the 2nd argument of the relation hasPart (coming from the FOL translation ∃x∃y hasPart(x,y) ∧ Bone(y) that arose from the axiom ∃hasPart.Bone ⊑ Vertebrate. On its turn, the horizontal dash line connecting the symbols ¬hasPart and ¬Feather represents the ALC expression ∃hasPart.Feather in the original axiom Bird ⊑ ∃hasPart.Feather. This expression, negated, corresponds in FOL Skolem NF to ∃x ¬hasPart(x,f(x))∨ ¬Feather(f(x)). Thus, during reasoning, skolemized predicates such as the last ones can only be unified with variables, and not with concrete individuals or other with distinct Skolem functions.
Dash lines can superpose other dash lines, for instance to represent the axiom A ⊑ ∃r1. (∃r2. B). In this normal form they cannot cross, although this would not consist in a problem for the ALC method.
A last remark regards memory usage. By using this normal form, the number of
newly introduced symbols (and also the number of axioms) grows linearly with the
number of impurities. It is in most cases a gain compared with other normalizations
(e.g., EL [
The connection method (CM) [
Such distinctive features naturally led to the idea of proposing a connection method especially tailored to infer over description logic Semantic Web ontologies. The core of the paper, the ALC connection calculus, is explained next.
Definition 7 (Path, connection, unifier, substitution). A path is a set of literals from a matrix in which every clause (or column) contributes with one literal. A connection is a pair of complementary literals from different clauses, like { 1 , ¬ 2}, where σ( 1) (or ( 2)) is the most general unifier (mgu) between predicates 1 and ¬ 2. σ is the set of substitutions, which are mappings from variables to terms. All occurrences of the variable contained in a substitution would be replaced by the term indicated in σ. Example 4 (Path, connection, unifier, substitution). Some paths of the matrix of Figure 1 are: {Bird(x), ¬Bone(f(x)), Animal(w) ,¬Bird(c), Vertebrate(c)} and {¬Animal(w), Bird(x), ¬Bone(f(x)), Animal(w) ,¬Bird(c), Vertebrate(c)}. Some connections from the matrix are {Bird(x), ¬Bird(c)}, {¬hasPart(x,f(x)), hasPart(w,z)}, and σ={x/c, w/c, z/f(c)} is the whole matrix’ mgu.
Lemma 1 (Validity, active path, set of concepts). An ALC formula represented as a
matrix M is valid when every path contains a connection { 1, ¬ 2}, provided
that ( 1) = (¬ 2). This is due to the fact that a connection represents the
tautology 1 ∨ ¬ 2 in DNF. As a result, the connection method aims at finding a
connection in each path, together with a unifier for the whole matrix. During the
a variable or instance x during a proof is defined by ( ) ≝ { | ( ) ∈ ℬ} [
1 ∈
Rules are applied bottom-up. To start, the matrix M representing ⊨ is put in the bottom of the St rule, and a clause 1 ∈ is chosen as the first clause. Then, the three last rules are applied. The key rule for the calculus is the Extension rule, once it finds connections of the form { ( ), ¬ ( )}, ({C, ¬C} in the notation used here) or {r(x,y),¬r(z,w)}and the proper unifier σ for it (In the first case σ={x/y} and in the second σ={x/z, y/w}). Besides this slight change in the Start rule ( 1 ∈ ), a blocking mechanism was included as a new rule, the Copy rule. If the current literal can only connect a clause already in the active path, this clause is copied to the matrix, and the indexing function :
→ ℕ, that assigns the number of copies of each clause, is incremented. The use of this function avoids ordering of individuals, as done in the original CM. An important remark about the rule is that the copy is virtual, in the sense that only an index is created. CM requires only one copy of the matrix in memory. This is one of its main advantages. Its use of memory may be better than accomplished is incrementing . Then, before making a copy of clause 2 (this copy will be named 2 the variable
), it is necessary to check whether the set of concepts associated to
(i.e., if the new was unified) of the new literal 2 from 2 being
created by the Cop rule is not contained in the set of concepts of the original variable
x ( ( )), from 2( ) of 2 [
Examples of the ALC CM calculus’ application can be found at [
Theorem 1 (Soundness and completeness) An ALC formula in positive matrix form
makes the Axiom rule (Ax) applicable to all leaves of the generated tree.
is valid iff there is a connection proof for “ , , ”, i.e. the application of the rules
Proof The introduced changes in rules do not lose the soundness of the original CM
(whose proof is available at [
∉ ), and, (b) the variable being copied is already a copy of another variable attached to the same concepts (as stated by the conditions ( ) ⊈ ( )18T). Therefore it prevents infinite applications of the Copy rule that would not help proving in the original CM’s completeness.
Theorem 2 (Termination). ALC CM always terminates.
⊨ 18T, and thus, such condition does not interfere of literal 2 Proof Having the mindset that the Copy rule is the only source of non-termination, the proof has three subcases: (i) When KB contains no cycle, the calculus finishes in a finite number of steps because the number of choices arising from the finite number of clauses and possible connections is also finite. Since the Copy rule is never fired, and there are no loops, ALC CM always terminates. (ii) When KB contains cycles and
⊨ , the system always terminates, because ALC CM behaves exactly equal the
original CM, whose termination proof can be found at [
⊭ is the only aspect not covered by the original CM, given FOL’s semi-decidability. Nevertheless, ALC CM always terminates for this case, due to the fact that the Copy rule obliges the set of concepts of the newly created instance not to be a subset of any of the sets of concepts of other introduced the number of distinct sets is limited to 2 finite. Thus ALC CM always terminates in all three cases. instances of the literal. Once every set of concepts is a subset of and is finite, | |. So, the number of copies for literals is
The system can also be expressed in an easier way using matrices to build proofs.
Figure 5 portraits an example using matrices. An ALC CM calculus’ algorithm of the
system was adapted [
Example 5 (ALC connection calculus). Figure 3 deploys the proof of the query stated in example 1. In the figure, literals of the active path are in boxes and arcs denote connections. For building a proof, firstly a clause from the consequent (Start rule) is chosen, say, the clause {¬Bird(c)} and a literal from it (¬Bird(c)).
Step 1 connects this clause with the first matrix clause. An instance or variable representing a fictitious individual that is being predicating about -, appears in each arc; in this connection, the instance c. The arrow points to literals still to be checked in the clause (only the literal ¬Animal in Step 1), that should be checked afterwards. After step 2, the connection {¬Animal, Animal} is not enough to prove all paths stemming from the other clause (the one with literal ¬Animal). In order to assure that, the remaining literals from that clause, viz hasPart, Bone and ¬Vertebrate, have still to be connected. Then, in step 3, when the predicate hasPart is connected, instance c being dealt with any more, but a relation between it and another variable or fictitious individual, say y (indicated by (c,y)).
Until that moment, only the Extension rule was applied. However, in step 4, the Reduction rule is used, triggered by its two enabling conditions: (i) there is a connection for the current literal already in the proof; and (ii) unification can take place. Unification would not be possible between different individuals and/or skolemized functions (in ALC, equality among individuals is not necessary).
Next, a connection for the literal Bone was needed. That time, the variable (or fictitious individual) y is being referred, for the reason that it stands for a part of the individual c (hasPart(c,y)).
In case the system is able to summon the query, the processing finishes when all paths are exhausted and have their connections found. In case a proof cannot be entailed, the system would have tried all available options of connections, unifiers and clause copies, having backtracked to the available options in case of failure.
In [
While planning the ALC CM, i.e. adapting the original CM to ALC, the notation was designed in order to avoid any ambiguities to arise from the lack of variables in the representation – that was the rationale of dashlines replacing the quantifiers, so as to eliminate possible ambiguities with skolemization for the connections. This notation can be changed even further, since assertions are better stored outside the matrices, bringing two benefits: matrix size can be dramatically shrunk and powerful indexing mechanisms for retrieving assertions, such as relational databases, can be employed. However, even sticking only to TBoxes, matrices can be sparse, a memory waste. A simple solution for this consists in storing matrices as arrays of arrays.
Concerning reasoning, the first aspect to be taken into account resides in the
strong similarity between CM and tableaux [
First, the work presented here shall be extended to more complex description logic
languages in a near future. Particularly, formalizations and implementations for the
DLs EL++, SHIQ and SROIQ will be practically useful for applications related to the
Semantic Web provided that good solutions for dealing with equality are available,
like eq-connections [
Another potential reasoning advantage to be pursued could be the memory required for ALC CM. Despite the fact that, given a connection proof, the size of an equivalent tableau proof is not significantly bigger (perhaps a quadratic increase in size); the proof search might indeed take up much more space, as the search is essentially saturation-based and many parts of a problem maybe not be required for the proof. However, these statements demand additional research to be proven true.
Last but not least, lean implementations written in Prolog, in the flavor of
leanCop [