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
2. An ALC Positive Matricial Normal Form
(ii) converting all the axioms into a Negated Normal Form (NNF), in which negations
occurs only on literals [
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).
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 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. 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 1and ¬ 2. σ is the set of Matrix C C ¬r ¬A1 ¬r A '1 ¬C ¬C
C
¬An A 'm
¬C A1 An ¬A'1 ¬A'n Direct Matrix r A r ¬A ' Axiom type
n C ⊑ ∃r. Cˆ , where Cˆ = A ,
i i=1 with Ai ∈ SC (pure conjunction) ∀ . ⊑ , where = A' j , j=1 m with A' j ∈ SD (pure disjunction)
Cˆ ⊑ , where n m Cˆ = Ai , = A' j ,
i=1 j=1
FOL Positive NNF mapping (C(x)∧ ¬r(x,f(x))) ∨ (C(x)∧¬ A1 (f(x))) v... v (C(x)∧¬ An (f(x))) (¬r(x,f(x))∧¬C(x)) ∨ (¬ A'1 (f(x))∧¬C(x)) v...v (¬ A'm (f(x))∧¬C(x)) A1 (x)∧...∧ An (x) ∧ ¬A1' (x)∧...∧ ¬Am' (x)
restriction: … ⊔ ∀r.A’ ⊔ …, with A’ ∈ SC (pure disjunction)
FOL Positive
DNNF mapping
... ∧ r(x,y)∧ A(y)∧ ...
…∧ r(x,y) ∧ ¬A’(y) ∧
…
NNF Positive Matrix r( x, y) A( y)
r( x, y) ¬A '( y) 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 ( ) ≝ { | ( ) ∈ ℬ} [
Definition 5 (ALC connection sequent calculus). Figure 1 brings the rules in sequent
style of the ALC connection calculus, adapted from [
ℎ
ℎ
Blocking didn’t occur in the original CM due to FOL semi-decidability, but it if the new
was unified) of the new literal 2 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., being created by the Cop rule is not contained in the set of concepts of the original x from 2( ) (in the rule, ( )) [Schmidt &
calculus, as well as an
algorithm of the system based on [
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 [
Example 1 (ALC connection calculus).
Animal ⊓ ∃hasPart.Bone ⊑ Vertebrate Bird ⊑ Animal ⊓ ∃hasPart.Bone ⊓ ∃hasPart.Feather ⊨Bird ⊑ Vertebrate 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
c Bird Bird Bird Bird Bird 1. ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
c Bird Bird Bird Bird Bird ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather 2. Bird Bird Bird Bird Bird 3. ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
(c,y) Bird Bird Bird Bird Bird 4. ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
(c,y) Bird Bird Bird Bird Bird 5. ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
y (c,y) Bird Bird Bird Bird Bird 6 &7. ¬Animal ¬hasPart ¬Bone ¬hasPart ¬Feather
(c,y) y c c c c
Animal hasPart
Bone ¬Vertebrate
Animal hasPart
Bone ¬Vertebrate
Animal hasPart
Bone ¬Vertebrate
Animal hasPart
Bone ¬Vertebrate
Animal hasPart
Bone ¬Vertebrate
Animal hasPart
Bone ¬Vertebrate ¬Bird(c) Vertebrate(c) ¬Bird(c) Vertebrate(c) ¬Bird(c) Vertebrate(c) ¬Bird(c) Vertebrate(c) ¬Bird(c) Vertebrate(c) ¬Bird(c) Vertebrate(c)
c {{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)).
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. 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 [
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
Last but not least, lean implementations written in Prolog, in the flavor of
leanCop [