=Paper=
{{Paper
|id=None
|storemode=property
|title=An ALC Description Logic Connection Method
|pdfUrl=https://ceur-ws.org/Vol-776/ontobras-most2011_paper24.pdf
|volume=Vol-776
|dblpUrl=https://dblp.org/rec/conf/ontobras/Freitas11
}}
==An ALC Description Logic Connection Method==
https://ceur-ws.org/Vol-776/ontobras-most2011_paper24.pdf
An ALC Description Logic Connection Method
Fred Freitas
Informatics Center - Federal Universidade of Pernambuco (CIn - UFPE)
Av. Prof. Luis Freire, s/n, Cidade Universitária, 50740-540, Recife – PE, Brazil
fred@cin.ufpe.br
Abstract. The connection method earned good reputation in the field of
automated theorem proving for around three decades, due to its simplicity,
clarity, efficiency and parsimonious use of memory. This seems to be a very
appealing feature, in particular in the context of Semantic Web, where it is
assumed that the knowledge bases might be of arbitrary size. In this paper, I
present a connection method especially tailored to infer over the description
logic (DL) ALC. Our ALC connection method is formalized in sequent style,
although matrices should be employed for practical reasons.
1. Introduction
The problem of reasoning over ontologies written in Description Logic (DL) [Baader et
al 2003] has been receiving strong interest from researchers, particularly since the
Semantic Web inception. Regarding this issue, the use of memory is certainly one
important asset for a good reasoning performance. I am proposing a formalized
inference system which seems adequate to address understandability and the use of a
small amount of memory. Our inference system is based on the connection method
(CM) [Bibel 1987], which is a simple, clear and effective inference method that has
been used successfully over first order logic (FOL). Its main features clearly meet with
the demands: (i) it keeps only one copy of each logical sentence in memory; and (iii) it
does not derive new sentences from the stored ones.
Definition 1 (Disjunctive normal form (DNF), clause, positive matricial form). A
formula in DNF is a disjunction of conjunctions, being in the form 𝐶1 ∨ … ∨ 𝐶𝑛 , where
each 𝐶𝑖 is a clause (or dual clause). Clauses are conjunctions of literals like 𝐿1 ∧ … ∧ 𝐿𝑚 ,
also denoted as {𝐿1 , … , 𝐿𝑚 }. Formulae can be also expressed in disjunctive clausal form
as {𝐶1 , … , 𝐶𝑛 }. Formulae stated this way are also in positive matricial form, since they can
be represented as a matrix. In the matrix, each clause occupies a column.
Definition 2 (Skolemization). Instead of existential quantifiers, universal quantifiers
(∀) are replaced by constants or Skolem functions, since I will work with the whole
knowledge based negated (see next section). Variables in the resulting DNF are then
(implicitly) existentially quantified.
I started with the Description Logic ALC (Attributive Concept Language with
Complements) [Baader et al 2003], since it constitutes the foundations of many other
DLs. I now present an ALC normal form and the ALC CM calculus.
2. An ALC Positive Matricial Normal Form
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
195
(ii) converting all the axioms into a Negated Normal Form (NNF), in which negations
occurs only on literals [Baader et al 2003]. Next, I define the normal form and
impurities with regard to it.
Definition 3 (ALC disjunction, ALC conjunction). An ALC disjunction is either a
literal, a disjunction 𝐸0 ⊔ 𝐸1 or an universal restriction ∀𝑟. 𝐸0 . An ALC conjunction is
either a literal, a conjunction 𝐸0 ⊓ 𝐸1 or an existential restriction ∃𝑟. 𝐸0 . 𝐸0 and 𝐸1 are
arbitrary concept expressions.
Definition 4 (ALC pure disjunction). The set 𝑆𝐷 of ALC pure disjunctions is the
smallest set where: (i) 𝐷0 ∈ 𝑆𝐷 for every literal 𝐷0 ; (ii) If 𝐷0 , 𝐷1 ∈ 𝑆𝐷 , then 𝐷0 ⊔ 𝐷1
∈ 𝑆𝐷 ; and (iii) if 𝐷0 ∈ 𝑆𝐷 then ∀𝑟. 𝐷0 ∈ 𝑆𝐷 . An element 𝐷 � ∈ 𝑆𝐷 is an ALC pure
disjunction. An ALC non-pure disjunction is an ALC disjunction that is not pure.
Definition 5 (ALC pure conjunction). The set 𝑆𝐶 of ALC pure conjunctions is the
smallest set where: (i) 𝐶0 ∈ 𝑆𝐶 for every literal 𝐶0 ; (ii) if 𝐶0 , 𝐶1 ∈ 𝑆𝐶 then 𝐶0 ⊓ 𝐶1 ∈
𝑆𝐶 ; and (iii) if 𝐶0 ∈ 𝑆𝐶 then ∃𝑟. 𝐶0 ∈ 𝑆𝐶 . An element 𝐶̌̂ ∈ 𝑆𝐶 is an ALC pure
conjunction. An ALC non-pure conjunction is an ALC conjunction that is not pure.
Definition 6 (Impurity of a non-pure expression). Impurities of 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 (∀𝑟. (𝐷0 ⊔ … ⊔ 𝐷𝑛 ⊔ (𝐶0 ⊓ … ⊓ 𝐶𝑚 ) ⊔ (𝐴0 ⊓ … ⊓ 𝐴𝑝 )), a non-pure
disjunction, contains two impurities: (𝐶0 ⊓ … ⊓ 𝐶𝑚 ) and �𝐴0 ⊓ … ⊓ 𝐴𝑝 �.
Definition 7 (Positive normal form). An � ALC axiom is in positive normal form iff it is
in one of the following forms: (𝑖)𝐶̂ ⊑ 𝐷 � ; (𝑖𝑖)𝐶 ⊑ ∃𝑟. 𝐶̂ ; and (𝑖𝑖𝑖) ∀𝑟. 𝐷
� � ⊑ 𝐶; where C
is a concept name, 𝐶̂ a pure conjunction and 𝐷 � a pure disjunction.
[Freitas et al 2011] contains ALC transformation algorithms to this normal form.
2.1. Translation Rules for the normalization
With all axioms in normal form, it is easy to map them both to FOL and to the matricial
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 three normal forms. An improvement of the approach is, as the usual DL notation,
we do not need variables, since all relations are binary.
In order to prove KB ⊨ α, the whole knowledge base KB is negated during this
transformation, once we wish to prove ¬KB ∨ α valid. Because of that, subsumption
axioms of the form C ⊑ D, which are 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 to apply over formulae, we deal with ¬𝛼 instead of 𝛼,
so we consider formulae as ¬𝐴1 ∨ …∨ ¬𝐴𝑛 ∨ ¬¬𝛼 where 𝐴𝑖 ∈T (axioms in the TBox).
The translation rules can then be applied over ¬𝛼 and all 𝐴𝑖 .
Regarding skolemization, one representational advantage of the approach resides
in the clearer matrix representation of universally quantified roles’ (∀𝑟. 𝐶 or in the
matrices, the negated ∃𝑟. 𝐶). This construct, by definition, has the interpretation
(∀𝑟. 𝐶)𝐼 = {∀𝑏, (𝑎, 𝑏) ∈ 𝑅𝐼 → 𝑏 ∈ 𝐶 𝐼 }. Hence, for an axiom of the form 𝐴 ≡ ∀𝑟. 𝐶, the
definition does not oblige concept A to dispose of instances – this is indeed a very
196
common error from DL users. But maybe it is not their fault: for instance, tableaux
proofs over such axioms don’t stress this semantics, in the sense that it allows instances
of A without any role instances from r associated to it. In the ALC CM, the matricial
representation explicits this situation: either there are no role instances (¬𝑟) or when it
has a role instance (a,b), b has to be an instance of concept C.
Table 1. Translation rules to map ALC into FOL positive NNF and matrices.
Axiom type FOL Positive NNF Matrix
mapping
n (C(x)∧ ¬r(x,f(x))) ∨
C ⊑ ∃r. Ĉ , where Ĉ =
i =1
Ai , (C(x)∧¬ A1 (f(x))) C C
¬r ¬A
C
v... v
1 ¬An
with Ai ∈ SC (pure conjunction) (C(x)∧¬ An (f(x)))
m
(¬r(x,f(x))∧¬C(x)) ∨
� ⊑ 𝐶 , where 𝐷
∀𝑟. 𝐷 �= A' ,
j =1
j (¬ A '1 (f(x))∧¬C(x)) ¬r A '1 A 'm
v...v ¬C ¬C
with A ' j ∈ S D (pure disjunction) (¬ A 'm (f(x))∧¬C(x)) ¬C
A1
A1 (x)∧...∧ An (x) ∧
Ĉ ⊑ 𝐷
� , where ¬A1' (x)∧...∧ ¬Am' (x)
An
n m ¬A '
Ĉ = � = A' ,
Ai , 𝐷 j 1
i =1 j =1
Ai ∈ SC (pure conjunction), ¬A ' n
A ' j ∈ S D (pure disjunction)
Table 2. Recursive sub-cases of existential and universal restrictions.
Axiom type FOL Positive NNF Direct
DNNF Positive Matrix
mapping Matrix
Ai is an existencial
restriction: ... ∧ r ( x, y ) r
… ⊓ ∃r.A ⊓ ... , r(x,y)∧
with A ∈ SC
A(y)∧
A( y ) A
...
(pure conjunction)
A ' j is an universal
restriction:
…∧ r ( x, y ) r
r(x,y) ∧
… ⊔ ∀r.A’ ⊔ …, ¬A’(y) ∧
¬A '( y ) ¬A '
with A’ ∈ SC …
(pure disjunction)
3. An ALC Connection Calculus in Sequent Style
Definition 3 (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
197
substitutions, which are mappings from variables to terms.
Definition 4 (Validity, active path, set of concepts). An ALC formula represented as a
matrix 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 proof, the current path is called active
path and denoted by ℬ. The set of concepts 𝜏 of a variable or instance x during a proof is
defined by 𝜏(𝑥) ≝ {𝐶|𝐶(𝑥) ∈ ℬ} [Schmidt & Tishkovsky 2007].
Definition 5 (ALC connection sequent calculus). Figure 1 brings the rules in sequent
style of the ALC connection calculus, adapted from [Otten 2010].
𝐴𝑥𝑖𝑜𝑚 (𝐴𝑥)
{ }, 𝑀, 𝑃𝑎𝑡ℎ
𝐶2 , 𝑀, {}
𝑆𝑡𝑎𝑟𝑡 𝑅𝑢𝑙𝑒 (𝑆𝑡)
𝜀, 𝑀, 𝜀
𝑤ℎ𝑒𝑟𝑒 𝑀 𝑖𝑠 𝑡ℎ𝑒 𝑚𝑎𝑡𝑟𝑖𝑥 𝐾𝐵 ⊨ 𝛼, 𝐶2 𝑖𝑠 𝑎 𝑐𝑜𝑝𝑦 𝑜𝑓 𝐶1 ∈ 𝛼
𝐶 𝜎 , 𝑀, 𝑃𝑎𝑡ℎ ∪ {𝐿2 }
𝑅𝑒𝑑𝑢𝑐𝑡𝑖𝑜𝑛 𝑅𝑢𝑙𝑒 (𝑅𝑒𝑑)
𝐶 ∪ {𝐿1 }, 𝑀, 𝑃𝑎𝑡ℎ ∪ {𝐿2 }
𝑤𝑖𝑡ℎ 𝜎(𝐿1 ) = 𝜎(𝐿 ���2 )
𝐶2𝜎 \{𝐿𝜎2 }, 𝑀, 𝑃𝑎𝑡ℎ ∪ {𝐿1 } 𝐶 𝜎 , 𝑀, 𝑃𝑎𝑡ℎ
𝐸𝑥𝑡𝑒𝑛𝑠𝑖𝑜𝑛 𝑅𝑢𝑙𝑒 (𝐸𝑥𝑡)
𝐶 ∪ {𝐿1 }, 𝑀, 𝑃𝑎𝑡ℎ
���2 ),
𝑤𝑖𝑡ℎ 𝐶2 𝑎 𝑐𝑜𝑝𝑦 𝑜𝑓 𝐶1 ∈ 𝑀, 𝐿2 ∈ 𝐶2 , 𝜎(𝐿1 ) = 𝜎(𝐿
𝜇
𝐶 ∪ {𝐿1 }, 𝑀 ∪ {𝐶2 }, 𝑃𝑎𝑡ℎ ∪ {𝐿2 }
𝐶𝑜𝑝𝑦 𝑅𝑢𝑙𝑒 (𝐶𝑜𝑝)
𝐶 ∪ {𝐿1 }, 𝑀, 𝑃𝑎𝑡ℎ ∪ {𝐿2 }
𝜎
𝑤𝑖𝑡ℎ 𝐿2 ∈ 𝐶2 , 𝜇 ← 𝜇 + 1, 𝑎𝑛𝑑 �𝑥𝜇𝜎 ∉ 𝑁𝑂 𝑜𝑟 𝜏(𝑥𝜇𝜎 � ⊈ 𝜏�𝑥𝜇−1 ���2 ) (𝑏𝑙𝑜𝑐𝑘𝑖𝑛𝑔 𝑐𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛𝑠)
)�, 𝜎(𝐿1 ) = 𝜎(𝐿
Figure 1. The ALC connection calculus rules in sequent style (adapted from
[Otten 2010]).
Blocking didn’t occur in the original CM due to FOL semi-decidability, but it
consists in a common practice in DL to guarantee termination. Here, to assure
termination, we have to check if the set of concepts 𝜏 associated to the variable 𝑥𝜇𝜎 (i.e.,
𝜇
if the new 𝑥𝜇 was unified) of the new literal 𝐿2 being created by the Cop rule is not
contained in the set of concepts of the original x from 𝐿2 (𝑥) (in the rule, 𝜏(𝑥 𝜎 ))
[Schmidt & Tishkovsky 2007]. Examples of the ALC CM calculus, as well as an
algorithm of the system based on [Bibel 1987] can be found at [Freitas et al 2010].
In terms of complexity, the system is PSPACE in case of non-cyclical ontologies
and EXPTIME for cyclical. Proofs of its completeness, soundness and termination are
presented in [Freitas et al 2010].
Example 1 (ALC connection calculus).
Animal ⊓ ∃hasPart.Bone ⊑ Vertebrate
⊨Bird ⊑ Vertebrate
Bird ⊑ Animal ⊓ ∃hasPart.Bone ⊓ ∃hasPart.Feather
In FOL positive matricial clausal form, where the variables y and t were respectively
skolemized by the function f(x) and the constant c, the formula is represented by
198
{{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 2 deploys the query proof. In the figure, literals of the active path are in
boxes and arcs denote connections. For building a proof, we first choose a clause from
the consequent (Start rule), say, the clause {¬Bird(c)} and a literal from it (¬Bird(c)).
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
1. Bone
¬Vertebrate
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
2. Bone
¬Vertebrate
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
3. (c,y) Bone
¬Vertebrate
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
4. (c,y) Bone
¬Vertebrate
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
5. (c,y) Bone
y
¬Vertebrate
c
Bird Bird Bird Bird Bird Animal ¬Bird (c) Vertebrate(c)
¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather hasPart
6 &7. (c,y) Bone c
y ¬Vertebrate
Figure 2. A connection proof example in matricial form.
Step 1 connects this clause with the first matrix clause. An instance or variable -
representing a fictitious individual we are predicating about -, appears in each arc, for
this connection, the instance c. The arrow points to literals to be checked in the clause
(¬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 we
connect hasPart, we are not talking about instance c any more, but about a relation
between it and another variable or fictitious individual, say y (indicated by (c,y)).
Until that moment, we were only applying the Extension rule. However, in step
4, we use the Reduction rule, 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.
199
Unification would not be possible if we were referring to different individuals or
skolemized functions (in ALC, equality among individuals is not necessary).
A small note on unification is necessary here, because it brings a small trick to
the calculus. Since horizontal dashlines represent universal restrictions (∀𝑟. 𝐶), the
qualifier concept (C, represented as ¬𝐶 in the matrix) correspond to a skolemized
concept (say C(f(c))). Therefore, it can only be unified with variables, but not with
concrete individuals or other skolemized qualifier concepts.
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.
4. Conclusions and Future Work
I have formalized a connection method to take on the DL ALC, by adapting the CM
calculus formalized in sequent style from [Otten 2010] and including a new rule. I also
introduced some notational improvements, the key one being the representation without
variables. Of course, I plan to continue this work in many research directions, such as
implementations, other DLs, Semantic Web, etc.
I intend to extend the work presented here 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 and for some other biomedical applications that I am involved in.
Last but not least, lean implementations written in Prolog, in the flavor of
leanCop [Otten & Bibel 2003], that demand small memory space, can serve
applications that are constrained in memory, such as stream reasoning in mobile
applications, for instance. They are also in my research agenda.
References
Baader, F., Calvanese, D., McGuinness, D,, Nardi, D., Patel-Schneider, P. (Eds.): The
Description Logic Handbook. Cambridge University Press, 2003.
Bibel, W. Automated theorem proving. Vieweg Verlag, Wiesbaden, 1987.
Freitas, F. A Connection Method for Reasoning with the Description Logic ALC.
Technical report. 2010. www.cin.ufpe.br/~fred/CM-ALCTechRep.doc
Otten, J.Restricting backtracking in connection calculi.AI Comm,23(2-3):159-182 2010.
Otten, J., Bibel, W. leanCoP: Lean Connection-Based Theorem Proving. Journal of
Symbolic Computation, Volume 36, pages 139-161. Elsevier Science, 2003.
Schmidt, R., Tishkovsky, D. Analysis of Blocking Mechanisms for Description Logics.
In Proceedings of the Workshop on Automated Reasoning, 2007.
200