=Paper=
{{Paper
|id=Vol-1350/paper-52
|storemode=property
|title=DysToPic:
                a Multi-Engine Theorem Prover for Preferential Description
                Logics
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-52.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/GiordanoGOPV15
}}
==DysToPic:
                a Multi-Engine Theorem Prover for Preferential Description
                Logics==
<pdf width="1500px">https://ceur-ws.org/Vol-1350/paper-52.pdf</pdf>
<pre>
           DysToPic: a Multi-Engine Theorem Prover for
                 Preferential Description Logics
                            Laura Giordano1 , Valentina Gliozzi2 ,
                   Nicola Olivetti3 , Gian Luca Pozzato2 , and Luca Violanti4
     1
          DISIT - U. Piemonte Orientale - Alessandria, Italy - laura.giordano@unipmn.it
                           2
                              Dip. Informatica - Universitá di Torino - Italy
                   {valentina.gliozzi,gianluca.pozzato}@unito.it
         3
           Aix Marseille Université - ENSAM, Université de Toulon, LSIS UMR 7296 - France
                               nicola.olivetti@univ-amu.fr
               4
                  NCR Edinburgh - United Kingdom - luca.violanti@gmail.com

            Abstract. We describe DysToPic, a theorem prover for the preferential De-
            scription Logic ALC + Tmin . This is a nonmonotonic extension of standard
            ALC based on a typicality operator T, which enjoys a preferential semantics.
            DysToPic is a multi-engine Prolog implementation of a labelled, two-phase
            tableaux calculus for ALC + Tmin whose basic idea is that of performing these
            two phases by different machines. The performances of DysToPic are promis-
            ing, and significantly better than the ones of its predecessor PreDeLo 1.0.

1        Introduction
Nonmonotonic extensions of Description Logics (DLs) have been actively investigated
since the early 90s [3, 1, 4, 6, 7, 13, 5]. A simple but powerful nonmonotonic extension
of DLs is proposed in [7, 13, 12]: in this approach “typical” or “normal” properties can
be directly specified by means of a “typicality” operator T enriching the underlying DL;
the typicality operator T is essentially characterized by the core properties of nonmono-
tonic reasoning axiomatized by either preferential logic [14] or rational logic [15]. In
these logics one can consistently express defeasible inclusions and exceptions such as
“normally, kids eat chocolate, but typical kids who have lactose intolerance do not”:
     T(Kid ) v ChocolateEater
     T(Kid u ∃HasIntolerance.Lactose) v ¬ChocolateEater .
In order to perform useful inferences, in [13] we have introduced a nonmonotonic ex-
tension of the logic ALC plus T based on a minimal model semantics. Intuitively, the
idea is to restrict our consideration to models that maximize typical instances of a con-
cept: more in detail, we introduce a preference relation among ALC plus T models,
then we define a minimal entailment restricted to models that are minimal with respect
to such preference relation. The resulting logic, called ALC + Tmin , supports typical-
ity assumptions, so that if one knows that Roman is a kid, one can nonmonotonically
assume that he is also a typical kid and therefore that he eats chocolate. As an example,
for a TBox specified by the inclusions above, in ALC + Tmin we can infer that:
         TBox |=ALC+Tmin T(Kid u Tall ) v ChocolateEater 5
         TBox ∪ {Kid (daniel)} |=ALC+Tmin ChocolateEater (daniel )
         TBox ∪ {Kid (daniel ), ∃HasIntolerance.Lactose(daniel )} |=ALC+Tmin
 5
     Being tall is irrelevant with respect to eating chocolate or not.
      x                                  |=ALC+Tmin ¬ChocolateEater (daniel )6
      TBox ∪ {Kid (daniel ), Tall (daniel )} |=ALC+Tmin ChocolateEater (daniel )
      TBox ∪ {∃HasBrother . Kid (seth)} |=ALC+Tmin ∃ HasBrother . ChocolateEater (seth)7

In this work we focus on theorem proving for nonmonotonic extensions of DLs. We in-
troduce DysToPic, a theorem prover for preferential Description Logic ALC +Tmin .
DysToPic implements the labelled tableaux calculus for this logic introduced in [13]
performing a two-phase computation: in the first phase, candidate models falsifying
a given query are generated (complete open branches); in the second phase the mini-
mality of candidate models is checked by means of an auxiliary tableau construction.
DysToPic is a multi-engine theorem prover, whose basic idea is that the two phases
of the calculus are performed by different machines: a “master” machine M , called the
employer, executes the first phase of the tableaux calculus, whereas other computers are
used to perform the second phase on open branches detected by M . When M finds an
open branch, it invokes the second phase on the calculus on a different “slave” machine,
called worker, S1 , while M goes on performing the first phase on other branches, rather
than waiting for the result of S1 . When another open branch is detected, then another
machine S2 is involved in the procedure in order to perform the second phase of the
calculus on that branch. In this way, the second phase is performed simultaneously on
different branches, leading to a significant increase of the performances.
    Labelled tableaux calculi are implemented in Prolog, following the line of the prede-
cessor PreDeLo 1.0, introduced in [11]: DysToPic is inspired by the methodology
introduced by the system leanTAP [2], even if it does not fit its style in a rigorous man-
ner. The basic idea is that each axiom or rule of the tableaux calculi is implemented by
a Prolog clause of the program: the resulting code is therefore simple and compact.
    In general, the literature contains very few proof methods for nonmonotonic ex-
tensions of DLs. We provide some experimental results to show that the performances
of DysToPic are promising, in particular comparing them to the ones of PreDeLo
1.0. DysToPic is available for free download at:
     http://www.di.unito.it/∼pozzato/theoremprovers.html

2      The Logic ALC + Tmin
The logic ALC + Tmin is obtained by adding to the standard ALC the typicality oper-
ator T [7, 12]. The intuitive idea is that T(C) selects the typical instances of a concept
C. We can therefore distinguish between the properties that hold for all instances of
concept C (C v D), and those that only hold for the normal or typical instances of C
(T(C) v D).
    The language L of the logic is defined by distinguishing concepts and extended
concepts as follows. Given an alphabet of concept names C, of role names R, and of
individual constants O, A ∈ C and > are concepts of L; if C, D ∈ L and R ∈ R,
then C u D, C t D, ¬C, ∀R.C, ∃R.C are concepts of L. If C is a concept, then C and
T(C) are extended concepts, and all the boolean combinations of extended concepts
 6
     Giving preference to more specific information.
 7
     Minimal consequence applies to individuals not explicitly named in the ABox as well, without
     any ad-hoc mechanism.
are extended concepts of L. A KB is a pair (TBox,ABox). TBox contains inclusion
relations (subsumptions) C v D, where C is an extended concept of the form either C 0
or T(C 0 ), and D ∈ L is a concept. ABox contains expressions of the form C(a) and
R(a, b), where C ∈ L is an extended concept, R ∈ R, and a, b ∈ O.
    In order to provide a semantics to the operator T, we extend the definition of a
model used in “standard” logic ALC. The idea is that the operator T is characterized
by a set of postulates that are essentially a reformulation of the Kraus, Lehmann and
Magidor’s axioms of preferential logic P [14]. Intuitively, the assertion T(C) v D
corresponds to the conditional assertion C |∼ D of P. T has therefore all the “core”
properties of nonmonotonic reasoning as it is axiomatized by P. The idea is that there
is a global preference relation among individuals, in the sense that x < y means that x
is “more normal” than y, and that the typical members of a concept C are the minimal
elements of C with respect to this relation. In this framework, an element x ∈ ∆ is
a typical instance of some concept C if x ∈ C I and there is no element in C I more
typical than x. The typicality preference relation is partial.
Definition 1. Given an irreflexive and transitive relation < over ∆, we define M in< (S)
= {x : x ∈ S and @y ∈ S s.t. y < x}. We say that < is well-founded if and only if, for
all S ⊆ ∆, for all x ∈ S, either x ∈ M in< (S) or ∃y ∈ M in< (S) such that y < x.
Definition 2. A model of ALC + Tmin is any structure h∆, <, Ii, where: ∆ is the
domain; I is the extension function that maps each extended concept C to C I ⊆ ∆,
and each role R to a RI ⊆ ∆ × ∆; < is an irreflexive, transitive and well-founded
(Definition 1) relation over ∆. I is defined in the usual way (as for ALC) and, in
addition, (T(C))I = M in< (C I ).
Given a model M of Definition 2, I can be extended so that it assigns to each individual
a of O a distinct element aI of the domain ∆ (unique name assumption). We say that
M satisfies an inclusion C v D if C I ⊆ DI , and that M satisfies C(a) if aI ∈ C I and
R(a, b) if (aI , bI ) ∈ RI . Moreover, M satisfies TBox if it satisfies all its inclusions,
and M satisfies ABox if it satisfies all its formulas. M satisfies a KB (TBox,ABox), if
it satisfies both TBox and ABox.
     The semantics of the typicality operator can be specified by modal logic. The in-
terpretation of T can be split into two parts: for any x of the domain ∆, x ∈ (T(C))I
just in case (i) x ∈ C I , and (ii) there is no y ∈ C I such that y < x. Condition (ii) can
be represented by means of an additional modality , whose semantics is given by the
preference relation < interpreted as an accessibility relation. The interpretation of  in
M is as follows: (C)I = {x ∈ ∆ | for every y ∈ ∆, if y < x then y ∈ C I }. We
immediately get that x ∈ (T(C))I if and only if x ∈ (C u ¬C)I .
     Even if the typicality operator T itself is nonmonotonic (i.e. T(C) v E does not
imply T(C u D) v E), what is inferred from a KB can still be inferred from any
KB’ with KB ⊆ KB’. In order to perform nonmonotonic inferences, in [13] we have
strengthened the above semantics by restricting entailment to a class of minimal (or
preferred) models. Intuitively, the idea is to restrict our consideration to models that
minimize the non-typical instances of a concept.
     Given a KB, we consider a finite set LT of concepts: these are the concepts whose
non-typical instances we want to minimize. We assume that the set LT contains at least
all concepts C such that T(C) occurs in the KB or in the query F , where a query F is
either an assertion C(a) or an inclusion relation C v D. As we have just said, x ∈ C I
is typical for C if x ∈ (¬C)I . Minimizing the non-typical instances of C therefore
means to minimize the objects falsifying ¬C for C ∈ LT . Hence, for a model M =
h∆, <, Ii, we define M
                          −
                                                         I
                        LT = {(x, ¬¬C) | x 6∈ (¬C) , with x ∈ ∆, C ∈ LT }.

Definition 3 (Preferred and minimal models). Given a model M = h∆, <, Ii of a
knowledge base KB, and a model M0 = h∆0 , <0 , I 0 i of KB, we say that M is preferred
to M0 w.r.t. LT , and we write M <LT M0 , if (i) ∆ = ∆0 , (ii) M
                                                                      −
                                                                              0−
                                                                    LT ⊂ MLT , (iii)
        0
aI = aI for all a ∈ O. M is a minimal model for KB (w.r.t. LT ) if it is a model of KB
and there is no other model M0 of KB such that M0 <LT M.
Definition 4 (Minimal Entailment in ALC + Tmin ). A query F is minimally entailed
in ALC + Tmin by KB with respect to LT if F is satisfied in all models of KB that are
minimal with respect to LT . We write KB |=ALC+Tmin F .
As an example, consider the TBox of the Introduction.
We have that TBox ∪ {Kid (daniel )} |=ALC+Tmin ChocolateEater (daniel ), since
daniel I ∈ (Kid u ¬Kid )I for all minimal models M = h∆ <, Ii of the TBox. In
contrast, by the nonmonotonic character of minimal entailment, TBox ∪ {Kid (daniel ),
∃HasIntolerance.Lactose(daniel )} |=ALC+Tmin ¬ChocolateEater (daniel ).

3   A Tableau Calculus for ALC + Tmin
In this section we recall the tableau calculus TABALC+     T for deciding whether a query
                                                     min
F is minimally entailed from a KB in ALC + Tmin introduced in [13]. The calcu-
lus performs a two-phase computation: in the first phase, a tableau calculus, called
      ALC+T
TAB P   H1    , simply verifies whether KB ∪ {¬F } is satisfiable in a model of Defini-
tion 2, building candidate models; in the second phase another tableau calculus, called
TAB ALC+    T , checks whether the candidate models found in the first phase are minimal
      P H2
models of KB, i.e. for each open branch of the first phase, TABALC+      T tries to build a
                                                                   P H2
model of KB which is preferred to the candidate model w.r.t. Definition 3. The whole
procedure is formally defined at the end of this section (Definition 5).
    TAB ALC+     T tries to build an open branch representing a minimal model satisfying
          min
KB ∪ {¬F }, where ¬F is the negation of the query F and is defined as follows: if
F ≡ C(a), then ¬F ≡ (¬C)(a); if F ≡ C v D, then ¬F ≡ (C u ¬D)(x), where x
                              ALC+T
does not occur in KB. TAB min         makes use of labels, denoted with x, y, z, . . .. Labels
represent individuals either named in the ABox or implicitly expressed by existential
                                                                            R
restrictions. These labels occur in constraints, that can have the form x −→ y or x : C,
where x, y are labels, R is a role and C is a concept of ALC + Tmin or has the form
¬D or ¬¬D, where D is a concept.
                                          T
3.1 The Tableaux Calculus TABALC+   P H1
                   ALC+T
A tableau of TABP   H1    is a tree whose nodes are pairs hS | U i. S is a set of con-
straints, whereas U contains formulas of the form C v DL , representing inclusion
relations C v D of the TBox. L is a list of labels, used in order to ensure the ter-
mination of the tableau calculus. A branch is a sequence of nodes hS1 | U1 i, hS2 |
U2 i, . . . , hSn | Un i . . ., where each node hSi | Ui i is obtained from its immediate pre-
decessor hSi−1 | Ui−1 i by applying a rule of TAB ALC+            T , having hS
                                                            P H1                i−1 | Ui−1 i as
the premise and hSi | Ui i as one of its conclusions. A branch is closed if one of its
nodes is an instance of a (Clash) axiom, otherwise it is open. A tableau is closed if all
its branches are closed.
     The rules of TABALC+         T are presented in Fig. 1. Rules (∃+ ) and (− ) are called
                             P H1
dynamic since they can introduce a new variable in their conclusions. The other rules are
called static. We do not need any extra rule for the positive occurrences of , since these
are taken into account by the computation of Sx→y      M
                                                              of (− ). The (cut) rule ensures
that, given any concept C ∈ LT , an open branch built by TAB ALC+          T contains either
                                                                      P H1
x : ¬C or x : ¬¬C for each label x: this is needed in order to allow TAB ALC+              T
                                                                                      P H2
to check the minimality of the model corresponding to the open branch. As mentioned
above, given a node hS | U i, each formula C v D in U is equipped with the list L of
labels to which the rule (v) has already been applied. This avoids multiple applications
of such rule to the same subsumption by using the same label.
     In order to check the satisfiability of a KB, we build its corresponding constraint
system hS | U i, and we check its satisfiability. Given KB=(TBox,ABox), its corre-
sponding constraint system hS | U i is defined as follows: S = {a : C | C(a) ∈
                 R
ABox} ∪ {a −→ b | R(a, b) ∈ ABox}; U = {C v D∅ | C v D ∈ TBox}. KB is sat-
isfiable if and only if its corresponding constraint system hS | U i is satisfiable. In order
to verify the satisfiability of KB ∪ {¬F }, we use TAB ALC+       T to check the satisfiability
                                                            P H1
of the constraint system hS | U i obtained by adding the constraint corresponding to ¬F
to S 0 , where hS 0 | U i is the corresponding constraint system of KB. To this purpose, the
                                ALC+T
rules of the calculus TABP        H1    are applied until either a contradiction is generated
(clash) or a model satisfying hS | U i can be obtained.
     The rules of TABALC+        T are applied with the following standard strategy: 1. apply
                          P H1
a rule to a label x only if no rule is applicable to a label y such that y ≺ x (where y ≺ x
says that label x has been introduced in the tableaux later than y); 2. apply dynamic
rules only if no static rule is applicable.
Theorem 1. Given LT , KB |=ALC+Tmin F if and only if there is no open branch
B in the tableau built by TABALC+  T for the constraint system corresponding to KB
                              P H1
∪ {¬F } such that the model represented by B is a minimal model of KB.

Thanks to the side conditions on the application of the rules and the blocking machinery
adopted by the dynamic ones, in [13] it has been shown that any tableau generated by
TABALC+    T for hS | U i is finite.
     P H1

                                             T
3.2 The Tableaux Calculus TABALC+     P H2
Let us now introduce the calculus TAB ALC+    T which checks whether each open branch
                                        P H2
B built by TAB ALC+    T represents a minimal model of the KB.
                  P H1
    Given an open branch B of a tableau built from TABALC+    T , let D(B) be the set of
                                                        P H1
labels occurring in B. Moreover, let B be the set of formulas x : ¬¬C occurring
                                         −


in B, that is to say B = {x : ¬¬C | x : ¬¬C occurs in B}.
                       −
  S, x : C, x : ¬C | U ⇥             ⇤S, x : ¬⇥ | U ⌅            ⇥S, x : | U ⇤                                             S, x : ¬(C ⇤ D) | U ⇥
                  (Clash)                    (Clash)                                                                                                                      ( )
                                                                        (Clash)               S, x : ¬(C ⇤ D), x : ¬C | U ⇥                 S, x : ¬(C ⇤ D), x : ¬D | U ⇥
                                                                                                                                              if x : ¬C ⇥ S and x : ¬D ⇥ S

         S, x : C ⇤ D | U ⇥                                            S, x : C ⇤ D | U ⇥                                                    S, x : ¬(C ⇤ D) | U ⇥
                                   ( +)                                                                         ( +)                                                       ( )
  S, x : C ⇤ D, x : C, x : D | U ⇥                 S, x : C ⇤ D, x : C | U ⇥          S, x : C ⇤ D, x : D | U ⇥                     S, x : ¬(C ⇤ D), x : ¬C, x : ¬D | U ⇥
                  if {x : C, x : D} ⇥ S                                              if x : C ⇥ S and x : D ⇥ S                                      if {x : ¬C, x : ¬D} ⇥ S

    S, x : ¬¬C | U ⇥                                  S, x : T(C) | U ⇥                                                          S, x : ¬T(C) | U ⇥
                          (¬)                                                  (T+ )                                                                                           (T )
  S, x : ¬¬C, x : C | U ⇥                     S, x : T(C), x : C, x : ¬C | U ⇥                          S, x : ¬T(C), x : ¬C | U ⇥          S, x : ¬T(C), x : ¬ ¬C | U ⇥
               if x : C ⇥ S                                 if {x : C, x : ¬C} ⇥ S                                                         if x : ¬C ⇥ S and x : ¬ ¬C ⇥ S
                                                                                                                                                               R
                        S | U⇥                                                      S | U, C ⇤ DL ⇥                                       ⌅S, x : ⇤R.C, x ⇥ y | U ⇧
                                                      (cut)                                                     ( )                                                            ( +)
 S, x :   ¬C | U ⇥              S, x : ¬ ¬C | U ⇥                         S, x : ¬C ⇤ D | U, C ⌅ DL,x ⇥                                                    R
                                                                                                                                       ⌅S, x : ⇤R.C, x ⇥ y, y : C | U ⇧
                     if x : ¬ ¬C ⇥ S and x : ¬C ⇥ S                                   if x occurs in S and x ⇥ L                                                       if y : C ⇥ S
                                              C LT
                                         x occurs in S
                                                                                    ⇥S, x : R.C | U ⇤
                                                                                                                                                                               ( +)
                    R                                      R                                        R                                              R
 ⌅S, x : ⇤R.C, x ⇥ y, y : C | U ⇧ ⌅S, x : ⇤R.C, x ⇥ v1 , v1 : C | U ⇧             ⌅S, x : ⇤R.C, x ⇥ v2 , v2 : C | U ⇧ . . . ⌅S, x : ⇤R.C, x ⇥ vn , vn : C | U ⇧
                                                                                                                                                                           y new
                                                                                                                                                           R
                                                                                                           if ⇤ ⌅z ⇥ x s.t. z   S,x: R.C x and ⌅ ⇧u s.t. x ⇥ u ⇤ S and u : C ⇤ S
                                                                                                                                                               vi occurring in S
                                                                                     S, x : ¬ ¬C | U ⇥
                                                                                                                                                                             ( )
 S, x : ¬ ¬C, y < x, y : C, y :      ¬C, SxM y | U ⇥ S, x : ¬ ¬C, v1 < x, v1 : C, v1 :          ¬C, SxM v1 | U ⇥ . . . S, x : ¬ ¬C, vn < x, vn : C, vn :           ¬C, SxM vn | U ⇥
                                                                                                                                                                               y new
                                                                                            if z ⇥ x s.t. z     S,x:¬ ¬C x and       u s.t. {u < x, u : C, u : ¬C, SxM u } S
                                                                                                                                                     ⇥vi occurring in S, x = vi



                                                          Fig. 1. The calculus TABALC+ T.
                                                                                  P H1



  S, x : C, x : ¬C | U | K⇥         ⇥S, x :    | U | K⇤     ⇤S, x : ¬⇥ | U | K⌅        ⇥S | U | ⇤          S, x : ¬ ¬C | U | K⇥                    S, x : T(C) | U | K⇥
                                                                         (Clash)                                         (Clash)                                               (T+ )
                      (Clash)                   (Clash)                                    (Clash)                                             S, x : C, x :     ¬C | U | K⇥
                                                                                                               if x : ¬ ¬C ⇥ B

                                                                                                                                                           R
                S, x : ¬T(C) | U | K⇥                                                  S | U, C ⇤ DL | K⇥                              ⌅S, x : ⇤R.C, x ⇥ y | U | K⇧
                                                          (T )                                                ( )                                                              ( +)
                                                                                                                                                       R
  S, x : ¬C | U | K⇥             S, x : ¬ ¬C | U | K⇥                          S, x : ¬C ⇤ D | U, C ⌅ DL,x | K⇥                     ⌅S, x : ⇤R.C, x ⇥ y, y : C | U | K⇧
                                                                                               x D(B) and x ⇥ L                                                        if y : C ⇥ S
                                          ⇥S, x : R.C | U | K⇤                                                                             S | U | K⇥
                                                                                                   ( +)                                                                      (cut)
          R                                 R                                  R
 ⇤S, x ⇥ v1 , v1 : C | U | K⌅         ⇤S, x ⇥ v2 , v2 : C | U | K⌅ . . . ⇤S, x ⇥ vn , vn : C | U | K⌅                 S, x :    ¬C | U | K⇥        S, x : ¬ ¬C | U | K⇥
                                                                   R
                                          If ⌅ ⌃u ⇤ D(B) s.t. x ⇥ u ⇤ S and u : C ⇤ S. ⇧vi ⇤ D(B)                                          if x : ¬ ¬C ⇥ S and x : ¬C ⇥ S
                                                                                                                                                         x D(B) C LT
                                                                       S, x : ¬ ¬C | U | K, x : ¬ ¬C⇥
                                                                                                                                                                ( )
                                                                                                                                           M
 ⇥S, v1 : C, v1 :    ¬C, SxM v1 , x : ¬ ¬C | U | K⇤ ⇥S, v2 : C, v2 :       ¬C, SxM v2 , x : ¬ ¬C | U | K⇤ . . . ⇥S, vn : C, vn : ¬C, Sx vn , x : ¬ ¬C | U | K⇤
                                                                                                                                                           M
                                                                                                                             if ⇥ ⇤u s.t. {u : C, u : ¬C, Sx u } S
                                                                                                                                                    ⇤vi D(B), x ⇥= vi

                            ALC+T
    Fig. 2. The calculus TABP H2  . To save space, we only include the most relevant rules.
                         ALC+T
    A tableau of TABP      H2     is a tree whose nodes are tuples of the form hS | U | Ki,
where S and U are defined as in TABALC+        T , whereas K contains formulas of the form
                                          P H1
x : ¬¬C, with C ∈ LT . The basic idea of TAB ALC+          T is as follows. Given an open
                                                      P H2
                            ALC+T
branch B built by TABP H1            and corresponding to a model MB of KB ∪ {¬F },
     ALC+T
TAB P  H2        checks whether MB is a minimal model of KB by trying to build a model
of KB which is preferred to MB . To this purpose, it keeps track (in K) of the negated
box formulas used in B (B ) in order to check whether it is possible to build a model
                                −


of KB containing less negated box formulas.
                         ALC+T                                                           T
    The rules of TABP     H2      are shown in Figure 2. The tableau built by TAB ALC+
                                                                                    P H2
                                                              B
closes if it is not possible to build a model smaller than M , it remains open otherwise.
Since by Definition 3 two models can be compared only if they have the same domain,
TAB ALC+     T tries to build an open branch containing all the labels appearing in B, i.e.
     P H2
those in D(B). To this aim, the dynamic rules use labels in D(B) instead of introducing
new ones in their conclusions. The rule (v) is applied to all the labels of D(B) (and
not only to those appearing in the branch). The rule (− ) is applied to a node hS, x :
¬¬C | U | K, x : ¬¬Ci, that is to say when the negated box formula x : ¬¬C
also belongs to the open branch B. Also in this case, the rule introduces a branch on
the choice of the individual vi ∈ D(B) to be used in the conclusion. In case a tableau
node has the form hS, x : ¬¬C | U | Ki, and x : ¬¬C 6∈ B , then TAB ALC+
                                                                          −                T
                                                                                      P H2
detects a clash, called (Clash)− : this corresponds to the situation where x : ¬¬C
does not belong to B, while the model corresponding to the branch being built contains
x : ¬¬C, and hence is not preferred to the model represented by B. The calculus
      ALC+T
TABP   H2     also contains the clash condition (Clash)∅ . Since each application of (− )
removes the negated box formulas x : ¬¬C from the set K, when K is empty all the
negated boxed formulas occurring in B also belong to the current branch. In this case,
                          ALC+T
the model built by TABP     H2     satisfies the same set of x : ¬¬C (for all individuals)
as B and, thus, it is not preferred to the one represented by B.
    Let KB be a knowledge base whose corresponding constraint system is hS | U i. Let
F be a query and let S 0 be the set of constraints obtained by adding to S the constraint
corresponding to ¬F . TABALC+        T is sound and complete in the following sense: an
                               P H2
                                ALC+T
open branch B built by TABP       H1      for hS 0 | U i is satisfiable in a minimal model of
KB iff the tableau in TAB ALC+     T for hS | U | B− i is closed.
                             P H2
                               ALC+T
    The termination of TABP      H2     is ensured by the fact that dynamic rules make use
of labels belonging to D(B), which is finite, rather than introducing “new” labels in
the tableau. Also, it is possible to show that the problem of verifying that a branch B
represents a minimal model for KB in TAB ALC+          T is in NP in the size of B.
                                                P H2
                                  ALC+T
    The overall procedure TAB min           is defined as follows:
Definition 5. Let KB be a knowledge base whose corresponding constraint system is
hS | U i. Let F be a query and let S 0 be the set of constraints obtained by adding to S
the constraint corresponding to ¬F . The calculus TABALC+      T checks whether a query
                                                         min
F can be minimally entailed from a KB by means of the following procedure:
                         ALC+T
    – the calculus TABP   H1      is applied to hS 0 | U i;
    – if, for each branch B built by TABALC+     T , either: (i) B is closed or (ii) the tableau
                                           P H1
                                   ALC+T
                                           for hS | U | B i is open, then the procedure
                                                              −
      built by the calculus TABP H2
      says YES else the procedure says NO

In [13] we have shown that TAB ALC+   T is a sound and complete decision procedure
                               min
for verifying if KB |=ALC+Tmin F , and that the problem is in CO -NE XP NP .
                      LT



4     Design of DysToPic
In this section we present DysToPic, a multi-engine theorem prover for reasoning in
ALC + Tmin . DysToPic is a SICStus Prolog implementation of the tableaux calculi
      ALC+T
TABmin         introduced in the previous section, wrapped by a Java interface which
relies on the Java RMI APIs for the distribution of the computation. The system is
designed for scalability and based on a “worker/employer” paradigm: the computational
burden for the “employer” can be spread among an arbitrarily high number of “workers”
which operate in complete autonomy, so that they can be either deployed on a single
machine or on a computer grid.
    The basic idea underlying DysToPic is as follows: there is no need for the first
phase of the calculus to wait for the result of one elaboration of the second phase on
an open branch, before generating another candidate branch. Indeed, in order to prove
whether a query F entails from a KB, the first phase can be executed on a machine;
every time that a branch remains open after the first phase, the execution of the second
phase for this branch can be performed in parallel, on a different machine. Meanwhile,
the main machine (worker), instead of waiting for the termination of the second phase
on that branch, can carry on with the computation of the first phase (potentially gen-
erating other branches). If a branch remains open in the second phase, then F is not
minimally entailed from KB (we have found a counterexample), so the computation
process can be interrupted early.

4.1 The Whole Architecture
In order to describe the architecture of DysToPic we refer to the worker-employer
metaphor. The system is characterized by: (i) a single employer, which is in charge of
verifying the query and yielding the final result. It also implements the first phase of
                              ALC+T
the calculus and uses TAB P    H1      to generate branches: the ones that it cannot close
(representing candidate models of KB ∪{¬F }), it passes to a worker; (ii) an unlimited
number of workers, which use TABALC+           T to evaluate the models generated by the
                                         P H2
employer; (iii) a repository, which stores all the answers coming from the workers.
First, each worker registers to the employer. When checking whether KB |=ALC+Tmin
F , the employer executes TABALC+         T . If the employer needs to check whether an
                                   P H1
open branch generated by the first phase represents a minimal model of the KB, then
it delegates the execution of the second phase to one of the registered workers, and
consequently proceeds with its computation on other branches generated in the first
phase. When a worker terminates its execution, it reports its result to the repository.
     If every branch has been processed and each worker has answered affirmatively,
i.e. each tableaux built in the second phase by TABALC+       T is open, the employer can
                                                        P H2
conclude that KB |=ALC+Tmin F . Otherwise, the employer can conclude the proof
as soon as the first negative answer comes into the repository, since (at least) a worker
found a closed tableaux in TAB ALC+     T for an open branch (candidate model) generated
                                  P H2
by the employer, in this case we have that KB 6|=ALC+Tmin F . It is worth noticing that
the employer has to keep a continuous dialogue with the repository.
     The library se.sics.jasper is used in order to combine Java and SICStus Pro-
log to decouple the two phases of the calculus. In detail, the employer handles the
query in Employer.java, a piece of Java code which presents it to alct1.pl, the
Prolog core implementing TAB ALC+         T . Every time that an open branch is generated,
                                   P H1
alct1.pl invokes Phase1RMIStub.java, another piece of Java code which will
send it to the correct worker. Workers will then have to process the open branches with
TABALC+      T , which is implemented in alct2.pl.
       P H2
     Concurrency is the main goal of our implementation, since we want the execution
of the first phase of the calculus to be independent from the second one. Java natively
supports concurrency via multithreading. The employer uses a separate thread (imple-
mented in Phase1Thread.java) to perform the current invocation of TAB ALC+            T
                                                                                 P H1
on a query, while its main thread polls the repository waiting for termination (the pro-
cedure can be stopped when the first counterexample is found, even if not all of the
branches have been explored). During the execution of TAB ALC+       T , every time that
                                                               P H1
the employer wants to ask a worker to verify a branch, a new thread is spawned. The
worker itself makes use of threads: its main thread simply enqueues each request com-
ing from the employer and spawns a new thread which performs TABALC+         T.
                                                                       P H2

4.2   The Implementation of the Tableaux Calculi
Concerning the implementation of the tableaux calculi TABALC+       T , each machine of
                                                              min
the system runs a SICStus Prolog implementation which is strongly related to the im-
plementation of the calculi given by PreDeLo 1.0, introduced in [11]. The imple-
mentation is inspired by the “lean” methodology of leanTAP, even if it does not follow
its style in a rigorous manner. The program comprises a set of clauses, each one imple-
menting a rule or axiom of the tableau calculi. The proof search is provided for free by
the mere depth-first search mechanism of Prolog, without any additional mechanism.
     DysToPic comprises two main predicates, called prove and prove phase2,
implementing, respectively, the first and the second phase of the tableau calculi.
Phase 1: the prove predicate. Concerning the first phase of the calculi, executed by
the employer, DysToPic represents a tableaux node hS | U i with two Prolog lists: S
and U. Elements of S are either pairs [X, F], representing formulas of the form x : F ,
                                                                                   R
or triples of the form either [X,R,Y] or [X,<,Y], representing either roles x −→ y
or the preference relation x < y, respectively. Elements of U are pairs of the form [[C
inc D],L], representing C v DL ∈ U described in Section 3.1.
                      ALC+T
    The calculi TAB min        are implemented by a top-level predicate
                      prove(+ABox,+TBox,[+X,+F],-Tree).
This predicate succeeds if and only if the query x : F is minimally entailed from the
KB represented by TBox and ABox. When the predicate succeeds, then the output term
Tree matches a Prolog term representing the closed tableaux found by the prover. The
top-level predicate prove/4 invokes a second-level one:
                    prove(+S,+U,+Lt,+Labels,+ABOX,-Tree)
having 6 arguments. In detail, S corresponds to ABox enriched by the negation of the
query x : F , whereas Lt is a list corresponding to the set of concepts LT . Labels
is the set of labels belonging to the current branch, whereas ABOX is used to store the
initial ABox (i.e. without the negation of the query) in order to eventually invoke the
second phase on it, in order to look for minimal models of the initial KB.
     Each clause of the prove/6 predicate implements an axiom or rule of the calculus
      ALC+T
TABP    H1      . To search a closed tableaux for hS | U i, DysToPic proceeds as follows.
First of all, if hS | U i is a clash, the goal will succeed immediately by using one of the
clauses implementing axioms. As an example, the following clause implements (Clash):
prove(S,U,_,_,_,tree(clash)):-
      member([X,C],S),member([X, neg C],S),!.
    If hS | U i is not an instance of the axioms, then the first applicable rule will be
chosen, e.g. if S contains an intersection [X,C and D], then the clause implementing
the (u+ ) rule will be chosen, and DysToPic will be recursively invoked on its unique
conclusion. DysToPic proceeds in a similar way for the other rules. The ordering of
the clauses is such that the application of the dynamic rules is postponed as much as
possible: this implements the strategy ensuring the termination of the calculi described
in the previous section. As an example, the clause implementing (T+ ) is as follows:
1. prove(S,U,Lt,Labels,ABOX,tree(...,Tree)):-member([X,ti C],S),
2.    (\+(member([X,C],S)); \+(member([X, box neg C],S))),!,
3.    prove([[X,C]|[[X, box neg C]|S]],U,Lt,Labels,ABOX,Tree),!.
In line 1, the standard Prolog predicate member is used in order to find a formula of the
form x : T(C) in the list S. In line 2, the side conditions on the applicability of such a
rule are checked: the rule can be applied if either x : C or x : ¬C do not belong to
S. In line 3 DysToPic is recursively invoked on the unique conclusion of the rule, in
which x : C and x : ¬C are added to the list S. The last clause of prove is:
prove(...) :- ... , jasper_call(JVM,
    method(’employer/Phase1RMIStub’,’solveViaRMI’,[static]),...,
    solve_via_rmi(NextWorkerName, ’toplevelphase2(...)’ ) ),!.
invoked when no other clauses are applicable. In this case, the branch built by the em-
ployer represents a model for the initial set of formulas, then the toplevelphase2
predicate is invoked on a worker in order to check whether such a model is minimal for
KB.
Phase 2: the prove phase2 predicate. Given an open branch built by the first phase,
the predicate toplevelphase2 is invoked on a worker. It first applies an optimiza-
tion preventing useless applications of (v), then it invokes the predicate
                     prove phase2(+S,+U,+Lt,+K,+Bb,+Db).
S and U contain the initial KB (without the query), whereas K, Bb and Db are Prolog
lists representing K, B and D(B) as described in Section 3.2. Lt is as for prove/6.
                          −


     Also in this case, each clause of prove phase2 implements an axiom or rule
of the calculi TAB ALC+    T . To search for a closed tableaux, DysToPic first checks
                     P H2
whether the current node hS | U | Ki is a clash. otherwise the first applicable rule
will be chosen, and DysToPic will be recursively invoked on its conclusions. As an
example, the clause implementing (T+ ) is as follows:
prove_phase2(S,U,Lt,K,Bb,Db) :- select([X,ti C],S,S1),
       prove_phase2([[X,C]|[[X,box neg C]|S1]],U,Lt,K,Bb,Db),!.
Notice that, according to the calculus TAB ALC+   T , the principal formula to which the
                                            P H2
rule is applied is removed from the current node: to this aim, the SICStus Prolog predi-
cate select is used rather than member.

4.3 Preliminary Performance Testing of DysToPic
We have made a preliminary attempt to show how DysToPic performs, especially in
comparison with its predecessor PreDeLo 1.0. The performances of DysToPic are
promising. We have tested both the provers by running SICStus Prolog 4.1.1 on Ubuntu
14.04.1 64 bit machines. Concerning DysToPic, we have tested it on 4 machines,
namely: 1. a desktop PC with an Intel Core i5-3570K CPU (3.4-3.8GHz, 4 cores, 4
threads, 8GB RAM); 2. a desktop PC with an Intel Pentium G2030 CPU (3.0GHz, 2
cores, 2 threads, 4GB RAM); 3. a Lenovo X220 laptop with an Intel Core i7-2640M
CPU (2.8-3.5GHz, 2 cores, 4 threads, 8GB RAM); 4. a Lenovo X230 laptop with an
Intel Core i7-3520M CPU (2.9-3.6GHz, 2 cores, 4 threads, 8GB RAM).
    We have performed two kinds of tests. On the one hand, we have randomly gener-
ated KBs with different sizes (from 10 to 100 ABox formulas and TBox inclusions) as
well as different numbers of named individuals: in less than 10 seconds, both DysToPic
and PreDeLo 1.0 are able to answer in more than the 75% of tests. Notice that, as
far as we know, it does not exist a set of acknowledged benchmarks for defeasible DLs.
On the other hand, we have tested the two theorem provers on specific examples. As
expected, DysToPic is better in than the competitor in answering that a query F is not
minimally entailed from a given KB. Surprisingly enough, its performances are better
than the ones of PreDeLo 1.0 also in case the provers conclude that F follows from
KB, as in the following example:
Example 1. Given TBox={T(Student) v ¬IncomeTaxPayer , WorkingStudent v
Student, T(WorkingStudent) v IncomeTaxPayer } and ABox={Student(mario),
WorkingStudent(mario), Tall (mario), Student(carlo), WorkingStudent(carlo),
Tall (carlo), Student(giuseppe), WorkingStudent(giuseppe), Tall (giuseppe)}, we
have tested both the provers in order to check whether IncomeTaxPayer (mario) is
minimally entailed from KB=(TBox,ABox). This query generates 1090 open branches
in TABALC+    T , each one requiring the execution of TAB ALC+T . PreDeLo 1.0 an-
        P H1                                              P H2
swers in 370 seconds, whereas DysToPic answers in 210 seconds if only two ma-
chines are involved (employer + one worker). If 4 workers are involved, DysToPic
only needs 112 seconds to conclude its computation.
Example 1 witnesses that the advantages obtained by distributing the computation jus-
tify the overhead introduced by the machinery needed for such distribution.


5   Conclusions
We have introduced DysToPic, a multi-engine theorem prover implementing tableaux
calculi for reasoning in preferential DL ALC + Tmin . DysToPic implements a dis-
tributed version of the tableaux calculus TABALC+     T introduced in [13], exploiting the
                                                 min
fact that the two phases characterizing such a calculus can be computed in parallel.
     We aim at extending DysToPic to the lightweight DLs of the DL-Lite and EL fam-
ily. Despite their relatively low expressivity, they are relevant for several applications,
in particular in the bio-medical domain. Extensions of EL⊥ and of DL-Litecore with
the typicality operator T have been proposed in [10], where it has also been shown that
minimal entailment is in Π2p (for EL⊥ , if restricted to a specific fragment). Tableaux
calculi performing a two phases computation, similar to TAB ALC+        T , have been pro-
                                                                  min
posed in [9, 8].

This research is partially supported by INDAM- GNCS Project 2015 “Logiche descrit-
tive e ragionamento non monotono”.
References
 1. Baader, F., Hollunder, B.: Priorities on defaults with prerequisites, and their application in
    treating specificity in terminological default logic. Journal of Automated Reasoning (JAR)
    15(1), 41–68 (1995)
 2. Beckert, B., Posegga, J.: leantap: Lean tableau-based deduction. Journal of Automated Rea-
    soning (JAR) 15(3), 339–358 (1995)
 3. Bonatti, P.A., Lutz, C., Wolter, F.: DLs with Circumscription. In: KR. pp. 400–410 (2006)
 4. Bonatti, P.A., Faella, M., Sauro, L.: Defeasible inclusions in low-complexity dls: Prelimi-
    nary notes. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on
    Artificial Intelligence (IJCAI 2009). pp. 696–701 (2009)
 5. Casini, G., Straccia, U.: Rational closure for defeasible description logics. In: Janhunen,
    T., Niemelä, I. (eds.) Logics in Artificial Intelligence - Proceedings of the12th European
    Conference (JELIA 2010). Lecture Notes in Computer Science (LNCS), vol. 6341, pp. 77–
    90. Springer (2010)
 6. Donini, F.M., Nardi, D., Rosati, R.: Description logics of minimal knowledge and negation
    as failure. ACM Transactions on Computational Logics (ToCL) 3(2), 177–225 (2002)
 7. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: ALC+T: a preferential extension of
    description logics. Fundamenta Informaticae 96, 341–372 (2009)
 8. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: A tableau calculus for a nonmonotonic
    extension of EL⊥ . In: Brünnler, K., Metcalfe, G. (eds.) Proceedings of the 20th Interna-
    tional Conference on Automated Reasoning with Analytic Tableaux and Related Methods
    (TABLEAUX 2011). Lecture Notes in Artificial Intelligence (LNAI), vol. 6793, pp. 180–
    195. Springer-Verlag, Bern, Switzerland (July 2011)
 9. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: A tableau calculus for a nonmono-
    tonic extension of the Description Logic DL − Lite core . In: Pirrone, R., Sorbello, F. (eds.)
    AI*IA 2011: Artificial Intelligence Around Man and Beyond - XIIth International Confer-
    ence of the Italian Association for Artificial Intelligence, Palermo, Italy, September 15-17,
    2011. Proceedings. Lecture Notes in Artificial Intelligence (LNAI), vol. 6934, pp. 164–176.
    Springer-Verlag, Palermo, Italy (Sptember 2011)
10. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Reasoning about typicality in low com-
    plexity DLs: the logics EL⊥ Tmin and DL-Litec Tmin . In: Walsh, T. (ed.) Proceedings of the
    22nd International Joint Conference on Artificial Intelligence (IJCAI 2011). pp. 894–899.
    IOS Press, Barcelona, Spain (2011)
11. Giordano, L., Gliozzi, V., Jalal, A., Olivetti, N., Pozzato, G.L.: Predelo 1.0: a theorem prover
    for preferential description logics. In: Baldoni, M., Baroglio, C., Boella, G., Micalizio, R.
    (eds.) Proceedings of AI*IA 2013. Lecture Notes in Artificial Intelligence LNAI, vol. 8249,
    pp. 60 – 72. Springer, Torino (December 2013)
12. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Preferential vs Rational Description
    Logics: which one for Reasoning About Typicality? . In: Coelho, H., Studer, R., Wooldridge,
    M. (eds.) Proceedings of the 19th European Conference on Artificial Intelligence (ECAI
    2010). FAIA (Frontiers in Artificial Intelligence and Applications), vol. 215, pp. 1069 –
    1070. IOS Press, Lisbon, Portugal (August 2010)
13. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: A NonMonotonic Description Logic
    for Reasoning About Typicality. Artificial Intelligence 195, 165 – 202 (2013)
14. Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and
    cumulative logics. Artificial Intelligence 44(1-2), 167–207 (1990)
15. Lehmann, D., Magidor, M.: What does a conditional knowledge base entail? Artificial Intel-
    ligence 55(1), 1–60 (1992)

</pre>