In this paper, we propose a connection method a la Bibel for an exception-tolerant extension of ALC. As for the language, we assume ALC extended with a typicality operator on concepts, which is a variant of defeasible DLs studied in the literature over the past decade and in which most of these can be embedded. We revisit the de nition of matrix representation of a knowledge base and establish the conditions for a given axiom to be provable from it. In particular, we show how term substitution is dealt with and de ne a suitable condition of blocking in the presence of typicality operators. We show that the calculus terminates and that it is sound and complete w.r.t. a DL version of the preferential semantics widely adopted in non-monotonic reasoning.
The problem of modelling exceptions in ontologies and reasoning meaningfully in
their presence has received a great deal of attention over the past decade. Among
the emblematic approaches put forward in the literature feature Giordano et al.'s
description logics of typicality [
One of the interesting features of some of the aforementioned approaches is the fact that, depending on the underlying DL that is assumed and given Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). certain conditions on how exceptionality (or typicality) is expressed, the kind of non-monotonic reasoning that is performed can be reduced to (a polynomial number of calls to) classical entailment check. Therefore, the study of automated deduction for the various avours of defeasible DLs, as well as its potential reduction to classical reasoning, remains a relevant research topic in the area.
The development of proof methods for defeasible description logics has, in
a sense, followed on the footsteps of those for classical DLs. As a result, the
majority of existing decision procedures for reasoning with defeasible ontologies
are based on semantic tableaux [
The connection method consists in a direct proof procedure of which the
main internal structure is a matrix representation of the knowledge base and
associated query. It was designed having as a guideline a more parsimonious usage
of memory during proof search. Indeed, contrary to tableaux and resolution, the
connection method does not create intermediate clauses or sentences along the
way, keeping its search space con ned to the boundaries of the matrix it started
o with. The rst connection calculus for description logics, ALC -CM, has been
proposed by Freitas and Otten [
The present paper aims to make the rst steps in the design of connection methods for reasoning over defeasible ontologies. In particular, we aim at providing a concrete calculus for a version of defeasible DL frequently considered in the literature that can be used to endow Raccoon with basic non-monotonic reasoning features. We hope our constructions will serve as a springboard for the development of the connection method in defeasible DLs of varying expressive power and further extensions of Raccoon.
In this paper, we shall assume the reader's familiarity with the di erent DL families, in particular with ALC. The remaining of the text is structured as follows: in Section 2, we present the defeasible extension of ALC we build on in this work; Section 3 is the heart of the paper and introduces our connection method for reasoning with defeasible ontologies, of which the inner workings are illustrated with a worked-out example in Section 4; Section 5 concludes the paper with a discussion and possible directions for further investigation. 5 https://github.com/dmfilho/raccoon
The defeasible DL ALCH [
In this paper, we shall nevertheless focus on the fragment ALC of ALCH
without role hierarchies and allowing for typicality of concepts, only. The reason
for this choice is three-fold: rst, it simpli es many of the technical de nitions
and results to be presented below; second, the fragment we here consider is
strongly related to the defeasible DL ALC + T of Giordano et al. [
The ( nite) sets of concept, role and individual names are denoted, respectively, with C, R, and I. With A; B; : : : we denote atomic concepts, with r; s; : : : role names, and with a; b; : : : individual names. Complex concepts of ALC are denoted with C; D; : : : and are built according to the following grammar: C ::= C j > j ? j :C j C u C j C t C j 8R:C j 9R:C j C (1)
The de nitions of axiom, GCI, assertion, TBox and ABox are as in the classical ALC case. If T and A are, respectively, a TBox and an ABox, with K = (T ; A) we denote henceforth a knowledge base (alias ontology).
Example 1 (Wizarding World Scenario). Assume we are interested in modeling facts about the wizarding world and its wonderful features. We have the atomic concepts C = fMuggle; Wizard; Spellg representing, respectively, the class of muggles, wizards, and spells. As for the set of atomic roles, we have the singleton R = fcastsg, representing a cast of a spell (done by a wizard). The set of individuals I is fhermione; oculusReparog. Below we have an example of an ALC knowledge base K = (T ; A) for the wizarding world scenario.
The semantics of ALC extends that of classical ALC and is in terms of partially-ordered structures called ordered interpretations. Before introducing these, we recall a few notions.
A binary relation is a strict partial order if it is irre exive and transitive. If < is a strict partial order on a given set X, with min< X =def fx 2 X j there is no y 2 X s.t. y < xg we denote the minimal elements of X w.r.t. <. A strict partial order on a set X is well-founded if for every ; 6= X0 X, we have min< X0 6= ;. De nition 1 (Ordered interpretation). An ALC ordered interpretation is a tuple O =def h O; O; <Oi s.t. h O; Oi is a classical ALC interpretation, <O O O is a well-founded strict partial order.
Given O = h O; O; <Oi, the intuition of O and O is the same as in a standard ALC interpretation. The intuition underlying the ordering <O is that it plays the role of a preference relation (or normality ordering): the objects that are lower down in the ordering <O are deemed more normal (or typical) than those higher up in <O. Within the context of (the interpretation of) a concept C, <O therefore allows us to single out the most normal representatives falling under C, which is the intuition of the semantics of concepts of the form C: De nition 2 (Semantics). An ordered interpretation O = h O; O; <Oi interprets the classical constructors in the usual way. Typicality-based concepts are interpreted as ( C)O =def min<O CO.
Hence, to be a typical element of a concept amounts to being one of the most preferred elements in the interpretation of that concept.
The de nition of satisfaction of a statement by an ordered interpretation O, denoted as O , carries over from the classical case. If X is a set of statements, with O X we denote the fact O satis es each statement in X, in which case we say O is a model of X. We say O is a model of a knowledge base K = (T ; A), denoted O K, if O is a model of both T and A.
Given a knowledge base K and a statement , we say that K preferentially entails , denoted K j= , if, for every O such that O K, we have O . 3
The connection method (CM) [
ALC -CM [
In this section, we introduce a connection method for ALC , which we henceforth call ALC -CM. It inherits the ALC -CM blocking, and deals with typicality by building an auxiliary structure which stands for the preference relation. 3.1
Matrix Representation The connection method requires formulae to be represented as matrices, composed of clauses, which are conjunctions of literals, possibly negated. To better handle concepts built using the typicality operator , we introduce below a typicality normal form (TNF).
De nition 3 (Pure disjunction and pure conjunction). A pure disjunction (D) and a pure conjunction (E^) are recursively de ned as follows: D ::= C j :C j D t D j 8R:C
E^ ::= C j :C j E u E^ j 9R:C ^
Pure disjunctions/conjunctions save memory and simplify proofs, see [
A v B.
An ABox axiom is in TNF if it is in one of the forms: (i) A(a), (ii) :A(a), (iii) r(a; b), or :r(a; b). A knowledge base (KB) is in TNF if all its axioms are in TNF. A query is in TNF if the queried axiom and the KB are in TNF.
The TNF allows us to deal only with axioms in speci c forms so that our matrix representation is simple and straightforward. An example of this simplicity is the restriction on concept assertions: only assertions with atomic concepts are allowed. Whether typical concept assertions or other assertions with complex concepts are present in the ABox, these assertions can be rewritten and these concepts relocated to the TBox as a subsumption axiom.
Proposition 1. Let K be an ALC knowledge base. There exists an ALC knowledge base K0 in TNF such that if O is a model of K0, then O for all 2 K.
Since the method is designed to check for the validity of a knowledge base
(or query), we represent it as a `disjunction set'. This set contains the original
axioms negated, although DLs do not allow for the negation of axioms to be
expressed. One way to solve this problem is to represent the knowledge base as
a single set, instantiating the TBox axioms, so that the TBox can be dropped.
This process is similar to the unfolding technique done by Baader et al. [
def :K=f9x(Du:E)(x) j D v E 2 T and x is a new variableg[f: j 2 Ag (2) De nition 6 (Literal and clause). A literal has one of the forms A(x), r(x; y), or their negations, where A is an atomic concept, r is an atomic role, and x, y are variables or individuals. A clause is a set of literals. A <-clause is a pair C< =def hC; <i, where C is a clause and < is an auxiliary relation on variables or individuals.
The <-clauses are obtained from axioms containing a typicality operator, as per the rules in Table 1. A clause C which is not related to a relation < can be seen as the <-clause hC; ;i.
De nition 7 (Matrix representation and graphical matrix). Let K be a knowledge base and :K its negation. A <-matrix M < is the set of <-clauses mapped from the axioms in :K as shown in Table 1. The graphical matrix of M < displays clauses as columns; the relation < (the union of the relations of all <-clauses in M <) associated to the matrix is shown as a lattice next to it. De nition 8 (Path, connection, -substitution and -complementary connection). A path through a <-matrix M < is a set composed by one literal of each clause in M <. A connection is a pair of literals fE; :Eg with the same concept or role name, but complementary to each other. A -substitution assigns each variable with an individual or another variable. The application of a -substitution to a literal is an application to its variables, i.e., (E(x)) = E( (x)) and (r(x; y)) = r( (x); (y)). A -complementary connection is a pair fE(x); :E(y)g or fr(x; v); :r(y; u)g, where (x) = (y) and (v) = (u). The complement L of a literal L is :E, if L = E, and E, if L = :E. De nition 9 (Set of concepts). If x is a variable or an individual, (x)=def fE 2 C j E(x) 2 Pathg is the set of concepts of x containing all concepts related to x in a path.
De nition 10 (Admissible -substitution, preference condition). Let be a term substitution. We say is admissible if the preference condition holds. The condition is de ned as follows: let x and y be variables or individuals in M <, and < be the union of the relations of all <-clauses in M <. Then, the preference condition holds after a -substitution if f(x; y),(y; x)g \ <+ = ;, with <+ the transitive closure of <.
We now formally de ne the ALC connection calculus (ALC -CM). The novelty here with regard to the previous classical DL-oriented calculus ALC -CM is twofold: (i ) the introduction of a new structure, the purpose of which is to denote a preference relation, and (ii ) the preference condition, which checks whether, in a candidate connection, the variables involved (if any) are incomparable w.r.t. the auxiliary ordering; in this case, the connection is allowed. By doing so, the calculus conforms to the preferential semantics de ned in Section 2. De nition 11 (Multiplicity). Let M < be a <-matrix and C< be a <-clause in M <. The multiplicity is a function : M < ! N that assigns to each <clause in M < a natural number denoting the number of copies of that clause in the matrix. Let iC< be the i-th copy of the clause C<, 1 i (C<). We say that C< =def f1C<; ; (C<) C<g is the set of copies of C< and
M < =def M < [
[ C<2M<
C< is the <-matrix M < combined with the clause copies.
De nition 12 (Blocking condition). Let (x ) be a new individual, i.e., (x ) 62 I. If ( (x )) ( (x 1)), then (x ) is blocked.
De nition 13 (ALC -CM calculus). Let M < be a <-matrix and let 2 M be a <-clause (or the query <-clause). The rules of the ALC connection calculus (ALC -CM) are as in Figure 1.
The rules in Figure 1 are applied in an analytical, bottom-up way and the
basic structure is the tuple hC; M <; Pathi, where clause C is the open
subgoal, M < is the <-matrix, and Path is the active path. When the Copy rule is
applied, it has to be followed by the Extension or the Reduction rule. (Freitas
and Varzinczak [
The tuple h ; ; Si, where , , and S are as referred to in Theorem 1, is called an ordered matrix proof.
De nition 15 (Preferential connection proof ). Let hC; M <; Pathi be a connection calculus tuple. A preferential connection proof for this tuple
fg; M <; Path C1; M < ; M <;; fg ; with C1 2 fC j hC; <0i 2 g
C; M <; Path [ fL2g C [ fL1g; M <; Path [ fL2g ; with (L1) = (L2) Extension Rule (Ext) C1 n fL2g; M <; Path [ fL1g
C [ fL1g; M <; Path
C; M <; Path
; with (L1) = (L2) Copy Rule (Cop) C0 [ fL1g; M < [ fC2<00 g; Path
C [ fL1g; M <; Path ; where C2<00 is a copy of C1<0 ; L2 2 C2<00 ; (L1) = (L2); and the blocking condition holds Fig. 1. The ALC -CM calculus. (also said the preferential connection proof for the <-matrix M <) is the application of the rules of the calculus to the initial tuple h ; M <; i (i.e., with C and Path initially empty), using an admissible -substitution s.t. all leaves are axioms (Ax).
Theorem 2 (Termination). Let M < be a <-matrix. Every sequence of rule applications starting with the tuple h ; M <; i terminates.
Theorem 3 (Soundness). If there exists a preferential connection proof for h ; M <; i with an admissible -substitution, then there is a multiplicity s.t. every path through M < contains a -complementary connection.
Theorem 4 (Completeness). If every path through M < contains a -complementary connection, then there is a preferential connection proof for h ; M <; i. 4
In Example 1, assume we want to know whether Hermione is a Muggle, but not a typical one. We can express this query as (Muggle u : Muggle)(hermione).
Let us transform the query into TNF. As it is a concept assertion, it is replaced by N1(hermione), adding Muggle u : Muggle v N1 in the knowledge base. Next, we rewrite this new axiom, based on the fact that A u N v C; B v N is a satis ability-preserving rewriting of AuB v C. We end up with the following knowledge base:
T = >8 Muggle v :Wizard; >9 ><9casts:Spell v Wizard;=> >:> M:ugMgleugugNle2vvNN21; >;>
A = 8 <
Muggle(hermione);
Spell(oculusReparo); :casts(hermione; oculusReparo); 9 =
The query N1(hermione) is a logical consequence of K if the matrix M (:K) [ ffN1(hermione)gg is valid. The resulting matrix and its partial order are below: 2 M(x0) M(x1) c(x2; y1) 6 666 :M(e) M(y0) S(y1) 6 4 W(x0) W(x1) :W(x2) 3 :M(x4) M(y3)
7 :N2(x4) :N2(x5) N1(h) 777 7 5 :M(h) :S(r) :c(h; r) x0 x1 x4
x5 M(x3) N2(x3) :N1(x3)
y3 e y0
With the relation at hand, we are able to restrict the -substitutions. For instance, in the example in Figure 2, we cannot do a -substitution for e and x0 because (e; x0) 2 <, and it would violate the preference condition. However, we can do a -substitution for e and x4. When we carry out this last substitution, the lattice of the preference relation is modi ed during the construction of the path to accommodate the -substitution, as shown in Figure 3.
x0
x1 fe; x4g y0 x5 y3
A proof in this method can be built in two equivalent ways: a simpler matrix with connections and a proof in the calculus. In Figure 4, we show the proof using the former: the matrix, the -substitution, and the nal partial order. In the gure, connections have been numbered to represent the order in which they were built.
The same proof using the calculus is shown in Figure 5. 2
:M(e) 6 6 6 M(x0) 6 6 4
W(x0)
M(x1)
S(y1) :M(h)
:S(r) M(y0) c(x2; y1) 7fy1=rg
6fy1=rg W(x1)
8fy3=eg 4fx0=hg 2 :c(h; r)
M(x3) Nfx24(=xh3g)3 Fig. 5. Connection proof in calculus style. The arrows copy the two subproofs generated after the extension rule Ext (y). It must also include the -substitution and partial order of Figure 4 (not duplicated here for the sake of space).
In this work, we have de ned a connection method for ALC , a commonly
considered fragment of the defeasible description logic ALCH [
As already alluded to in the introduction, the work here reported makes the rst steps in the study of connection methods as viable alternatives for reasoning with defeasible ontologies. It is therefore part of a broader long-term agenda. Immediate next steps stemming from the present work are: (i ) extending the method to the full language of ALCH , in particular to handle typicality of role names and in role hierarchies, and (ii ) endowing Raccoon with the ability to reason over defeasible extensions of ALC.
The reader conversant with preferential reasoning would have noticed that
in this work we assume preferential entailment, which is a Tarskian notion of
consequence and therefore monotonic. As pointed out in the literature on
nonmonotonic reasoning, preferential entailment is not always enough for reasoning
defeasibly with exceptions. Stronger, more robust, forms of entailment are often
called for and one particular de nition thereof, namely the rational closure of a
defeasible ontology has been thoroughly investigated in the context of defeasible
ALC [
In any case, the aforementioned approaches to the computation of the rational closure of a defeasible knowledge base rely on a number of calls to a classical (monotonic) reasoner and therefore the availability of a method for preferential reasoning in ALC as the one we propose here is an important step in the investigation of stronger forms of entailment in the presence of typicality operators.
The limitations of adopting a single preference ordering in modelling object
typicality have already been pointed out by Britz and Varzinczak [
This study has been nanced in part by the Coordenac~ao de Aperfeicoamento de Pessoal de N vel Superior - Brasil (CAPES) - Finance Code 001. It also has been supported in part by the project Reconciling Description Logics and NonMonotonic Reasoning in the Legal Domain (PRC CNRS{FACEPE, France{Brazil). Fred Freitas is partially supported by a Research Productivity grant provided by the Brazilian funding agency National Council for Scienti c and Technological Development { CNPq.