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.
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.
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.
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 [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 ๐ ๐ผ .
The expression (โ๐.
). 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.
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 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.
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 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 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].
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 โจBird โ Vertebrate {{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)). 2.
3.
5.
Step 1 connects this clause with the first matrix clause. An instance or variablerepresenting 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.
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.