Cardinality Restrictions Within Description Logic Connection Calculi

Abstract

Recently, we have proposed the $\theta$-connection method for the description logic (DL) . It replaces the usage of Skolem terms and unification by additional annotation and introduces blocking through a new rule in the connection calculus, to ensure termination in the case of cyclic ontologies. In this work, we enhance this calculus and its representation to take on , an extended fragment that includes role hierarchies, qualified number restrictions and (in)equalities. The main novelty of the calculus lies in the introduction of equality, as well as in the redefinition of connection to accommodate number restrictions, either explicitly or expressed through equality. The new calculus uses the Eq system, thus introducing substitutivity axioms for each concept or role name. The application of Bibel’s equality connections appears here as a first solution to deal with equality.

1 Introduction

Particularly after the appearance of the Semantic Web, Description Logic (DL) [1] has attracted growing attention in the Informatics’ mainstream, with applications in many areas. The possibility of supplying Web users with query answers obtained by complex, albeit decidable reasoning may constitute the main reason for such interest.

At least in the last two decades, the field of DL reasoning has been taken over by tableaux calculi and reasoners. The DL family of languages has spread to include very expressive fragments such as [15]; cutting-edge reasoning performance was accordingly achieved, with the development of DL-specific optimization techniques.

On the one hand, a clear advantage for tableaux calculi against the growing array of DL constructs - which demand particular treatment during reasoning - may lie in its easy adaptability. Dealing with a new construct may only require conceiving a new tableaux rule, maybe along with some optimization companion.

On the other hand, promising methods may have been neglected in such a scenario, in which the tough competition is often focused on gains through optimizations. Therefore, perhaps there is still room available for “basic research” on DL reasoning, in the sense that other efficient calculi need to be adapted to DL, tuned and tested.

Recently, we have embarked in such an endeavor. Departing from the successful first-order logic (FOL) Connection Method (CM) - whose matrix representation provides a parsimonious usage of memory compared to other methods -, we designed, a first connection calculus for DL, the [6]. It incorporates several features of most DL calculi: blocking (implemented by a new rule in connection calculi), lack of variables, unification and Skolem functions.

Moreover, RACCOON [7], the reasoner which embodied this calculus, displayed surprisingly promising performance for an engine which has no DL optimizations. In most of our benchmarking for , it was only clearly surpassed by Konclude [15] (even against FacT ++  [16] and Hermit [8] – see Sect. 5), even considering that these reasoners were designed to face more complex DL fragments than , a disadvantage for them. Nonetheless, this fact corroborates connection calculi as fair, competitive choices for DL ontology querying and reasoning.

In an attempt to extend the expressivity of the ontologies it can cope with, in this work we enhance this calculus and its representation to take on , an extended fragment that includes role number restrictions and (in)equalities. The main novelty lies in the introduction of (in)equalities, as well as the redefinition of connection to accommodate number restrictions, either explicitly or expressed through equalities. The application of Bibel’s eq-connections (equality connections) [4] appears here as a first solution to deal with (in)equalities, although cardinality restrictions do not need equality connections, once, in this case, an equality connects only to an inequality, given a proper $\theta$-substitution for the pair is available. Surely, there are other more efficient solutions to dealing with equality, such as paramodulation [13] and RUE (Resolution and Unifications with Equality) [5], not to speak on the many advanced techniques already applied in the DL setting. The aim of the new calculus is providing a first solution and roadmap on how to deal with equality and number restrictions, based on its semantics.

The text is organized as follows. Section 2 provides an explanation of the FOL CM. Section 3 introduces ; its normalization is shown in Sect. 4. Section 5 explains our formal connection calculus for . Section 6 discusses related work on equality handling in FOL and DL. Section 7 concludes the article. The calculus’ termination, soundness and completeness are proven in www.cin.ufpe.br/~fred/RR.pdf.

2 The Connection Method

The connection method has a long tradition in automated deduction. Conceived by W. Bibel in the early 80’s, it is a validity procedure (opposed to refutation procedures like tableaux and resolution), i.e., it tries to prove whether a formula, theorem or query is valid. It consists of a matrix-based deduction procedure designed to be economical in the use of memory, as it is not generative as tableaux and resolution, in the sense that it does not create intermediary clauses or sentences during proof search. We explain how it works below, preceded by necessary definitions.

A (first-order) literal, denoted by $L$, is either an atomic formula or its negation. The complement $\neg L$ of a literal $L$ is $P$ if $L$ is of the form $\neg P$, and $\neg L$ otherwise. A formula in disjunctive normal form (DNF) is a disjunction of conjunctions (like $C_{1} \vee \ldots \vee C_{n}$), where each clause $C_{i}$ has the form $L_{1} \wedge \ldots \wedge L_{m}$ and each $L_{i}$ is a literal. The matrix of a formula in DNF is its representation as a set $\left\{ {C_{1} , \ldots ,C_{n} } \right\}$, where each $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.

2.1 Method Representation

Suppose we wish to entail whether $KB\,\,{ \vDash }\,\,\alpha$ is valid using a direct method, like the Connection Method (CM). By the Deduction Theorem [3], we must then prove directly $KB \to \alpha$, or, in other words, if $\neg KB \vee \left\{ \alpha \right\}$ is valid. This opposes to classical refutation methods, like tableaux and resolution, which builds a proof by testing whether $KB \cup \left\{ {\neg \alpha } \right\}\,\,{ \vDash } \,\, \bot$. Hence, in the CM, the whole knowledge base $KB$ should be negated, including instantiated predicates, like $A\left( a \right)$, where $a$ is a constant or individual. Given $KB = \left\{ {\alpha_{1} ,\alpha_{2} , \ldots ,\alpha_{n} } \right\}, \alpha_{i}$ being FOL formulae, in this work we define query as a matrix $\neg KB \vee \left\{ \alpha \right\}$ (i.e., $\neg \alpha_{1} \vee \neg \alpha_{2} \vee \ldots \vee \neg \alpha_{n} \vee \alpha$) to be proven valid, where $\alpha$ is the query consequent. A query represented in this way is said to be in positive DNF.

Besides, the effects for a negated $KB$ in a DNF representation are: (i) axioms of the form $E \to D$ (in DL, $E\,{ \sqsubseteq }\,D$) translate into $E \wedge \neg D$; (ii) in a matrix, variables are existentially quantified; (iii) FOL Skolemization works over universally quantified variables, instead of existentially ones; and (iv) the consequent $\alpha$ is not negated.

Example 1 (Query, positive DNF, clause, matrix).

The query

$$ \begin{aligned} & \{ \forall w \;Animal \left( w \right) \wedge \exists z \left( {hasPart\left( {w,z} \right) \wedge Bone\left( z \right)} \right) \to Vertebrate\left( w \right), \forall x\, Bird\left( x \right) \to \\ & Animal\left( x \right) \wedge \exists y \left( {hasPart\left( {x,y} \right) \wedge Bone\left( y \right)} \right) \wedge \exists v \left( {hasPart\left( {x,v} \right) \wedge Feather\left( v \right)} \right)\} \\ & { \vDash }\,\,\forall t \,Bird\left( t \right) \to Vertebrate\left( t \right) \\ \end{aligned} $$

is represented by the following positive DNF matrix and graphical matrix, where variables $y, v$ and $t$ were skolemized by functions $f\left( x \right), g\left( x \right)$ and constant $c$ (Fig. 1):

Fig. 1.

A FOL query in disjunctive clausal form represented as a matrix and graphical matrix (with literals abridged, e.g. $A\left( w \right)$ stands for $Animal\left( w \right)$, etc.)

2.2 Method Intuition and Functioning

We have represented a FOL query in DNF with clauses as columns, i.e., we are dealing with the matrix vertically. If we change our perspective, traversing the matrix horizontally in all possible ways (or paths), with each column supplying only one literal in a path, and group these paths conjunctively, we are indeed converting the query to the conjunctive normal formal (in the most inefficient way). For instance, in the matrix above, two of the paths are (randomly) listed below:

$$ \begin{aligned} & \left\{ {A\left( w \right), B\left( x \right),B\left( x \right), \neg Bo\left( {f\left( x \right)} \right), \neg h\left( {x,g\left( x \right)} \right), B\left( x \right), \neg B\left( c \right), V\left( c \right)} \right\} \\ & \left\{ {h\left( {w,z} \right), \neg A\left( x \right),B\left( x \right), \neg Bo\left( {f\left( x \right)} \right),\neg h\left( {x,g\left( x \right)} \right), \neg F\left( {g\left( x \right)} \right), \neg B\left( c \right), V\left( c \right)} \right\}. \\ \end{aligned} $$

The conjunctive formula would look like (with all variables quantified):

$$ \begin{aligned} & \ldots \wedge \left( {A\left( w \right) \vee B\left( x \right) \vee B\left( x \right) \vee \neg Bo\left( {f\left( x \right)} \right) \vee \neg h\left( {x,g\left( x \right)} \right) \vee B\left( x \right) \vee \neg B\left( c \right) \vee V\left( c \right)} \right) \wedge \ldots \\ & \wedge \left( {h\left( {w,z} \right) \vee \neg A\left( x \right) \vee B\left( x \right) \vee \neg Bo\left( {f\left( x \right)} \right) \vee \neg h\left( {x,g\left( x \right)} \right) \vee \neg F\left( {g\left( x \right)} \right) \vee \neg B\left( c \right) \vee V\left( c \right)} \right) \wedge \ldots \\ \end{aligned} $$

It is now easy to see that such a formula (or matrix) is valid iff every path has a connection, i.e., a $\sigma$-complimentary pair of literals, where $\sigma$ is the (most general) unifier between them. For instance, the first path above is true, once it contains the valid sub-formula $B\left( x \right) \vee \neg B\left( c \right)$, with $\sigma = \left\{ {x/c} \right\}$; the second is true because it has the sub-formula $h\left( {w,z} \right) \vee \neg h\left( {x,g\left( x \right)} \right)$, with $\sigma = \left\{ {x/c, w/c,z/g\left( c \right)} \right\}$, and so on.

The method then must check all paths for connections in a systematic way. Note that a connection prunes many paths in a single pass, due to the matricial arrangement of clauses, a relevant source of reasoning efficiency.

Example 2 (Connection Method).

Figure 2 shows the step-by-step query solution. The reader may note, e.g., that the first connection (step 1) solves 16 paths.

Fig. 2.

The query solution, with literals abridged. Arrows stand for pending sets of literals.

Each connection can create up to two sets of literals still to be solved, one in each clause (column) involved in the connection. The first of these literals in each clause is marked in each step of the Figure with an arrow.

Otten [11] proposed a “sequent-style” calculus formalization, alternatively to the graphical matricial one. Our calculus is based on his; it is explained in Sect. 5.

3 The Description Logic

An ontology in is a set of axioms over a signature $\Sigma = \left( {N_{C} ,N_{R} ,N_{O} } \right)$, 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), and $N_{O}$ is the set of individual names (constants) [1]. The sets are mutually disjoint. The set of concept expressions (C) is recursively defined as follows (with $n \in {\mathbb{N}}^{*}$, and $C$ a concept expression, i.e., $C \in$ C):

$$ C\,:: = N_{C} \left| { C\,{ \sqcap }\,C} \right|C\,{ \sqcup }\,C\left| {\neg C} \right|\exists r.C\left| {\forall r.C\left| { \ge n r} \right.} \right| \ge n r.C\left| { \le n r} \right| \le n r.C $$

allows for a set of basic axioms (TBox, RBox), and a set of axioms of a particular situation (ABox). In the definitions below a, b $\in N_{O} , r,s \in N_{R} , D,E \in$ C and $i,n \ge 1$. A TBox axiom is a subsumption like D ${ \sqsubseteq }$ E; an RBox one is like $r\; \subseteq \;s$; and an ABox is a finite set of assertions (or instances) of three types: (i) concept assertions like $C\left( a \right)$; (ii) role assertions $r\left( {a,b} \right)$; (iii) (in)equality assertions $a = b$ (or $a \ne b$). An ontology O is an ordered tuple

An interpretation I has a domain $\Delta ^{I}$ and an interpretation function $.^{I}$ that maps to every $A$ $\in N_{C}$ a set ${\text{A}}^{I} \, \subseteq \,\Delta ^{I}$; to every $r \in N_{R}$ a relation $r^{I} \, \subseteq \,\Delta ^{I} \, \times \,\Delta ^{I}$; and to every $a \in N_{O}$ an element $a^{I} \in$ $\Delta ^{I}$. The function $.^{I}$ extends to concepts as depicted in Table 1.

Table 1. Syntax and semantics of constructors

An interpretation I satisfies an axiom $\alpha \left( {I\,{ \vDash }\,\alpha } \right)$ iff all I axioms and $\alpha$ are satisfied, i.e., I satisfies C ${ \sqsubseteq }$ D iff $C^{I} \, \subseteq \,D^{I} , C\left( a \right)$ iff $a^{I} \, \in \,C^{I}$, $r\left( {a,b} \right)$ iff $\left\langle {a,b} \right\rangle \in r^{I} , r\; \subseteq \;s$ iff $r^{I} \; \subseteq \;s^{I}$. $O$ entails $\alpha \left( {O\,{ \vDash }\,\alpha } \right)$ iff every model of $O$ is also a model of α. In this paper, variables are denoted by x, y, z, possibly with subscripts. Terms are variables or individuals.

4 Normal Form and Matrix Representation for

Matrices with (qualified) number restrictions can be represented in two ways: the abridged form, i.e., with the number restrictions explicit, and the expanded form, with number restrictions substituted by axioms containing concepts, roles and (in)equalities that correspond to the semantic definitions. Besides, to take on (in)equalities, substitutivity axioms (e.g., $\forall x\forall y \left( {x = y} \right) \to (E\left( x \right) \to E\left( {y)} \right)$ for concept names, and $\forall x\forall y\forall z\forall k \left( {x = z} \right) \wedge \left( {y = k} \right) \to \left( {r\left( {x,y} \right) \to r\left( {z,k} \right)} \right)$ for role names) are represented as clauses for every concept and role name in the query.

Next, the matrix is converted to a specific DNF, introduced here. This DNF, with definitions concerning representation as matrices for the calculus, is presented below.

Definition 1 ( literal, formula, clause, matrix).

are atomic concepts or roles, possibly negated and/or instantiated, or (in)equalities. Literals involved in universal or existential restrictions are underlined. In case a restriction involves more than one clause, literals are indexed (in the top of the literal) with a same new column index number. An formula in 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}$, with each $L_{i}$ being a literal. The matrix of an formula in DNF is 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}$.

Definition 2 (Substitutivity clauses, graphical matrix).

matrices representing number restrictions also contain substitutivity clauses for every concept and role name, in the forms $\left\{ {x \ne y, E\left( x \right),\neg E\left( y \right)} \right\}$ and $\left\{ {x \ne z,y \ne k,r\left( {x,y} \right),\neg r\left( {z,k} \right)} \right\}$ with $E \in N_{C} , r \in N_{R}$.

In the graphical matrix representation, clauses are represented as columns, and restrictions as lines; restrictions with indexes are horizontal; without are vertical (see Example 3 – substitutivity axioms are not presented). Literals participating in a universal restriction in an axiom’s left-hand side (LHS) or in an existential restriction in the right-hand side (RHS) are underlined; otherwise, they are sidelined.

Example 3 (Query, clause, matrix, abridged/expanded forms).

Figure 3 shows query $O = \left\{ {{ > }1\, {\text{hasPart}}.{\text{Wheel}}\,{ \sqsubseteq }\,{\text{Vehicle}}, \;\, {\text{Car}}\,{ \sqsubseteq }\, \ge 3\, {\text{hasPart}}.{\text{Wheel}}} \right\},\;\, \alpha = \,{\text{Car}}\,{ \sqsubseteq }\,{\text{Vehicle}}$ in abridged form. The index marks clauses involved in a same restriction).

Fig. 3.

The query from Example 1 represented as an matrix in abridged form

The negations in literals $\underline{{ < 3 \neg {\text{hasPart}}^{1} }}$ and $\underline{{\neg {\text{Wheel}}^{1} }}$ constitute merely a notational convention that facilitates the connections. They reflect the transformation to the expanded form, where these literals are converted into negated literals and equalities.

The number restriction expanded form, according to the semantics defined in Table 1, replaces $\underline{{ > 1{\text{hasPart}},\, {\text{Wheel}}}}$ by ${\text{hasPart}}\,\left( {{\text{x}},{\text{y}}_{1} } \right)\,{ \sqcap }\,{\text{Wheel}}\left( {{\text{y}}_{1} } \right)\,{ \sqcap }\,{\text{hasPart }}\left( {{\text{x}},{\text{y}}_{2} } \right)\,{ \sqcap }\,{\text{Wheel}}\left( {{\text{y}}_{2} } \right) \wedge {\text{y}}_{1} \ne {\text{y}}_{2}$ and $\underline{{ < 3 \;\neg {\text{hasPart}}^{1} }}$ by ${\bigwedge }_{{{\text{i}} = 1}}^{3} \,{\text{hasPart}}\,\left( {{\text{x}},{\text{v}}_{\text{i}} } \right)\,{ \sqcap }\,{\text{Wheel}}\left( {{\text{v}}_{\text{i}} } \right)\,{ \sqcap }{\text{v}}_{1} \ne {\text{v}}_{2} \,{ \sqcap }\,{\text{v}}_{1} \ne {\text{v}}_{3} \to {\text{v}}_{2} = {\text{v}}_{3}$ before creating the matrix. The resulting matrix is depicted in Fig. 4. For the sake of space, substitutivity axioms are not shown.

Fig. 4.

Same example in expanded form, showing the (in)equalities (again, literals are abridged, i.e., ${\text{C}}$ means ${\text{Car}}, {\text{h}}$ means ${\text{hasPart}}$, etc.)

Definition 3 (Impurity, pure conjunction/disjunction).

Impurity in an 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 Definition in [6]).

Example 4 (Impurity, pure conjunction/disjunction).

(a) $\exists r.A$ and $\mathop {\bigwedge }\nolimits_{i = 1}^{n} A_{i}$ are PCs if A and each $A_{i}$ are also PCs; (b) $(\forall r.\left( {D_{0} \,{ \sqcup } \ldots { \sqcup }\,D_{n} \,{ \sqcup }\left( {E_{0} \,{ \sqcap } \ldots { \sqcap }\,E_{m} } \right)\,{ \sqcup }\,\left( {A_{0} \,{ \sqcap } \ldots { \sqcap }\,A_{p} } \right)} \right)$ is not a PD, as it contains two impurities: $\left( {E_{0} \,{ \sqcap } \ldots { \sqcap }\,E_{m} } \right)$ and $\left( {A_{0} \,{ \sqcap } \ldots { \sqcap }\,A_{p} } \right).$

Definition 4 (Two-lined disjunctive normal form).

An axiom is in two-lined DNF iff it is in DNF and in one of the following normal forms (NFs): $\left( {\text{i}} \right)\,\widehat{E} { \sqsubseteq } \check{D};$ $\left( {\text{ii}} \right)\,E\, { \sqsubseteq }\,\widehat{E}; \left( {\text{iii}} \right)\,\check{D}\, { \sqsubseteq }\,E,$ where E is a concept name¹ $\widehat{E }$ is a PC, and $\check{D}$ is a PD.

Example 5 (Two-lined disjunctive normal form).

The axioms (i) $\widehat{E}\,{ \sqsubseteq }\,\check{D};$ (ii) $E\,{ \sqsubseteq }\,\exists r.\widehat{E}$ and (iii) $\forall r.\check{D}\,{ \sqsubseteq }\,E,$ where $\widehat{E} = \mathop {\bigwedge }\nolimits_{i = 1}^{n} E_{i}$ and $\check{D} = \mathop {\bigvee }\nolimits_{j = 1}^{m} D_{j}$ (Fig. 5).

Fig. 5.

Examples of the three two-lined normal forms’ representations in

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\, { \sqsubseteq }\,\exists r.B,B\,{ \sqsubseteq }\,\exists s.A\}$ is cyclic.

5 The

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

Besides, equality connections, proposed by Bibel [4], are needed here as a first attempt to address (in)equalities, and thus (qualified) cardinality restrictions. The idea is to include substitutivity axioms for each concept and role name, e.g., for concept P: $x = y \to \left( {\,P\left( x \right), \to \,P\left( y \right)} \right)$, represented as a single column $\left\{ {x = y,\,P\left( x \right),\neg \,P\left( y \right)} \right\}$

Moreover, expands the notion of connection to include equality, which is used to express number restrictions. An ontology represented as a matrix with the equalities is said to be in the expanded form and is explained in the next section. The abridged form, with number restrictions without equalities, is tackled in Subsect. 4.2.

5.1 Expanded Form - Representation and Reasoning

Definition 6 (Path, connection, $\varvec{\theta}$-substitution, $\varvec{\theta}$-complementary connection).

A path through a matrix M contains exactly one literal from each clause/column in M. A connection is a pair of literals in three forms: (i) $\left\{ {E, \neg E} \right\}$ with the same concept/role name, instantiated with the same instance(s) or not; (ii) $\left\{ {x = y,x \ne y} \right\}$, with $x$ and $y$ instantiated with the same instance or not. A $\theta$-substitution assigns each (possibly omitted) variable an individual or another variable, in an literal. A $\theta$-complementary connection is a pair of literals $\left\{ {E\left( x \right), \neg E\left( y \right)} \right\}$ or $\left\{ {p\left( {x,v} \right), \neg p\left( {y,u} \right)} \right\}$, with $\theta \left( x \right) = \theta \left( y \right),\,\theta \left( v \right) = \theta \left( u \right)$. The complement $\overline{L}$ of a literal $L$ is $E$ if $=$ $\neg E$, and it is $\neg E$ if $L =$ $E$.

Remark 1 ($\varvec{\theta}$-substitution).

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

Definition 7 (Set of concepts).

The set of concepts $\tau \left( x \right)$ of a term $x$ contains all concept names instantiated by $x$ so far, defined as $\tau \left( x \right)\,\underline{\underline{\text{def}}} \,\left\{ {E \in N_{C} |E\left( x \right) \in Path} \right\}$.

Definition 8 (Skolem condition).

The Skolem condition ensures that at most one concept name is underlined for each term in the graphical matrix form. If i is an index, this condition is defined as $\forall a\;|\,\{ \underline{{E^{i} }} \in N_{C } \left| {\underline{{E^{i} \left( a \right)}} } \right. \in Path\} \, |\, \le 1$.

Definition 9 ( connection calculus).

Figure 6 brings the formal connection calculus , adapted from the FOL CM [11]. 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 ⊨ $\alpha$ (O is an ontology) and Path is the active path, i.e. the (sub-)path being currently checked. The index $\mu \in {\mathbb{N}}$ of a clause $C^{\mu }$ denotes that $C^{\mu }$ is the $\mu$-th copy of clause C, increased when Cop is applied for that clause (the variable x in $C^{\mu }$ is denoted $x_{\mu }$) – see example of copied clauses in Fig. 13$a$. When Cop is applied, it is followed by the application of Ext or Red, to avoid non-determinism in the rules’ application. The Blocking Condition states that, when a cycle finishes, the last new individual $x_{\mu }^{\theta }$ (if it is new, then $x_{\mu }^{\theta } \notin N_{O}$, as in the condition) has a set of concepts $\tau (x_{\mu }^{\theta } )$ which is not a subset of the set of concepts of the previous copied individual, i.e., $\tau (x_{\mu }^{\theta } )\,\nsubseteq\,\tau \left( {x_{\mu - 1}^{\theta } } \right)$ [14]. If this condition is not satisfied, blocking occurs.

Fig. 6.

The connection calculus

Lemma 1 (Matrix characterization).

A matrix M is valid iff there exist an index $\mu$, a set of $\theta$-substitutions $\left\langle {\theta_{i} } \right\rangle$ and a set of connections $S$, s.t. every path through $M^{\mu }$, the matrix with copied clauses, contains a $\theta$-complementary connection $\left\{ {L_{1}^{\theta } ,L_{2}^{\theta } } \right\} \in S$, i.e. a connection with $\theta \left( {L_{1} } \right) = \theta \left( {\overline{{L_{2} }} } \right)$. The tuple $\left\langle \mu \right.,\left\langle {\theta_{i} } \right\rangle ,\;\left. S \right\rangle$ is called a matrix proof.

Clause copying and its multiplicity $\mu$ already existed in the original CM, but neither a copy rule nor blocking were necessary, as FOL is semi-decidable. To regain termination, the new Copy rule implements blocking [1], when no alternative connection is available and cyclic ontologies are being processed. The rule regulates the creation of new individuals, blocking when infinite cycles are detected. The Skolem condition solves the FOL cases where the combination of Skolemization and unification correctly prevents connections (see Soundness Theorem in WWW.cin.ufpe.br/~fred/RR.pdf).

In the Ext and Red rules, $\theta$-substitutions replace implicit variables by terms in the current path. A restriction avoids the situation in FOL matrices, where unification is tried with distinct Skolem functions: any individual $x$ can have in its set of concepts $\tau \left( x \right)$ at most a single concept name with a column index in the matrix, stated by the condition $\forall a\,\left| { \left\{ {\underline{{E^{i} }} \in N_{C } \left| {\underline{{\,E^{i} \left( a \right)}} } \right. \in Path} \right\}} \right| \, \le 1$.

Example 6 ( connection calculus).

Figures 7 and 8 show the proof of the query from Example 1 using the matrix representation and the calculus, respectively.

Fig. 7.

The query’s proof in graphical matrix representation. Arcs are connections whose labels are the names of the involved individual(s)/variable(s). Arrows indicate pending literals’ lists.

Fig. 8.

The proof of the query using the calculus, where M is an abbreviation for $\{ \{ \underline{{{\text{h}}, {\text{W}}\left( {{\text{y}}_{1} } \right)}} ,$ $\underline{{{\text{h}},{\text{W}}\left( {{\text{y}}_{2} } \right)}} ,\,{\text{y}}_{1} \ne {\text{y}}_{2} ,\neg {\text{V}}\} , \{ {\text{C}},\;\underline{{\neg {\text{h}}^{1} }} \} \} ,$ $\{ {\text{C,}}\; \underline{{\neg {\text{W}}\left( {{\text{v}}_{1} } \right)^{1} }} \} , \{ {\text{C, }} \underline{{\neg {\text{h}}^{2} }} \} \} , \{ {\text{C,}} \underline{{\;\neg {\text{W}}\left( {{\text{v}}_{2} } \right)^{2} }} \} , \{ {\text{C, }} \underline{{\neg {\text{h}}^{3} }} \} \} ,$ $\{ {\text{C,}}\underline{{\;\neg {\text{W}}\left( {{\text{v}}_{3} } \right)^{3} }} \} ,\;\left\{ {{\text{C}}, {\text{v}}_{1} = {\text{v}}_{2} } \right\},\;\left\{ {{\text{C}},\,\,\,{\text{v}}_{1} = {\text{v}}_{3} } \right\},$ $\left\{ {{\text{C}},\;\;{\text{v}}_{2} = {\text{v}}_{3} } \right\},\;\left\{ {{\text{V}}\left( {\text{a}} \right)} \right\},\;\left\{ { \neg {\text{C}}\left( {\text{a}} \right)} \right\}\}$. The double-ended arrow just copies the proof part to save text space.

Furthermore, when equality between pairs of individuals are being dealt, equality connections [4] with substitutivity axioms, in explicit or implicit form, can be relied upon. One can solve, e.g., $\left\{ {P\left( a \right),a = b} \right\}{ \vDash }P\left( b \right)$, as portrayed in Fig. 9. Figure 9(i) displays the equality connections performed in the usual way, with the introduction of the substitutivity axiom P: $x = y \to \left( {P\left( x \right) \to P\left( y \right)} \right)$ (represented as the column $\left\{ {x = y, P\left( x \right),\neg P\left( y \right)} \right\}$), while Fig. 9(ii) presents the same connection in an abridged way.

Fig. 9.

(i) A connection using the substitutivity axiom; (ii) an equality connection [4]

This subject naturally leads to the representation of number restrictions connections in the abridged form, deployed in the next subsection.

5.2 Abridged Form - Representation and Reasoning

(Qualified) number restrictions can be in abridged form ($\ge \,\left| {\, \le nr} \right.\left( {.C} \right)$ with $n \in {\mathbb{N}}^{*}$). In this case, one should note that $\neg \left( { \ge n r} \right) = \le \left( {n - 1} \right) r$ and $\neg \left( { \le n r} \right) = \ge \left( {n + 1} \right) r$.

Definition 10 (Number restriction literal).

Number restriction literals are literals representing (qualified) number restrictions. They can be negated and/or instantiated, and/or under- or sidelined or with no line. In case a restriction involves more than one clause, literals are top indexed with a same new column index number.

Definition 11 (Number restriction valid interval).

Two number restrictions form a valid interval iff their numerical restrictions share an intersection, e.g. >5r, <8 $\neg r$.

Definition 12 (Number restriction $\theta$-substitution, $\theta$-complementary number restriction connection).

Let $A$ and $B$ be two number restriction literals, $\le | \ge n r$ and $\ge | \le m \;\neg r$, instantiated or not, representing role instance sets $\left\langle {r\left( {x, y_{1} } \right), \ldots ,r\left( {x, y_{n} } \right)} \right\rangle$ and $\left\langle {r\left( {z, w_{1} } \right), \ldots ,r\left( {z, w_{m} } \right)} \right\rangle$, with a valid interval between them ($vi$). A number restriction $\theta$-substitution for the pair is a mapping $\theta$, s.t. $\theta \left( x \right) = \theta \left( y \right), \theta \left( {y_{i} } \right) =\uptheta\left( {w_{i} } \right)$, with $i = 1$ to $\hbox{min} \left( {vi} \right)$. A $\theta$-complementary number restriction connection is a pair of number restriction literals over a same role in the form $\left\{ { \le \left| {\, \ge n\, r, \ge \,} \right| \le m\; \neg r} \right\}$, that, under a number restriction $\theta$-substitution, share a valid interval $vi$.

A connection represents a tautology, e.g. $E\,{ \sqcup }\,\neg E$. For number restrictions, this means a valid interval, as, for example, any individual possessing any number of role instances (including 0) with r satisfies the restriction >5r${ \sqcup }$ <8r. If there is a “hole”, for instance, >8r${ \sqcup }$ <5r, then individuals with 5 to 8 role instances of r would not satisfy the restriction, and the latter cannot be a tautology. Recall that <8r is represented as <8 $\neg r$, only to facilitate the connections to be settled.

Example 6 ( connection calculus, abridged form).

Figures 10 and 11 display the proof from Example 2 in the abridged form, using the graphical matrix representation and the formal calculus. Note that $\hbox{min} \left( {{ > }1 \,{\text{hasPart}}, { < }3 \,\neg {\text{hasPart}}} \right) = 2$.

Fig. 10.

Proof of Example 2 in the abridged form. $\langle \left( {a,{\text{v}}_{\text{i}} } \right)\rangle,\,{\text{i}} = 1,2$ is a set of two role instances and ${\text{v}}_{\text{i}} ,{\text{i}} = 1,2$ is a set of two instances (of concept Wheel).

Fig. 11.

The proof of Example 2 using the calculus, with $M = \{ \{ > 1{\text{hasPart}},{\text{Wheel}},\neg {\text{Vehicle}}\} ,$ $\{ {\text{Car}}, \underline{{ < 3 \;\neg {\text{hasPart}}^{1} }} \} ,\,\{ {\text{Car}},\,\underline{{\neg {\text{Wheel}}^{1} }} \} , \, \left\{ {{\text{Vehicle}}\left( {\text{a}} \right)} \right\}, \, \{ \neg {\text{Car}}\left( {\text{a}} \right)\} \}$ (literals are abbreviated)

The abridged form can easily accommodate number restrictions with role hierarchies, if connections between number restrictions and role axioms exist.

Example 7 (Number restrictions, role hierarchies).

$O = \left\{ { > 2 \,{\text{hasPart}}.{\text{Wheel}}\,{ \sqsubseteq }\,{\text{Car},}} \right.$ $\,{\text{hasComponent}}\, \subseteq \,{\text{hasPart}} ,{\text{Truck}}\,{ \sqsubseteq }\, \ge 6\, {\text{hasPart}}.{\text{Wheel}}\} ,\, \alpha = {\text{Truck}}\,{ \sqsubseteq }\,{\text{Car}}.$

This query is represented by $M = \{ \{ \underline{{ > \,2\,{\text{ hasPart}},{\text{Wheel}},\,}} \neg {\text{Car}}\} ,\{ {\text{hasComponent }},$

$$ \neg {\text{hasPart}}\} ,\,\left\{ {{\text{Truck}},\underline{{ < 5\; \neg {\text{hasComponent}}^{1} }} } \right\} ,\,\left\{ {{\text{Truck}}, \,\underline{{\neg {\text{Wheel}}^{1} }} } \right\},\,\left\{ {\neg {\text{Truck(a)}}} \right\} ,\,\left\{ {{\text{Car}}\left( {\text{a}} \right)} \right\}. $$

Figure 12 brings the proof for M, with $\hbox{min} \left( { > 2 \,{\text{hasPart}}, < 5 \,{\text{hasPart}}} \right) = 3$.

Fig. 12.

Proof with number restrictions and a role hierarchy axiom

6 Discussion

Matricial inference methods, such as the CM, presents a few advantages over other methods, as well as some drawbacks. We will discuss our method, at first in the light of memory handling and existent solutions to solve equality equations in the context of FOL. Next, we briefly comment some recent comparative performance of our reasoner, RACCOON (ReAsoner based on the Connection Calculus Over ONtologies) against well-known DL reasoners [7], and existent solutions for number restrictions within the DL scenario, followed by a small discussion on next steps.

As for memory usage, in the CM, matrices require only a copy of the matrix and data structures to store the current path, the pending clauses and literals, the unifier and literal’s indices. It does not generate any intermediary results; this constitutes an interesting benefit in terms of memory usage over generative methods such as resolution or tableaux, which create intermediary clauses and sub-formulae.

Indeed, dealing efficiently with memory with cyclic ontologies is crucial for a DL reasoner, since a number of fragments (including ) have been proven PSpace-complete [1]. Our calculus processes cycles (thanks to the Copy rule), saving memory due to keeping only one copy of the matrix in memory [3, 4]. The other copies are virtual, i.e., only the index $\mu$ is created or incremented and stored, together with the $\theta$-substitution and the current path. The next example portraits this case.

Example 8 (Cycles).

$O = \{ \exists {\text{hasSon}}.\left( {{\text{Dr}}\,{ \sqcup }\, {\text{DrAncestor}}} \right){ \sqsubseteq } \,{\text{DrAncestor}}, {\text{hasSon}}({\text{ZePadre}},$ ${\text{Moises}}), {\text{hasSon }}\left( {{\text{Moises}},{\text{Luiz}}} \right), {\text{hasSon }}\left( {{\text{Luiz}},{\text{Fred}}} \right), {\text{Dr }}\left( {\text{Fred}} \right)\} ,\alpha = {\text{DrAncestor}}\left( {\text{ZePadre}} \right).$ This cyclic query has its proof represented by both Figs. 13a and b.

Fig. 13.

Proof representations of a cyclic query, with $\left( a \right)$ explicit and $\left( b \right)$ implicit copies

Figure 13a brings an explicit copy of the second clause, needed for the proof. On the other hand, Fig. 13b incorporate indices to denote how the only copy was used with different individuals and instantiations. At least in theory, such idea exists in the CM, called implicit amplification [3]; we adopted it in RACCOON with the same notation, and gain memory with its procedure.

Clausal inference methods require normal forms, in which transformations apply over formulae to produce clauses over which the method works. On the one hand, clause manipulation accelerates reasoning in reasonably expressive logics, e.g., FOL. On the other hand, the drawbacks are at least two-fold.

First, literals’ redundancy among clauses often constitutes an overhead in large knowledge bases. In the CM, matrix representation minors the problem during reasoning, as the method is non-generative; anyway, it remains if, in an initial query representation in DNF, clauses share too many literals. For the , the two-lined normal form reduces this type of redundancy at the expense of introducing a small number of new symbols. To sum up, the best solution consists in applying a non-clausal connection method [12], where matrices can be nested.

Another problem for clausal calculi resides on adapting to an increasing set of constructs in DL: each new construct to be inserted into the calculi requires careful analysis, and frequently changes in the existing rules. This problem also plagues equality approaches in clausal systems. Consolidated solutions from saturation-based reasoning, such as paramodulation [13], are hard to be integrated, and the former is not complete for the connection method [11]. Nevertheless, an equality approach based on RUE (Resolution with Unification and Equality) [5] seems plausible for connection calculi but has not been tried yet. Our aim in formalizing our calculus with the Eq system is paving the way for such more efficient solutions.

Although the Eq system is not yet coded in RACCOON, the goal-oriented search embodied by the connection calculus, together with its economical approach to memory, made the reasoner display unexpected fair results for consistency, compared to Hermit, FacT++ and Konclude. A summary of the benchmarking conducted over the ORE 2014 and 2015 baselines is deployed in Fig. 14 [7].

Fig. 14.

Comparison of RACCOON and ORE competitors for consistency on the ORE 2014 and 2015 baselines ( ontologies)

In the baselines, ontologies were ranked by size and expressivity. RACCOON exhibited the fastest results (side by side with Konclude) in smaller and less complex ontologies; however, against the larger and more complex set (the last ones), results start to decay (in a graceful fashion), probably due to the lack of DL optimizations. Furthermore, in the first experiment, RACCOON’s performance fell short in ontologies in the presence of a certain structure where cycles occur inside other cycles massively. Apart from that, the results seem promising, given the possibility of implementing reductions built in other competitors.

When faced with number restrictions and their equalities, the idea is applying the abridged form first, which demand less steps and memory; only in the cases it does not suffice, the expanded form must be used (comparing two number restrictions has a quadratic complexity in the simpler cases, not to talk about checking the ABox). Besides, with the expanded form, hundreds of substitutivity axioms might need to be added to the matrix. Thus, can only be competitive in this DL fragment, when, e.g., solutions based on rewriting [2, 10] can be devised and integrated, i.e., a way to substitute equal individuals by their canonical representative is envisaged. Bibel already suggested term rewriting as a possible technique to solve equality in the CM [4]. Integrating it with the represents a challenge for our calculus to remain competitive as more expressive fragments are to be addressed.

7 Conclusions and Future Work

In the current work, is presented, a connection method that enhances the , by, mainly, introducing (in)equalities and, as a respective solution to handle them, equality connections with equality predicate substitutivity axioms explicit or implicit, as defined by Bibel. Two new forms of representing number restrictions are also shown: the abridged and the expanded form. In the former, cardinality restrictions are a new type of literals themselves, and this new notion of literal together with its respective new connection type had to be defined. In the latter, number restrictions are replaced by literals and (in)equalities that correspond to the number restriction’s semantic definition.

As for theoretical future work, we aim to create more sophisticated blocking schemes for dynamic and double blocking for DL constructs like inverses, union, intersection and complement of roles [9], transitivity, role chains and value maps, complex role axioms and dealing with nominals. As for practical future work, we intend to enhance the fragment currently dealt by RACCOON to include , as well as the future new solutions mentioned as theoretical future work.