A Connection Calculus for the Description Logic ${\mathcal{ALC}}$

Abstract

This paper presents a connection calculus for the description logic (DL) ${\mathcal{ALC}}$. It replaces the usage of Skolem terms and unification by additional annotation and introduces blocking, a typical feature of DL provers, by a new rule, to ensure termination in the case of cyclic ontologies. Besides the connection calculus, a simplified clausal form normalization is presented. Furthermore, termination, soundness and completeness of the calculus are proven.

1 Introduction

Description logics (DL) are widely used for knowledge representation and modelling ontologies, e.g., they are the standard ontology language for the semantic web [1]. One approach to reason with DL is the embedding of DL into classical first-order logic (FOL) and using existing provers for FOL. On the one hand, when using a FOL prover to answer DL queries, no alterations are required, since DL correspond to decidable fragments of FOL [6, 8]. Moreover, the main FOL reasoners were exhaustively tested, and thus, their usage is reliable. On the other hand, in a preliminary study, Tsarkov et al. reported that, even running one of the fastest FOL provers, the FOL approach displays a performance much slower than a specially crafted DL reasoner [12].

This paper proposes a connection calculus θ-CM for ${\mathcal{ALC}}$, an important fragment of DL. It relies on annotations instead of Skolem terms, and includes a rule for copying clauses that implements blocking, similarly to existing tableau-based DL reasoners. It is a significantly enhanced version of the connection calculus proposed earlier [3], which essentially translates a DL formula into a FOL matrix, thus including Skolem terms and unification, the latter here replaced by a similar procedure, θ-substitution.

The calculus was implemented in RACCOON (ReAsoner based on the Connection Calculus Over Ontologies) [4]. Therefore, such a calculus and its implementation can serve any Semantic Web application that deals with ${\mathcal{ALC}}$, an important DL language.

Section 2 presents the DL ${\mathcal{ALC}}$; its normalization is shown in Sect. 3. Section 4 explains the formal connection calculus for ${\mathcal{ALC}}$, while its termination, soundness and completeness are proven in Sect. 5. Section 6 concludes with a summary.

2 The Description Logic ${\mathcal{ALC}}$

An ontology O in ${\mathcal{ALC}}$ is a set of axioms over a signature (N _C , N _R , N _O ), where N _C is the set of concept names (unary predicate symbols), N _R is the set of role or property names (binary predicate symbols); N _O is the set of individual names (constants) [1]. Concept expressions are inductively defined as follows. N _C includes ⊤, the universal concept that subsumes all concepts, and ⊥, the bottom concept subsumed by all concepts; all concept names belong to N _C . If r ∈ N _R is a role and C, D ∈ N _C are concepts, then these formulae are also concepts: (i) $C\;\sqcup\;D$ (ii) $C\;\sqcap\;D$, (iii) ¬C, (iv) ∀r.C; (v) ∃r.C.

A knowledge base in DL consists of a set of basic axioms (TBox), and a set of axioms specific to a particular situation (ABox). Two axiom types are allowed in a TBox ${\mathcal{T}}$: (i) C ⊑ D; (ii) C ≡ D, standing for C ⊑ D and D ⊑ C. An ABox ${\mathcal{A}}$ w.r.t. a TBox ${\mathcal{T}}$ is a finite set of assertions of two types: (i) a concept assertion is a statement of the form C(a), where a ∈ N _O , C ∈ N _C and (ii) a role assertion r(a, b), where a, b ∈ N _O , r ∈ N _R . An ${\mathcal{ALC}}$ formula is either an axiom or an assertion; an ontology O is an ordered pair (${\mathcal{T}}, {\mathcal{A}}$).

There are two major ways of defining the semantics of ${\mathcal{ALC}}$. The first one relies on the definitions of interpretation, model, etc., over a domain Δ [1]. Another way is by mapping ${\mathcal{ALC}}$ constructs to FOL (see [1], 2.2.1.3) and exploiting the semantics defined for FOL, see, e.g., [2]. This approach defines a translation ϕ that maps a concept C to a unary predicate ϕ _C (x) with a free variable x. If C is a concept and r a role, then, e.g., ∃r.C is translated into the FOL formula $\phi_{\exists r.C} \left( y \right) = \exists x r\left( {y,x} \right){\wedge } \phi_{C} (x)$ [1].

The work described in this paper uses an adaption of the translation approach, hence, taking advantage of existing concepts of connection calculi for FOL.

As for notation, in this paper, words starting with a capital letter denote concepts; roles start with small letters. Individuals are denoted by the lowercase letters a, b, c, d; variables are denoted by x, y, z, k, u, v. Terms are either variables or individuals.

3 Normal Form and Matrix for ${\mathcal{ALC}}$

Definition 1

(Query). A query α (a TBox or ABox axiom) against an ontology O is an ${\mathcal{ALC}}$ formula for which the logical consequence O ⊨ α should be proven.

Definition 2

${\bf (}{\mathcal{ALC}}$ Disjunctive Normal Form, Clause, Matrix, Graphical Matrix). Literals (of ${\mathcal{ALC}}$) are atomic concepts or roles, possibly negated. Literals involved in an universal restriction ∀r.C or in a existential restriction ∃r.C are underlined. In case a restriction involves more than one clause, literals are indexed with the same new column index number at the top. Literals can participate at most in two universal restrictions in left-hand side (LHS) axiom’s sub-formula or in two existential ones in the right-hand side (RHS); therefore, they can have at most two indices, e.g. L ^i,j. An ${\mathcal{ALC}}$ formula in disjunctive normal form (DNF) is a disjunction of conjunctions (like $C_{1} \vee \ldots \vee C_{n}$), where each C _i has the form $L_{1} \wedge \ldots \wedge L_{m}$ and each L _i is a literal. The (${\mathcal{ALC}}$) matrix of an ${\mathcal{ALC}}$ formula in DNF is its representation as a set $\left\{ {C_{1} , \ldots ,C_{n} } \right\}$, where each clause C _i has the form $\left\{ {L_{1} , \ldots ,L_{m} } \right\}$ with literals L _i . In the graphical matrix representation, clauses are represented as columns, and restrictions as lines; restrictions with indexes are horizontal, while those without are vertical (see Example 1).

Remark 1.

To deduce O ⊨ α the validity of the formula $C_{1 } \wedge \ldots \wedge C_{n} \to \alpha\;(O \to \alpha )$, i.e. of ¬O ∨ α, must be proven. The effects for the DNF are: (i) axioms of the form E ⊑ D translate into E ∧ ¬D; (ii) ABox assertions are negated; (iii) free variables are existentially quantified; (iv) FOL Skolemization is applied to universal variables; and (v) the query α is not negated.

Example 1

(Query, Clause, ${\mathcal{ALC}}$ Matrix). The query {∃hasPet.Cat ⊑ CatOwner, OldLady ⊑ ∃hasPet.Animal ⊓ ∀ hasPet.Cat} ⊨ OldLady ⊑ CatOwner reads in FOL as:

$$ \left. {\begin{array}{*{20}c} {\forall x\left( {\left( {\exists y hasPet\left( {x,y} \right) \wedge Cat\left( y \right)} \right) \to CatOwner\left( x \right)} \right)} \\ {\forall z\left( {OldLady\left( z \right) \to \forall k\left( {hasPet\left( {z,k} \right) \to Cat\left( k \right)} \right)} \right)} \\ {\forall z\left( {OldLady\left( z \right) \to \exists v\left( {hasPet\left( {z,v} \right) \wedge Animal\left( v \right)} \right)} \right)} \\ \end{array} } \right\}\vDash\forall u(OldLady\left( u \right) \to CatOwner(u)) $$

and is represented by the FOL matrix (where a is a Skolem terms, f a function symbol):

$$ \begin{aligned} & \{ \{ hasPet\left( {x,y} \right), \, Cat\left( y \right), \, \neg CatOwner(x)\} ,\{ OldLady\left( z \right),hasPet\left( {z,v} \right),\neg Cat(v)\} , \\ & \{ OldLady\left( z \right), \, \neg hasPet(z,f(z))\} ,\{ OldLady\left( z \right), \, \neg Animal(f(z))\} ,\{ \neg OldLady(a)\} ,\{ CatOwner(a)\} \} \\ \end{aligned} $$

and by the following ${\mathcal{ALC}}$ matrix (the column index marks the two clauses involved in he same restriction; variables are omitted as they are specified implicitly) (Fig. 1):

$$ \begin{aligned} & \{ \{ \underline{hasPet,Cat} , \, \neg CatOwner\} ,\{ OldLady,\underline{hasPet,\neg Cat} \} ,\{ OldLady,\underline{{\neg hasPet^{1} }} \} , \\ & \{ OldLady,\underline{{\neg Animal^{1} }} \} ,\{ \neg OldLady\left( a \right)\} ,\{ CatOwner\left( a \right)\} \} \\ \end{aligned} $$

Fig. 1.

The query from Example 1 represented as an ${\mathcal{ALC}}$ matrix

Definition 3

(Impurity, Pure Conjunction/Disjunction). Impurity in an ${\mathcal{ALC}}$ formula is a disjunction in a conjunction, or a conjunction in a disjunction. A pure conjunction (PC) or disjunction (PD) does not contain impurities (see [3] for a formal definition).

Example 2

(Impurity, Pure Conjunction/Disjunction). (a) ∃r.A and $\wedge_{i = 1}^{n} A_{i}$ are PCs if A and each A _i is also a PC. (b) $\forall r.\left( {D_{0} \,{ \sqcup } \ldots \,{ \sqcup }\,D_{n} { \sqcup }\left( {C_{0} \,{ \sqcap } \ldots \,{ \sqcap }C_{m} } \right){ \sqcup }\left( {A_{0} \,{ \sqcap } \ldots \,{ \sqcap }A_{p} } \right)} \right)$ is not a PD as it contains two impurities: $\left( {C_{0}\,{ \sqcap } \ldots { \sqcap }\,C_{m} } \right)$ and $\left( {A_{0} \,{ \sqcap } \ldots { \sqcap }\,A_{p} } \right)$.

Definition 4

(Two-Lined Disjunctive Normal Form). An ${\mathcal{ALC}}$ axiom is in 2-lined DNF iff it is in DNF and in one of the normal forms (NFs): (i) $\hat{E}$ ⊑ $\check{D}$; (ii) $E$ ⊑ $\hat{E}$; (iii) $\check{D}$ ⊑ $E$, where E is a concept name¹, $\hat{E}$ is a pure conjunction, and $\check{D}$ is a pure disjunction².

Example 3

(Two-Lined Disjunctive Normal Form). The axioms (i) $\hat{E}$ ⊑ $\check{D}$ (1NF); (ii) $E$ ⊑ $\exists r.\hat{E}$ (2NF) and (iii) $\forall r.\check{D}$ ⊑ $E$ (3NF), where $\hat{E} = {\wedge }_{i = 1}^{n} C_{i}$ and $\check{D} = {\vee }_{j = 1}^{m} D_{j}$ (Fig. 2).

Fig. 2.

Examples of the three two-lined normal forms’ representations in ${\mathcal{ALC}}$

Example 4

(Two-Lined DNF). Table 1 shows examples of quantification restrictions. Vertical lines represent existential restrict ions $(\exists r.C)$, horizontal lines represent universal restrictions $(\forall r.C)$ on the LHS axiom’s sub-formula or the opposite on the RHS. Lines may overlap. Note also that, if written in FOL, Skolem functions should appear in the two last NFs in Table 1 (e.g., $\neg r(x,f(x))$ would replace $\exists y \ldots \neg r(x,y)$).

Table 1. Examples of quantification restrictions

Remark 2.

The motivation for relying on these NFs is a two-fold: it saves memory by avoiding redundancies in the matrix, and it helps proving the system’s soundness, completeness and termination, by restricting the problematic cases to 2-lined columns.

Normalized, “purified” TBoxes may add new, introduced concepts; however, they are conservative extensions [5] of their originals, since to every model of the former there is a (sometimes distinct) model of the latter, and validity is preserved. Besides, for these NFs, in the worst case, the number of new concepts grows linearly with the number of impurities; in the average case, this is better than other normalizations (e.g., in [10], the number of new axioms grows linearly with the axioms’ length).

Definition 5

(Cycle, Cyclic/Acyclic Ontologies and Matrices). If A and B are atomic concepts in an ontology O, A directly uses B, if B appears in the right-hand side of a subsumption axiom whose left-hand side is A. Let the relation uses be the transitive closure of directly uses. A cyclic ontology or matrix has a cycle when an atomic concept uses itself; otherwise it is acyclic [1]; e.g., $O = \{ A$ ⊑ $\exists r.B,B$ ⊑ $\exists s.A\}$ is a cyclic ontology. Besides, in acyclic ontologies all subsumption axioms have a concept name in its LHS.

4 The ${\mathcal{ALC}}$ ${\boldsymbol \theta}$-Connection Calculus (${\mathcal{ALC}}$ ${\boldsymbol \theta}$-CM)

The ${\mathcal{ALC}}$ θ-Connection Method (henceforth ${\mathcal{ALC}}$ θ-CM) differs from the FOL Connection Method (CM) by replacing Skolem functions and unification by θ-substitutions, and, just as typical DL systems, employs blocking to assure termination.

Definition 6

(Path, Connection, θ -Substitution, θ -Complementary Connection). A path through a matrix M contains exactly one literal from each clause in M. A connection is a pair of literals {E, ¬E} with the same concept/role name, but different polarities. A θ-substitution assigns each (possibly omitted) variable an individual or another variable. A θ-complementary connection is a pair of ${\mathcal{ALC}}$ literals $\left\{ {E(x), \neg E(y)} \right\}$ or $\left\{ {p(x,v), \neg p(y,u)} \right\}$, with $\theta (x) = \theta (y),\theta (v) = \theta (u)$. The complement $\bar{L}$ of a literal L is E if L = ¬E, and it is ¬E if L = E.

Remark 3

( θ -Substitution). Simple term unification without Skolem functions is used to calculate θ-substitutions. The application of a θ-substitution to a literal is an application to its variables, i.e. $\theta (E) = E(\theta (x))$ and $\theta (r) = r(\theta (x),\theta (y))$, where E is an atomic concept and r is a role. Furthermore, $x^{\theta } = \theta \left( x \right)$.

Definition 7

(Set of Concepts, Skolem Condition). The set of concepts $\tau (x)$ of a variable or individual x contains all concepts that were instantiated by x so far, or, more formally, $\tau \left( x \right) \displaystyle\mathop{=}^{\rm def} \left\{ {E \in N_{C} |E\left( x \right) \in Path} \right\}$. The Skolem condition, ensures that at most one concept is underlined in the graphical matrix form. This condition is formally defined as $\forall a\left| { \left\{ {\underline{{E^{i} }} \in N_{C } |\underline{{E^{i} (a)}} \in Path } \right\} } \right| \le 1$, where i is a column index.

Lemma 1

(Equivalence Between θ -Substitution in ${\mathcal{ALC}}$ θ -CM and Unification in CM for ${\mathcal{ALC}}$ Formulae). θ-substitution is equivalent to unification for ${\mathcal{ALC}}$ formula, i.e., both procedures either return the same results or behave the same way w.r.t. their calculi, when given the same inputs.

Proof.

The cases occurring in ${\mathcal{ALC}}$, all covered by θ-substitution, are in Table 2.

Table 2. Equivalence for ${\mathcal{ALC}}$ between CM unification and θ-substitution in ${\mathcal{ALC}}$ θ-CM

Note that in all cases θ-substitution and unification yield the same substitution or no substitution; the only exception resides in the case where $L_{1} = E\left( x \right)$ and $L_{2} = \neg E\left( {f\left( y \right)} \right)$ ($L_{1} = E, L_{2} = \underline{{\neg E^{i} }}$ in the notation without variables). However, Lemma 2 shows that they are equivalent, in the sense that unification in FOL CM prevents the same connections that ${\mathcal{ALC}}$ θ-CM and θ-unification prevent. ∎

Definition 8

${\bf (}{\mathcal{ALC}}$ Connection Calculus). Figure 3 shows the formal ${\mathcal{ALC}}$ connection calculus (${\mathcal{ALC}}$ θ-CM), adapted from the FOL CM [9]. The rules of the calculus are applied in an analytic, bottom-up way. The basic structure is the tuple $< C,M,Path >$, where clause C is the open sub-goal, M the matrix corresponding to the query $O{ \vDash }\alpha$ (O is an ${\mathcal{ALC}}$ ontology) and Path is the active path, i.e. the (sub-)path currently checked. The index $\mu \in {\mathbb{N}}$ of a clause C ^μ denotes that C ^μ is the μ-th copy of clause C, increased when Cop is applied for that clause (the variable x in C ^μ is denoted x _μ ) – see example of copied clauses in Fig. 8. When Cop is used, it is followed by the application of Ext or Red, to avoid non-determinism in the rules’ application. The Blocking Condition is defined as follows: the new individual $x_{\mu }^{\theta }$ (if it is new, then $x_{\mu }^{\theta } \notin N_{O}$, as in the condition) has its set of concepts $\tau (x_{\mu }^{\theta } )$ compared to the set of concepts of the previous copied individual, i.e., $\tau (x_{\mu }^{\theta } )\;\text{g}\;\tau \left( {x_{\mu - 1}^{\theta } } \right)$ [11], to test if the former is a subset of the latter.

Fig. 3.

The connection calculus ${\mathcal{ALC}}$ θ-CM

Remark 4

${\bf (}{\mathcal{ALC}}$ Connection Calculus). FOL CM already copies clauses, using the indexing function μ; in ${\mathcal{ALC}}$ θ-CM, Cop implements blocking [1], when no alternative connection is available and cyclic ontologies are dealt. It regulates the creation of new individuals, thus preventing non-termination. The Skolem condition solves the FOL cases where the combination of Skolemization and unification correctly prevents connections (see Soundness Theorem below). The Skolem condition is easy to implement: only a flag denoting if each variable/individual in any path contains an underlined concept suffices Finally, in the Ext and Red rules, θ-substitutions replace variables by variables/individuals in the whole matrix. Any individual x can have in its set of concepts τ(x) at most a single concept name with a column index in the matrix (i.e., $\forall a\left| {\left\{ {\underline{{E^{i} }} \in N_{C} | \underline{{E^{i} (a)}} \in Path} \right\}} \right| \le 1$). This restriction avoids the situation in FOL matrices, where unification is tried with distinct Skolem functions (see Lemmas 1, 2).

Example 5

( ${\bf (} {\mathcal{ALC}}$ Connection Calculus). Figures 4 and 5 show the proof of the query from Example 1 using the matrix representation and the formal calculus, respectively.

Fig. 4.

The proof of the query using the graphical matrix representation. Arcs are connections whose labels are the names of the involved individual(s)/variable.

Fig. 5.

The proof of the query using the formal connection calculus, where M is an abbreviation for $M = \{ \left\{ {\underline{h,C} , \neg CO} \right\},\left\{ {O,\underline{h, \neg C} } \right\},\left\{ {O,\underline{{\neg h^{1} }} } \right\},\left\{ {O,\underline{{\neg A^{1} }} } \right\},\left\{ {\neg O\left( a \right)} \right\}, \left\{ {CO\left( a \right)} \right\}\}$ (the double-ended arrow just copies the proof part to save text space).

5 Termination, Soundness and Completeness

Definition 9

(Functional Equivalence Between Decidable Inference Systems w.r.t. a Set of Formulae). An inference system A is functionally equivalent to a system B w.r.t. a set of formulae $\Sigma$ when, for any formula α, ${\Sigma }\,{ \vdash }_{A} \alpha \leftrightarrow {\Sigma }\,{ \vdash }_{B} \alpha$ and ${\varSigma }\,{ \nvdash }_{A} \alpha \leftrightarrow {\varSigma }\,{ \nvdash }_{B} \alpha$.

Lemma 2

(Functional Equivalence Between CM and ${\mathcal{ALC}}$ θ -CM for Acyclic ${\mathcal{ALC}}$ Formulae). ${\mathcal{ALC}}$ θ-CM is functionally equivalent to CM w.r.t. acyclic ${\mathcal{ALC}}$ formulae.

Proof.

Given that (i) Cop is not applied here; (ii) the two systems only differ on the replacement of unification by θ-substitution in the Ext and Red rules; and (iii) θ-substitution is equivalent to unification, Lemma 1 proves all cases but one: a connection with two Skolem functions. The proof for that case is inductive over the matrix structure.

Induction Hypothesis: $O\,{\nvdash}_{CM}\,\alpha$, where the only available connection is between literals with distinct Skolem functions.

Base Case: Suppose a tentative connection between literals with two distinct Skolem functions. For instance, a posed query $\exists r.A$ ⊑ $E,E$ ⊑ $\forall r.a\,{ \vDash }E(a)$, represented in FOL for the CM in Fig. 6a. Unification prevents the connection (denoted by a dotted lined) in the CM. For ${\mathcal{ALC}}$ θ-CM, this connection is forbidden too, due to the Skolem condition. In Fig. 6b, for the new variable y, $\tau \left( y \right) = \{ \underline{{A^{2} }} \}$; so it cannot contain also $\neg \underline{{A^{1} }}$, otherwise it would violate the Skolem condition $(\forall a\left| {\left\{ {\underline{{E^{i} }} \in N_{C} | \underline{{E^{i} (a)}} \in Path} \right\}} \right| \le 1)$.

Fig. 6.

Tentative connection proof for a) $\exists r.A$ ⊑ $E, E$ ⊑ $\forall r.A\,{ \nvdash }_{CM}\,\neg E(a)$, with σ = {y/a} and b) $\exists r.A$ ⊑ $E, E$ ⊑ $\forall r.A\,{\nvdash}_{ALC \theta - CM}\,\neg E\left( a \right)$. Dotted lines stand for forbidden connections.

Inductive Case. Suppose an individual a or a variable x that, in CM, takes part in several connections, two of two in literals with Skolem functions. Then the same behavior from the base case will occur here: CM prevents the last connection ought to unification between two different Skolem functions, while ${\mathcal{ALC}}$ θ-CM avoids the connection on the basis that the Skolem condition is violated. In Fig. 7, the set of concepts of y or a cannot admit two underlined concepts, i.e. $\tau \left( y \right) = \{ \underline{{A^{1} }} \}$, but $\tau \left( y \right) \ne \{ \underline{{A^{1} }} , \underline{{\neg C^{2} }} \}$, again due to the Skolem condition $(\left| {\left\{ {\underline{{E^{i} }} \in N_{C} | \underline{{E^{i} (y)}} \in Path} \right\}} \right| \le 1)$.

Fig. 7.

Tentative ${\mathcal{ALC}}$ θ-CM connection proof for the inductive case

Since the two systems apply the same rules in the same order and the effects of unification in the FOL CM are the same as that of the θ-substitution in ${\mathcal{ALC}}$ θ-CM, the systems are equivalent for the set of acyclic ${\mathcal{ALC}}$ formulae. ∎

Remark 5

(Cyclic Ontologies). Lemma 2 entails that termination, soundness and completeness need only to be proven for the cyclic cases. Lemma 2.22 from [1] states that in a cyclic ontology O, for an individual name x _i  ∊ ABox ${\mathcal{A}}$ of concept E _i (i.e., individual $E_{i} (x_{i} )$ is an assertion), then there is a unique finite sequence of roles $r_{1} , \ldots , r_{i} (i \ge 1)$, a unique finite sequence of i role instances (the so-called role successors) $r_{1} (x_{0} ,x_{1} ), \ldots , r_{i} (x_{i - 1} ,x_{i} )$, and a unique, finite sequence of individual names $x_{1} , \ldots , x_{i - 1}$ that creates x _i for the ${\mathcal{ALCN}}$ tableaux system, as defined by the authors (also holds for ${\mathcal{ALC}}$, since it is a subset of ${\mathcal{ALCN}}$). For the ${\mathcal{ALC}}$ θ-CM, a similar corollary is valid, without needing role successors.

Lemma 3

(Uniqueness of a Generation Sequence). Suppose E _i an ${\mathcal{ALC}}$ concept from a query over a cyclic ontology O, x _i an individual name of concept E _i (i.e.,$E_{i} (x_{i} )$). Then, there is a unique finite sequence of individual names $x_{0} , \ldots , x_{i - 1}$, x _i in a path.

Proof.

Since only one rule is applied at a time, the new concept instance E _i (x _i ) (with the new individual name x _i ) is created in the end of the active path. Since the active path contains the unique sequence $E(x_{0} ), \ldots , E(x_{i - 1} )$, the corollary holds. ∎

On the other hand, it is easy to see why role successors [1, Lemma 2.22] are not needed in ${\mathcal{ALC}}$ θ-CM (for notation ${ \vdash }_{ALC \theta - CM}$ and ${ \vdash }_{CM}$ stand for deductions carried out with ${\mathcal{ALC}}$ θ-CM, CM respectively). Observe the generation of ¬E(c) for the query described as $E\;\text{v}\;\exists r.E{ \vdash }_{ALC \theta - CM} \neg E\left( a \right)$ in Fig. 8: the active path in this case is $\left\{ {\neg E\left( a \right),\neg E\left( b \right), \neg E\left( c \right)} \right\}$. In tableaux systems, role successors ¬r(a, b) and ¬r(b, c) would also need to be created to arrive at ¬E(c).

Fig. 8.

The creation of the unique sequence $\{ \neg E\left( a \right),\neg E\left( b \right),\neg E(c) \}$ to arrive at ¬E(c) for the unfinished query $E$ ⊑ $\exists r.E\,{\nvdash}_{ALC \theta - CM}\,\neg E\left( a \right)$, with $\mu (\{ E,\underline{\neg E} \} ) = 2$

Theorem 1

(Termination). Given M, the matrix representing the arbitrary query $O\,{ \vdash }_{ALC \theta - CM}\,\alpha$, and a chosen initial clause C, any rule sequence in the ${\mathcal{ALC}}$ θ-CM applied over the tuple “$\varepsilon , M, \varepsilon$” terminates.

Proof.

Case (1) $O\,{ \vdash }_{ALC \theta - CM}\,\alpha$, which has itself three sub-cases:

• (a) ${\mathcal{ALC}}$ θ-CM does not apply the Copy rule, and M is proven valid. This case reduces to the last, since the proof is found and has no cycle; then, ${\mathcal{ALC}}$ θ-CM terminates.

• (b) ${\mathcal{ALC}}$ θ-CM uses cyclic axioms, but the Copy rule is only applied with already existent individuals. Again, ${\mathcal{ALC}}$ θ-CM is equivalent to CM, because the already existent individuals are not created by Cop; thus, $x_{\mu }^{\theta } \in N_{O}$, which never meets the blocking conditions. Consequently, the indexing function μ is incremented, the cyclic columns $C_{2}^{\mu }$ are copied, and the process repeats that of the CM. Besides, after the copy, θ-substitutions work just as unifications (Lemma 1). Since CM terminates (see proof at [2, III.6.4.]), ${\mathcal{ALC}}$ θ-CM terminates for this case, too.

• (c) ${\mathcal{ALC}}$ θ-CM uses the cyclic axioms and the Copy rule (Cop) to create new individuals. The blocking condition from Cop ensures termination, given that it prevents Cop to be applied indefinitely, thus generating infinite repetitions of finite sequence(s) of individual names $x_{0} , \ldots , x_{j - 1} ,x_{j}$ in the active path p that would characterize the loop. The blocking condition identifies such repetitions, by checking if the generated concept instances are new individuals names (testing if the new instance is not in the ABox already, i.e., if $x_{\mu }^{\theta } \notin N_{O}$), and if their set of concepts (τ) is changing (by testing whether $\tau (x_{\mu }^{\theta } )\;\text{g}\;\tau \left( {x_{\mu - 1}^{\theta } } \right)$, i.e., if the new instance`s set of concepts is a subset of the set of the previously created instance). If both conditions are met, this active path is blocked; ${\mathcal{ALC}}$ θ-CM runs until a proof is found (see Completeness Theorem below) and halts.

Case (2) $O\;{\nvdash}_{ALC \theta - CM}\;\alpha$, which has two sub-cases:

• (a) The Copy rule is not applied or is applied with existent individuals, not created by previous Copy rule applications (i.e., $x_{\mu }^{\theta } \in N_{O}$), there are open subgoals which make $O\;{\nvdash }_{ALC \theta - CM}\;\alpha$. This case is analogous to cases (1) (a) and (b).

• (b) When the Copy rule creates new x _i individuals, the case is similar to (1) (c). The infinite open cycles are detected by the Copy rule and blocked, and the proof fails due to open subgoals. Hence, ${\mathcal{ALC}}$ θ-CM terminates for this case, and thus, for all cases. ∎

Theorem 2

(Soundness). An ${\mathcal{ALC}}$ formula in the two-lined disjunctive normal form M is valid if there is a connection proof for “$\varepsilon ,M,\varepsilon$” in the ${\mathcal{ALC}}$ θ-CM, i.e. there exists a derivation in which all leaves are axioms.

Proof.

CM is a decision procedure for ${\mathcal{ALC}}$, since ${\mathcal{ALC}}$ corresponds to the decidable FOL fragment L ² [8]. Thus, $O\;{ \vdash }_{CM}\;\alpha$ implies in $O\,\vDash\,\alpha$. Hence, it suffices to prove that $O\;{ \vdash }_{ALC \theta - CM}\;\alpha$ implies in $O\;{ \vdash }_{CM}\;\alpha$. For the cyclic cases and when M originally contains (Skolem) functions, the ${\mathcal{ALC}}$ formulae will be converted to the 2NF and 3NF, respectively $E$ ⊑ $\exists r.\hat{E}( {\text{or }}E$ ⊑ $\hat{E} )$; and $\forall r.\check{D}$ ⊑ $E$ (or $\check{D}$ ⊑ $E$), E being an atomic concept, $\hat{E}$ a pure conjunction and $\check{D}$ a pure disjunction. This case is proved by the contrapositive: $O\,{\nvdash}_{CM}\;\alpha$ must imply in $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$.

The contrapositive proof is by structural induction on the structure of the finite sequence of individual names $x_{1} , \ldots , x_{i - 1}$ that generates the next individual of the cycle x _i . The cases of each of the two normal forms are proven in a similar way, as they differ only in the polarity of the class(es) involved in the existential/universal restriction. Note that in any case, the normal forms only generate columns with two elements, which facilitates the inductive proof. The proof for second normal form comes next. The set of formulae in the first, second, third normal forms is denoted by S _1NF , S _2NF and S _3NF .

Induction Hypothesis: $O\,{\nvdash}_{CM}\;\alpha$, where a ∈ O, S _2NF (also works for S _3NF ).

Base Case: $O = \{ E$ ⊑ $\exists r.E \} \in S_{2DNF } , O\,{\nvdash}_{CM}\;\alpha$, α being an arbitrary formula, e.g. $\alpha = \left\{ {\neg E\left( a \right)} \right\}$, as shown in Fig. 9a, b. After the connection $\{ E\left( x \right),\neg E\left( a \right)\}$, with σ = {x/a}, due to the lack of complement for ¬E(f(x))), first FOL CM copies the second clause increasing this clause’s μ (see Fig. 9a). Then, occurs-check blocks the new connection, and, therefore, $E$ ⊑ $\exists r.E\,{\nvdash}_{CM} \neg E\left( a \right)$.

Fig. 9.

Tentative connection proof, showing that a) $E\,$ ⊑ $\exists r.E\,{\nvdash}_{CM}\;\neg E\left( a \right)$, $\sigma = \{ x/a\}$, with μ({E(x), ¬E(f(x))}) = 1, and that b) $E\,$ ⊑ $\exists r.E\,{\nvdash}_{ALC \theta - CM}\;\neg E\left(a \right)$, with $\mu (\{ E,\underline{\neg E} \} ) = 2$

As for the ${\mathcal{ALC}}$ θ-CM, the case is portrayed in Fig. 9b. The first connection is equal to that of CM (except for applying θ instead of σ). In the second clause $(\{ E,\underline{{\neg E^{1} }} \} ), \underline{{\neg E(b)^{1} }}$ is built as a θ-substitution. Next (not shown in the figure), Cop is applied, and a new clause $\{ E,\underline{{\neg E^{2} }} \}$ appears in M. Then, the connection $\{ \underline{{\neg E(b)^{1} }} ,E(b)\}$ is settled, and instead of generating a new individual name c, b is reused in the new literal E(b) (an alternative test for blocking suggested by Baader et al. [1]). A new clause copy is made, and since the connection $\{ \underline{{\neg E(b)^{2} }} ,E(b)\}$ reappears, the process is blocked and $E$ ⊑ $\exists r.E\,{\nvdash}_{ALC \theta - CM} \neg E\left( a \right)$. The lines below the last matrix represent the fact that each new clause copy shall not represent the same individual instantiated in E, i.e., a new individual must instantiate ¬E. So, for the base case a ∈ O, S _2NF , $O\,{\nvdash}_{CM}\;\alpha$ implies in $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$, q.e.d.

Inductive Case: Suppose $O = \{ E\,$ ⊑ $\exists r.B, B\,$ ⊑ $\hat{E} \}, \alpha = \left\{ {\neg E\left( {y_{0} } \right)} \right\}, \alpha$, α an arbitrary formula), y ₀ an individual name, $\hat{E}$ a pure conjunction that uses E. In that case, $\hat{E}$ is in one of the following forms: $E\,{ \sqcap }\hat{A}, \exists r.\left( {E\,{ \sqcap }\hat{A} } \right)$ or $\exists r.\left( {E\,{ \sqcap }\hat{A} } \right)\,{ \sqcap }\hat{A}$, being $\hat{A},\hat{F}$ also pure conjunctions. In either form, M contains the column $\{ B\left( x \right), \neg E\left( {f(x)} \right)\}$ for CM and $\{ B\left( x \right),\underline{{\neg E(y)^{1} }} \}$ for ${\mathcal{ALC}}$ θ-CM. Therefore, even after pursuing long finite sequences of individual names $x_{1} , \ldots , x_{i - 1}$, CM fails just as in the base case, by occurs-check or looping. Similarly, ${\mathcal{ALC}}$ θ-CM generates $\underline{{\neg E(y_{1} )^{1} }}$ after the first loop and in the next; then, the blocking condition is reached, and ${\mathcal{ALC}}$ θ-CM halts.

For the inductive case where $a \subseteq O, S_{2NF } ,O\,\nvdash_{CM}\;\alpha$ implies in $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$. So, the contrapositive $O{ \vdash }_{ALC \theta - CM}\;\alpha$ implies in $O\,\vDash\,\alpha$ and ${\mathcal{ALC}}$ θ-CM is sound. ∎

Theorem 3

(Completeness). There is a connection proof for “$\varepsilon ,M,\varepsilon$”, i.e.. there exists a derivation in which all leaves are axioms, if the ${\mathcal{ALC}}$ formula F that corresponds to the matrix M is valid.

Proof.

Analogously to the soundness proof, it suffices to prove that if $O\,{\vDash}\,\alpha$ then $O\;{ \vdash }_{ALC \theta - CM}\;\alpha$. To show that, it is enough to demonstrate $O\;{ \vdash }_{CM}\;\alpha$ implies in $O\;{ \vdash }_{ALC \theta - CM}\;\alpha$, again, by the contrapositive: $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$ must imply in $O\,{\nvdash}_{CM}\;\alpha$, when M contains cycles. $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$ has two sub-cases:

• (a) When the Copy rule is not applied or is applied with already existent individual names, not created by previous Copy rule applications (i.e., x ^θ _μ  ∊ N _O ), there are open subgoals which make $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$. This case is analogous to the last case: FOL CM fails with the same open subgoals, and $O\,{\nvdash}_{CM}\;\alpha$ for this case, too. Thus, $O\,{\nvdash}_{CM}\;\alpha$.

• (b) The case when $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$ and the Copy rule creates new x _i instances, can be shown by an inductive proof similar to the one of soundness. The idea is to show that FOL CM loops or finishes by occur-check when blocking takes place in ${\mathcal{ALC}}$ θ-CM for the base and inductive cases. Therefore, when ${\mathcal{ALC}}$ θ-CM fails after exhausting all possible connections and θ-substitutions, CM, by occur-checks and/or loops, is also unable to find a proof, i.e., $O\,{\nvdash}_{CM}\;\alpha$.

Indeed, the soundness theorem has shown that there is a functional equivalence between the two systems for the cyclic case too: ${\mathcal{ALC}}$ θ-CM blocks the cases that CM either loops or halts and vice-versa.

Hence, $O\,{\nvdash}_{ALC \theta - CM}\;\alpha$ implies $O\,{\nvdash}_{CM}\;\alpha$, and ALC θ-CM is complete. ∎

6 Conclusions, Ongoing and Future Work

In the current work, ${\mathcal{ALC}}$ θ-CM is introduced, a connection method for DL that presents two novelties: (i) it replaces Skolem functions and unification by θ-substitutions that emulate the process of creating instances in the model that is typical for DL tableaux systems; and (ii) it introduces a blocking scheme (with a new Copy rule) to deal with cyclic ontologies in order to assure termination.

For the inference process, it employs a normal form that minimizes redundancy in the representation and in the proof search. Moreover, termination, soundness and completeness were proven with the aid of these NFs, which restrict the more convoluted cases to matrix columns of only two literals. This facilitates to portrait the correspondence between FOL unification and θ-substitution/blocking for ${\mathcal{ALC}}$ θ-CM.

For future work, we will tackle cardinality restrictions ($\ge / \le n\;r$ for ${\mathcal{ALCN}}$ and $\ge / \le n\;r.C$ for ${\mathcal{SHQ}}$ ) by dealing with equality between instances. We also aim to create more sophisticated blocking schemes for dynamic and double blocking for DL constructs like inverse roles [7] or dealing with nominals.