<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Abductive Logic Programming for Datalog ontologies</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Marco Gavanelli</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Evelina Lamma</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Fabrizio Riguzzi</string-name>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Elena Bellodi</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Riccardo Zese</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Giuseppe Cota</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Dipartimento di Ingegneria</institution>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Dipartimento di Matematica e Informatica</institution>
        </aff>
        <aff id="aff2">
          <label>2</label>
          <institution>University of Ferrara Via Saragat</institution>
          <addr-line>1, I-44122, Ferrara</addr-line>
          ,
          <country country="IT">Italy</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>Ontologies are a fundamental component of the Semantic Web since they provide a formal and machine manipulable model of a domain. Description Logics (DLs) are often the languages of choice for modeling ontologies. Great e ort has been spent in identifying decidable or even tractable fragments of DLs. Conversely, for knowledge representation and reasoning, integration with rules and rule-based reasoning is crucial in the so-called Semantic Web stack vision. Datalog is an extension of Datalog which can be used for representing lightweight ontologies, and is able to express the DL-Lite family of ontology languages, with tractable query answering under certain language restrictions. In this work, we show that Abductive Logic Programming (ALP) is also a suitable framework for representing Datalog ontologies, supporting query answering through an abductive proof procedure, and smoothly achieving the integration of ontologies and rule-based reasoning. In particular, we consider an Abductive Logic Programming framework named SCIFF and derived from the IFF abductive framework, able to deal with existentially (and universally) quanti ed variables in rule heads, and Constraint Logic Programming constraints. Forward and backward reasoning is naturally supported in the ALP framework. The SCIFF language smoothly supports the integration of rules, expressed in a Logic Programming language, with Datalog ontologies, mapped into SCIFF (forward) integrity constraints. The main advantage is that this integration is achieved within a single language, grounded on abduction in computational logic.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>In order to realize this vision, the W3C has supported the development of
a family of knowledge representation formalisms of increasing complexity for
de ning ontologies, called Web Ontology Language (OWL). Ontologies are a
fundamental component of the Semantic Web, and Description Logics (DLs) are
often the languages of choice for modeling them.</p>
      <p>
        Several DL reasoners, such us Pellet [
        <xref ref-type="bibr" rid="ref32">32</xref>
        ], RacerPro [
        <xref ref-type="bibr" rid="ref19">19</xref>
        ] and HermiT [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ], are
used to extract implicit information from the modeled ontologies, and most of
them implement the tableau algorithm in a procedural language. Nonetheless,
some tableau expansion rules are non-deterministic, thus requiring to implement
a search strategy in an or-branching search space. A di erent approach is to
provide a Prolog-based implementation for the tableau expansion rules [34].
      </p>
      <p>
        Extensive work focused on developing tractable DLs, identifying the DL-Lite
family [
        <xref ref-type="bibr" rid="ref14">14</xref>
        ], for which answering conjunctive queries is in AC0 in data complexity.
      </p>
      <p>
        In a related research direction, [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ] proposed Datalog , an extension of
Datalog with existential rules for de ning ontologies. Datalog can be used for
representing lightweight ontologies, and encompasses the DL-Lite family [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ].
By suitably restricting the language syntax and adopting appropriate syntactic
conditions, also Datalog achieves tractability [
        <xref ref-type="bibr" rid="ref9">9</xref>
        ].
      </p>
      <p>
        In this work we consider the Datalog language and show how ontologies
expressed in this language can be also modeled in an Abductive Logic
Programming (ALP) framework, where query answering is supported by the underlying
ALP proof procedure. ALP has been proved a powerful tool for knowledge
representation and reasoning [
        <xref ref-type="bibr" rid="ref24">24</xref>
        ], taking advantage from ALP operational support as
(static or dynamic) veri cation tool. ALP languages are usually equipped with
a declarative (model-theoretic) semantics, and an operational semantics given
in terms of a proof-procedure. Several abductive proof procedures have been
dened (both backward, forward, and a mix of the two such), with many di erent
applications (diagnosis, monitoring, veri cation, etc.). Among them, the IFF
abductive proof-procedure [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ] was proposed to deal with forward rules, and with
non-ground abducibles. This proof procedure has been later extended [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ], and
the resulting proof procedure, named SCIFF, can deal with both existentially
and universally quanti ed variables in rule heads, and Constraint Logic
Programming (CLP) constraints [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ]. The resulting system was used for modeling
and implementing several knowledge representation frameworks, such as deontic
logic [
        <xref ref-type="bibr" rid="ref6">6</xref>
        ], normative systems, interaction protocols for multi-agent systems [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ],
Web services choreographies [
        <xref ref-type="bibr" rid="ref2">2</xref>
        ], etc.
      </p>
      <p>Here we concentrate on Datalog ontologies, and show how an ALP language
enriched with quanti ed variables (existential to our purposes) can be a useful
knowledge representation and reasoning framework for them. We do not focus
here on complexity results of the overall system, which is, however, not tractable.</p>
      <p>Forward and backward reasoning is naturally supported by the ALP proof
procedure, and the considered SCIFF language smoothly supports the
integration of rules, expressed in a Logic Programming language, with ontologies
expressed in Datalog . In fact, SCIFF allows us to map Datalog ontologies into
the forward integrity constraints on which it is based.</p>
      <p>In the following, Section 2 brie y introduces Datalog . Section 3 introduces
Abductive Logic Programming and the SCIFF language, with a mention to its
abductive proof procedure. Section 4 shows how the considered Datalog
language can be mapped into SCIFF, and the kind of queries that the abductive
proof procedure can handle. Section 5 illustrates related work. Section 6
concludes the paper, and outlines future work.
2</p>
    </sec>
    <sec id="sec-2">
      <title>Datalog</title>
      <p>
        Datalog extends Datalog by allowing existential quanti ers, the equality
predicate and the truth constant false in rule heads. Datalog can be used for
representing lightweight ontologies and is able to express the DL-Lite family of
ontology languages [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ]. By suitably restricting the language syntax, Datalog
achieves tractability [
        <xref ref-type="bibr" rid="ref9">9</xref>
        ].
      </p>
      <p>In order to describe Datalog , let us assume (i) an in nite set of data
constants , (ii) an in nite set of labeled nulls N (used as \fresh" Skolem terms),
and (iii) an in nite set of variables V . Di erent constants represent di erent
values (unique name assumption), while di erent nulls may represent the same
value. We assume a lexicographic order on [ N , with every symbol in N
following all symbols in . We denote by X vectors of variables X1; : : : ; Xk with
k 0. A relational schema R is a nite set of relation names (or predicates).
A term t is a constant, null or variable. An atomic formula (or atom) has the
form p(t1; : : : ; tn), where p is an n-ary predicate, and t1; : : : ; tn are terms. A
database D for R is a possibly in nite set of atoms with predicates from R
and arguments from [ N . A conjunctive query (CQ) over R has the form
q(X) = 9Y (X; Y), where (X; Y) is a conjunction of atoms having as
arguments variables X and Y and constants (but no nulls). A Boolean CQ (BCQ)
over R is a CQ having head predicate q of arity 0 (i.e., no variables in X).</p>
      <p>We often write a BCQ as the set of all its atoms, having constants and
variables as arguments, and omitting the quanti ers. Answers to CQs and BCQs
are de ned via homomorphisms, which are mappings : [ N [ V ! [</p>
      <p>N [ V such that (i) c 2 implies (c) = c, (ii) c 2 N implies (c) 2 [ N ,
and (iii) is naturally extended to term vectors, atoms, sets of atoms, and
conjunctions of atoms. The set of all answers to a CQ q(X) = 9Y (X; Y) over
a database D, denoted q(D), is the set of all tuples t over for which there
exists a homomorphism : X [ Y ! [ N such that ( (X; Y)) D and
(X) = t. The answer to a BCQ q = 9Y (Y) over a database D, denoted q(D),
is Yes, denoted D j= q, i there exists a homomorphism : Y ! [ N such
that ( (Y)) D, i.e., if q(D) 6= ;.</p>
      <p>Given a relational schema R, a tuple-generating dependency (or TGD) F is
a rst-order formula of the form 8X8Y (X; Y) ! 9Z (X; Z), where (X; Y)
and (X; Z) are conjunctions of atoms over R, called the body and the head of
F , respectively. Such F is satis ed in a database D for R i , whenever there
exists a homomorphism h such that h( (X; Y)) D, there exists an extension
h0 of h such that h0( (X; Z)) D. We usually omit the universal quanti ers in
TGDs. A TGD is guarded i it contains an atom in its body that involves all
variables appearing in the body.</p>
      <p>Query answering under TGDs is de ned as follows. For a set of TGDs T on R,
and a database D for R, the set of models of D given T , denoted mods(D; T ),
is the set of all (possibly in nite) databases B such that D B and every
F 2 T is satis ed in B. The set of answers to a CQ q on D given T , denoted
ans(q; D; T ), is the set of all tuples t such that t 2 q(B) for all B 2 mods(D; T ).
The answer to a BCQ q over D given T is Yes, denoted D [ T j= q, i B j= q
for all B 2 mods(D; T ).</p>
      <p>A Datalog theory may contain also negative constraints (or NC), which are
rst-order formulas of the form 8X (X) ! ?, where (X) is a conjunction
of atoms (not necessarily guarded). The universal quanti ers are usually left
implicit.</p>
      <p>Equality-generating dependencies (or EGDs) are the third component of a
Datalog theory. An EGD F is a rst-order formula of the form 8X (X) !
Xi = Xj , where (X), called the body of F , is a conjunction of atoms, and
Xi and Xj are variables from X. We call Xi = Xj the head of F . Such F is
satis ed in a database D for R i , whenever there exists a homomorphism h such
that h( (X)) D, it holds that h(Xi) = h(Xj ). We usually omit the universal
quanti ers in EGDs.</p>
      <p>The chase is a bottom-up procedure for deriving atoms entailed by a database
and a Datalog theory. The chase works on a database through the so-called
TGD and EGD chase rules.</p>
      <p>The TGD chase rule is de ned as follows. Given a relational database D for
a schema R, and a TGD F on R of the form 8X8Y (X; Y) ! 9Z (X; Z), F is
applicable to D if there is a homomorphism h that maps the atoms of (X; Y) to
atoms of D. Let F be applicable and h1 be a homomorphism that extends h as
follows: for each Xi 2 X, h1(Xi) = h(Xi); for each Zj 2 Z, h1(Zj ) = zj , where
zj is a \fresh" null, i.e., zj 2 N ; zj 62 D, and zj lexicographically follows all
other labeled nulls already introduced. The result of the application of the TGD
chase rule for F is the addition to D of all the atomic formulas in h1( (X; Z))
that are not already in D.</p>
      <p>The EGD chase rule is de ned as follows. An EGD F on R of the form
(X) ! Xi = Xj is applicable to a database D for R i there exists a
homomorphism h : (X) ! D such that h(Xi) and h(Xj ) are di erent and not both
constants. If h(Xi) and h(Xj ) are di erent constants in , then there is a hard
violation of F . Otherwise, the result of the application of F to D is the database
h(D) obtained from D by replacing every occurrence of h(Xi) with h(Xj ) if
h(Xi) precedes h(Xj ) in the lexicographic order, and every occurrence of h(Xj )
with h(Xi) if h(Xj ) precedes h(Xi) in the lexicographic order.</p>
      <p>
        The chase algorithm consists of an exhaustive application of the TGD and
EGD chase rules that may lead to an in nite result. The chase rules are applied
iteratively: in each iteration (1) a single TGD is applied once and then (2) the
EGDs are applied until a x point is reached. EGDs are assumed to be separable
[
        <xref ref-type="bibr" rid="ref12">12</xref>
        ]. Intuitively, separability holds whenever: (i) if there is a hard violation of an
EGD in the chase, then there is also one on the database w.r.t. the set of EGDs
alone (i.e., without considering the TGDs); and (ii) if there is no hard violation,
then the answers to a BCQ w.r.t. the entire set of dependencies equals those
w.r.t. the TGDs alone (i.e., without the EGDs).
      </p>
      <p>
        The two problems of CQ and BCQ evaluation under TGDs and EGDs are
logspace-equivalent [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ]. Moreover, query answering under TGDs is equivalent
to query answering under TGDs with only single atoms in their heads [
        <xref ref-type="bibr" rid="ref9">9</xref>
        ].
Henceforth, we focus only on the BCQ evaluation problem and we assume that every
TGD has a single atom in its head. A BCQ q on a database D, a set TT of TGDs
and a set TE of EGDs can be answered by performing the chase and checking
whether the query is entailed by the extended database that is obtained. In this
case we write D [ TT [ TE j= q.
      </p>
      <p>
        Example 1. Let us consider the following ontology for a real estate information
extraction system, a slight modi cation of the one presented in Gottlob et al.
[
        <xref ref-type="bibr" rid="ref18">18</xref>
        ]:
      </p>
      <p>F1 = ann(X; label); ann(X; price); visible(X) ! priceElem(X)
If X is annotated as a label, as a price and is visible, then it is a price element.</p>
      <p>F2 = ann(X; label); ann(X; priceRange); visible(X) ! priceElem(X)
If X is annotated as a label, as a price range, and is visible, then it is a price
element.</p>
      <p>F3 = priceElem(E); group(E; X) ! f orSale(X)
If E is a price element and is grouped with X, then X is for sale.</p>
      <p>F4 = f orSale(X) ! 9P price(X; P )
If X is for sale, then there exists a price for X.</p>
      <p>F5 = hasCode(X; C); codeLoc(C; L) ! loc(X; L)
If X has postal code C, and C's location is L, then X's location is L.</p>
      <p>F6 = hasCode(X; C) ! 9L codeLoc(C; L); loc(X; L)
If X has postal code C, then there exists L such that C has location L and so
does X.</p>
      <p>F7 = loc(X; L1); loc(X; L2) ! L1 = L2
If X has the locations L1 and L2, then L1 and L2 are the same.</p>
      <p>F8 = loc(X; L) ! advertised(X)
If X has a location L then X is advertised.</p>
      <p>Suppose we are given the database
codeLoc(ox1; central); codeLoc(ox1; south); codeLoc(ox2; summertown)
hasCode(prop1; ox2); ann(e1; price); ann(e1; label); visible(e1);
group(e1; prop1)</p>
      <sec id="sec-2-1">
        <title>The atomic BCQs priceElem(e1), f orSale(prop1) and advertised(prop1) eval</title>
        <p>uate to true, while the CQ loc(prop1; L) has answers q(L) = fsummertowng.
In fact, even if loc(prop1; z1) with z1 2 N is entailed by formula F5,
formula F7 imposes that summertown = z1. If F7 were absent then q(L) =
fsummertown; z1g.</p>
        <p>Answering BCQs q over databases and ontologies containing NCs can be
performed by rst checking whether the BCQ (X) evaluates to false for each NC
of the form 8X (X) ! ?. If one of these checks fails, then the answer to the
original BCQ q is positive, otherwise the negative constraints can be simply
ignored when answering the original BCQ q.</p>
        <p>
          A guarded Datalog ontology is a quadruple (D; TT ; TC ; TE ) consisting of a
database D, a nite set of guarded TGDs TT , a nite set of negative constraints
TC and a nite set of EGDs TE that are separable from TT . The data complexity
(i.e., the complexity where both the query and the theory are xed) of evaluating
BCQs relative to a guarded Datalog theory is polynomial [
          <xref ref-type="bibr" rid="ref9">9</xref>
          ].
        </p>
        <p>
          In the case in which the EGDs are key dependencies and the TGDs are
inclusion dependencies, Cal et al. [
          <xref ref-type="bibr" rid="ref13">13</xref>
          ] proposed a backward chaining algorithm
for answering BCQ. A key dependency is a set of EGDs of the form
fr(X; Y1; : : : ; Ym); r(X; Y10; :::; Y m0) ! Yi = Yi0g1 i m
A TGD of the form r1(X; Y) ! 9Zr2(X; Z), where r1 and r2 are predicate names
and no variable appears more than once in the body nor in the head, is called an
inclusion dependency. The key dependencies must not interact with the inclusion
dependencies, similarly to the semantic separability condition mentioned above
for TGDs and EGDs. In this case once it is known that no hard violation occurs,
queries can be answered by considering the inclusion dependencies only, ignoring
the key dependencies. A necessary and su cient syntactic condition for non
interaction is based on the construction of CD-graphs [
          <xref ref-type="bibr" rid="ref13">13</xref>
          ].
3
        </p>
      </sec>
    </sec>
    <sec id="sec-3">
      <title>ALP and its proof procedure</title>
      <p>Abductive Logic Programming (ALP, for short) is a family of programming
languages that integrate abductive reasoning into logic programming. An ALP
program is a logic program, consisting of a set of clauses, that can contain in the
body some distinguished predicates, belonging to a set A and called abducibles.
The aim is nding a set of abducibles EXP, built from symbols in A that,
together with the knowledge base, is an explanation for a given known e ect
(also called goal G):
Also, EXP should satisfy a set of logic formulae, called Integrity Constraints
IC:</p>
      <p>KB [ EXP j= G:
KB [ EXP j= IC:
(1)
(2)</p>
      <p>E.g., a knowledge base might contain a set of rules stating that a person is a
nature lover
natureLover(X)
natureLover(X)
hasAnimal(X; Y ); pet(Y ):
biologist(X):
From this knowledge base one can infer, e.g., that each person who owns a pet
is a nature lover. However, in some cases we might have the information that
kevin is a nature lover, and wish to infer more information about him. In such a
case we might label predicates hasAnimal, pet and biologist as abducible (in
the following, abducible predicates are written in bold) and apply an abductive
proof procedure to the knowledge base. Two explanations are possible: either
there exists an animal that is owned by kevin and that is a pet:
(9Y )</p>
      <p>hasAnimal(kevin; Y ); pet(Y )
or kevin is a biologist:</p>
      <p>biologist(kevin)
We see that the computed answer includes abduced atoms, which can contain
variables.</p>
      <p>Integrity constraints can help reducing the number of computed
explanations, ruling out those that are not possible. For example, the following integrity
constraint states that to become a biologist one needs to be at least 25 years
old:
biologist(X); age(X; A) ! A
25
We might know that kevin is a child, and have a de nition of the predicate
child:
child(X)</p>
      <p>
        age(X; A); A &lt; 10:
In this example we see the usefulness of constraints as in Constraint Logic
Programming [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ]: the symbols &lt;; ; ::: are handled as constraints, i.e., they are not
predicates de ned in a knowledge base, but they associate a numeric domain to
the involved variables and restrict it according to constraint propagation. Now,
the goal natureLover(kevin); child(kevin) returns only one possible
explanation:
(9Y )(9A)
hasAnimal(kevin; Y ); pet(Y ); age(kevin; A)
A &lt; 10
since the option that kevin is a biologist is ruled out. Note that we do not need
to know the exact age of kevin to rule out the biologist hypothesis.
      </p>
      <p>
        SCIFF [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ] is a language in the ALP class, originally designed to model and
verify interactions in open societies of agents [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ], and it is an extension of the
IFF proof-procedure [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ]. As in the IFF language, it considers forward integrity
constraints of the form
      </p>
      <p>body ! head
where the body is a conjunction of literals and the head is a disjunction of
conjunctions of literals. While in the IFF the literals can be built only on de ned
or abducible predicates, in SCIFF they can also be CLP constraints, occurring
events (only in the body), or positive and negative expectations.
De nition 1. A SCIFF Program is a pair hKB; ICi where KB is a set of
clauses and IC is a set of forward rules called Integrity Constraints (ICs, for
short in the following).</p>
      <p>SCIFF considers a (possibly dynamically growing) set of facts (named event
set) HAP, that contains ground atoms H(Event[; T ime]). This set can grow
dynamically, during the computation, thus implementing a dynamic
acquisition of events. Some distinguished abducibles are called expectations. A
positive expectation, written E(Event[; T ime]) means that a corresponding event
H(Event[; T ime]) is expected to happen, while EN(Event[; T ime]) is a negative
expectation, and requires events H(Event[; T ime]) not to happen. To simplify
the notation, we will omit the T ime argument from events and expectations
when not needed, as it is for our purposes.</p>
      <p>
        While events are ground atoms, expectations can contain variables. In
positive expectations all variables are existentially quanti ed (expressing the idea
that a single event is enough to support them), while negative expectations are
universally quanti ed, so that any event matching with a negative expectation
leads to inconsistency with the current hypothesis. CLP [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ] constraints can be
imposed on variables. The computed answer includes in general three elements:
a substitution for the variables in the goal (as usual in Prolog), the constraint
store (as in CLP), and the set EXP of abduced literals.
      </p>
      <p>The declarative semantics of SCIFF includes the classic conditions of
abductive logic programming</p>
      <p>KB [ HAP [ EXP j= G</p>
      <p>KB [ HAP [ EXP j= IC
plus speci c conditions to support the con rmation of expectations.</p>
      <p>Positive expectations are con rmed if</p>
      <p>KB [ HAP [ EXP j= E(X) ! H(X);
while negative expectations are con rmed (or better they are not violated) if</p>
      <p>KB [ HAP [ EXP j= EN(X) ^ H(X) ! false:</p>
      <p>The declarative semantics of SCIFF also requires that the same event cannot
be expected both to happen and not to happen</p>
      <p>KB [ HAP [ EXP j= E(X) ^ EN(X) ! false
(3)</p>
      <p>
        The SCIFF proof-procedure is a rewriting system that de nes a proof tree,
whose nodes represent states of the computation. A set of transitions rewrite a
node into one or more children nodes. SCIFF inherits the transitions of the IFF
proof-procedure [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ], and extends it in various directions. We recall the basics of
SCIFF; a complete description is in [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ], with proofs of soundness, completeness,
and termination. An e cient implementation of SCIFF is described in [
        <xref ref-type="bibr" rid="ref5">5</xref>
        ].
      </p>
      <p>
        Each node of the proof is a tuple T hR; CS; P SIC; EXPi, where R is the
resolvent, CS is the CLP constraint store, PSIC is a set of implications (called
Partially Solved Integrity Constraints) derived from propagation of integrity
constraints, and EXP is the current set of abduced literals. The main transitions,
inherited from the IFF are:
Unfolding replaces a (non abducible) atom with its de nitions;
Propagation if an abduced atom a(X) occurs in the condition of an IC (e.g.,
a(Y ) ! p), the atom is removed from the condition (generating X = Y ! p);
Case Analysis given an implication containing an equality in the condition
(e.g., X = Y ! p), generates two children in logical or (in the example,
either X = Y and p, or X 6= Y );
Equality rewriting rewrites equalities as in the Clark's equality theory;
Logical simpli cations other simpli cations like (true ! A) , A, etc.
SCIFF includes also the transitions of CLP [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ] for constraint solving. Finally,
in this paper we consider the generative version of SCIFF, previously called
also g-SCIFF [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ], in which also the H events in the set HAP are considered
as abducibles, and can be assumed like the other abducible predicates, beside
being provided as input in the event set HAP.
4
      </p>
    </sec>
    <sec id="sec-4">
      <title>Mapping Datalog into ALP programs</title>
      <p>In this section, we show that a Datalog program can be represented as a set
of SCIFF integrity constraints and an event set. SCIFF abductive declarative
semantics provides the model-theoretic counterpart to Datalog semantics.
Operationally, query answering is achieved bottom-up via the chase in Datalog ,
while in the ALP framework it is supported by the SCIFF proof procedure.
SCIFF is able to integrate a knowledge base KB, expressed in terms of Logic
Programming clauses, possibly with abducibles in their body, and to deal with
integrity constraints.</p>
      <p>To our purposes, we consider only SCIFF programs with an empty KB, ICs
with only conjunctions of positive expectations and CLP constraints (or false)
in their heads. We show that this subset of the language su ces to represent
Datalog ontologies.</p>
      <p>We map the nite set of relation names of a Datalog relational schema R
into the set of predicates of the corresponding SCIFF program.
De nition 2. The mapping is recursively de ned as follows, where A is an
atom, M can be either H or E, and F1, F2, . . . are formulae:
(Body ! Head) = H(Body) !</p>
      <p>H(A) = H(A)</p>
      <p>E(A) = E(A)
M(F1 ^ F2) = M(F1) ^ M(F2)</p>
      <p>M(false) = false
M(Yi = Yj ) = Yi = Yj</p>
      <p>E(9X A) = A</p>
      <sec id="sec-4-1">
        <title>E(Head)</title>
        <p>A Datalog database D for R corresponds to the (possibly in nite) SCIFF
event set HAP, since there is a one-to-one correspondence between each tuple in
D and each (ground) fact in HAP. This mapping is denoted as HAP = H(D).
Notice that since the SCIFF event set can dynamically grow, new constants can
be introduced as a new event occurs (these new constants correspond to those
in the set N of Datalog ).</p>
        <p>A Datalog TGD F of the kind body ! head is mapped into the SCIFF
integrity constraint IC = (F ), where the body is mapped into conjunctions of
SCIFF atoms, and head into conjunctions of SCIFF abducible atoms. Existential
quanti cations of variables occurring in the head of the TGD are maintained in
the head of the SCIFF IC, but they are left implicit in the SCIFF syntax, while
the rest of the variables are universally quanti ed with scope the entire IC.</p>
        <p>Given a set of TGDs T , let us denote the mapping of T into the corresponding
set IC of SCIFF integrity constraints, as IC = (T ).</p>
        <p>Recall that for a set of TGDs T on R, and a database D for R, the set of
models of D given T , denoted mods(D; T ), is the set of all (possibly in nite)
databases B such that D B and every F 2 T is satis ed in B. For any such
database B, we can prove that there exists an abductive explanation EXP =
E(B), HAP0 = H(B) such that:</p>
        <p>HAP0 [ EXP j= IC
where HAP0 HAP = H(D), and IC = (T ).</p>
        <p>Finally, Datalog negative constraints NC are mapped into SCIFF ICs with
head false, and equality-generating dependencies EGDs into SCIFF ICs, each
one with an equality CLP constraint in its head.</p>
        <p>Therefore, informally speaking, the set of models of D given T , mods(D; T ),
corresponds to the set of all the abductive explanations EXP satisfying the set
of SCIFF integrity constraints IC = (T ).</p>
        <p>A Datalog CQ q(X) = 9Y (X; Y) over R is mapped into a SCIFF goal
G = E( (X; Y)), where E( (X; Y)) is a conjunction of SCIFF atoms.
Notice that in the SCIFF framework we have therefore a goal with existential
variables only, and among them, we are interested in computed answer
substitutions for the original (tuple of) variables X (and therefore Y variables can be
made anonymous).</p>
        <p>A Datalog BCQ q = (Y) is mapped similarly: G = E( (Y)).</p>
        <p>Recall that in Datalog the set of answers to a CQ q on D given T , denoted
ans(q; D; T ), is the set of all tuples t such that t 2 q(B) for all B 2 mods(D; T ).
With abuse of notation, we will write q(t) to mean answer t for q on D given T .</p>
        <p>We can hence state the following theorems for (model-theoretic) completeness
of query answering.</p>
        <p>Theorem 1 (Completeness of query answering). For each answer q(t) of
a CQ q(X) = 9Y (X; Y) on D given T , in the corresponding SCIFF program
h;; (IC)i there exists an answer substitution and an abductive explanation
EXP [ HAP0 for goal G = E( (X; )) such that:
where HAP = H(D), IC = (T ), and G = E( (t; )).</p>
        <p>Corollary 1 (Completeness of boolean query answering). If the answer
to a BCQ q = 9Y (Y) over D given T is Yes, denoted D [ T j= q, then in
the corresponding SCIFF program there exists an abductive explanation EXP [
HAP0 such that:</p>
        <p>H(D), IC = (T ), and G = E( ( )).</p>
        <p>
          The SCIFF proof procedure has been proved sound w.r.t. SCIFF declarative
semantics in [
          <xref ref-type="bibr" rid="ref4">4</xref>
          ], therefore for each abductive explanation EXP for a given goal
G in a SCIFF program, there exists a SCIFF-based computation producing a set
of abducibles (positive expectations to our purposes) EXP, and a computed
answer substitution for goal G possibly more general than .
        </p>
        <p>Example 2 (Real estate information extraction system in ALP). Let us conclude
this section by re-considering the Datalog ontology for the real estate
information extraction system of Example 1. TGDs F1-F8 are one-to-one mapped into
the following SCIFF ICs:</p>
        <sec id="sec-4-1-1">
          <title>IC1 : H(ann(X; label)); H(ann(X; price)); H(visible(X)) ! E(priceElem(X))</title>
        </sec>
      </sec>
      <sec id="sec-4-2">
        <title>IC2 : H(ann(X; label)); H(ann(X; priceRange)); H(visible(X))</title>
        <p>! E(priceElem(X))</p>
        <sec id="sec-4-2-1">
          <title>IC3 : H(priceElem(E)); H(group(E; X)) ! E(f orSale(X))</title>
          <p>IC4 : H(f orSale(X)) ! (9P ) E(price(X; P ))</p>
        </sec>
        <sec id="sec-4-2-2">
          <title>IC5 : H(hasCode(X; C)); H(codeLoc(C; L)) ! E(loc(X; L))</title>
          <p>IC6 : H(hasCode(X; C)) ! (9L) E(codeLoc(C; L)); E(loc(X; L))
IC7 : H(loc(X; L1)); H(loc(X; L2)) ! L1 = L2</p>
        </sec>
        <sec id="sec-4-2-3">
          <title>IC8 : H(loc(X; L)) ! E(advertised(X))</title>
          <p>The database is then simply mapped into the following event set HAP:
fH(codeLoc(ox1; central)); H(codeLoc(ox1; south));</p>
        </sec>
      </sec>
      <sec id="sec-4-3">
        <title>H(codeLoc(ox2; summertown)); H(hasCode(prop1; ox2)); H(ann(e1; price));</title>
        <sec id="sec-4-3-1">
          <title>H(ann(e1; label)); H(visible(e1)); H(group(e1; prop1))g</title>
          <p>The SCIFF proof procedure applies ICs in a forward manner, and it infers
the following set of abducibles from the program above:</p>
          <p>EXP = fE(priceElem(e1)); E(f orSale(prop1)); 9P E(price(prop1; P ));</p>
        </sec>
        <sec id="sec-4-3-2">
          <title>E(loc(prop1; summertown)); E(advertised(prop1))g</title>
          <p>plus the corresponding H atoms, that are not reported for the sake of brevity.</p>
          <p>Each of the (ground) atomic queries of Example 1 is entailed in the SCIFF
program above, since there exist sets EXP and HAP0 such that:
HAP0 [ EXP j= E(priceElem(e1)); E(f orSale(prop1)); E(advertised(prop1))
The query 9L E(loc(prop1; L)) is entailed as well, considering the uni cation
L = summertown since:</p>
          <p>HAP0 [ EXP j= E(loc(prop1; summertown)):</p>
          <p>It is worth noting that the SCIFF framework is much more expressive than
the restricted version used in this paper; in fact, in the mapping we used an
empty KB, but in general the Knowledge Base can be a logic program, that can
includes expectations, abducible literals, as well as CLP constraints. Beside the
forward propagation of Integrity Constraints, SCIFF supports also backward
reasoning.
5</p>
        </sec>
      </sec>
    </sec>
    <sec id="sec-5">
      <title>Related Work</title>
      <p>Various approaches has been followed to reason upon ontologies.</p>
      <p>Usually, DL reasoners implement a tableau algorithm using a procedural
language. Since some tableau expansion rules are non-deterministic, the developers
have to implement a search strategy from scratch.</p>
      <p>
        Pellet [
        <xref ref-type="bibr" rid="ref32">32</xref>
        ] is a free open-source Java-based reasoner for SROIQ with simple
datatypes (i.e., for OWL 1.1). It implements a tableau-based decision
procedure for general TBoxes (subsumption, satis ability, classi cation) and ABoxes
(retrieval, conjunctive query answering). It supports the OWL-API, the DIG
interface, and the Jena interface and comes with numerous other features.
      </p>
      <p>
        Pellet can compute the set of all the explanations for given queries by
exploiting the tableau algorithm. An explanation is roughly a subset of the knowledge
base (KB) that is su cient for entailing the query. It applies Reiter's hitting
set algorithm [
        <xref ref-type="bibr" rid="ref29">29</xref>
        ] to nd all the explanations. This is a black box method:
Pellet repeatedly removes an axiom from the KB and then computes again a new
explanation exploiting the tableau algorithm on the new KB, recording all the
di erent explanations so found.
      </p>
      <p>
        Di erently from Pellet, reasoners written in Prolog can exploit Prolog's
backtracking facilities for performing the search. This has been observed in various
works. In [
        <xref ref-type="bibr" rid="ref28 ref8">8, 28</xref>
        ] the authors proposed a tableau reasoner in Prolog for First
Order Logic (FOL) based on free-variable semantic tableaux. However, the reasoner
is not tailored to DLs.
      </p>
      <p>
        Hustadt, Motik and Sattler [
        <xref ref-type="bibr" rid="ref22">22</xref>
        ] presented the KAON2 algorithm that
exploits basic superposition, a refutational theorem proving method for FOL with
equality, and a new inference rule, called decomposition, to reduce a SHIQ KB
into a disjunctive Datalog program, while DLog [
        <xref ref-type="bibr" rid="ref25">25, 33</xref>
        ] is an ABox reasoning
algorithm for the SHIQ language that allows to store the content of the ABox
externally in a database and to answer instance check and instance retrieval
queries by transforming the KB into a Prolog program.
      </p>
      <p>
        Meissner presented the implementation of a reasoner for the DL ALCN
written in Prolog [
        <xref ref-type="bibr" rid="ref26">26</xref>
        ] which was then extended and reimplemented in the Oz
language [
        <xref ref-type="bibr" rid="ref27">27</xref>
        ]. Starting from [
        <xref ref-type="bibr" rid="ref26">26</xref>
        ], Herchenroder [
        <xref ref-type="bibr" rid="ref20">20</xref>
        ] implemented heuristic search
techniques in order to reduce the inference time for the DL ALC. Faizi [
        <xref ref-type="bibr" rid="ref15">15</xref>
        ] added
to [
        <xref ref-type="bibr" rid="ref20">20</xref>
        ] the possibility of returning information about the steps executed during
the inference process for queries but still handled only ALC.
      </p>
      <p>
        A di erent approach is the one by Ricca et al. [
        <xref ref-type="bibr" rid="ref30">30</xref>
        ] that presented OntoDLV,
a system for reasoning on a logic-based ontology representation language called
OntoDLP. This is an extension of (disjunctive) ASP and can interoperate with
OWL. OntoDLV rewrites the OWL KB into the OntoDLP language, can retrieve
information directly from external OWL Ontologies and answers queries by using
ASP.
      </p>
      <p>TRILL [34, 35] adopts a Prolog-based implementation for the tableau
expansion rules for ALC description logics. Di erently from previous reasoners, TRILL
is also able to return explanations for the given queries. Moreover, TRILL di ers
in particular from DLog for the possibility of answering general queries instead
of instance check and instance retrieval only.</p>
      <p>As reported in Section 2, reasoning upon Datalog ontologies is achieved,
instead, via the chase bottom-up procedure, which is exploited for deriving atoms
entailed by a database and a Datalog theory.</p>
      <p>
        In this work, instead, we apply an abductive logic programming proof-procedure
to reason upon ontologic data. It is worth to notice that in a previous work [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]
the SCIFF proof-procedure was interfaced with Pellet to perform ontological
reasoning; in the current work, instead, SCIFF is directly used to perform the
reasoning by mapping atoms in the ontology to SCIFF concepts (like events and
expectations).
6
      </p>
    </sec>
    <sec id="sec-6">
      <title>Conclusions and Future Work</title>
      <p>
        In this paper, we addressed representation and reasoning for Datalog ontologies
in an Abductive Logic Programming framework, with existential (and
universal) variables, and Constraint Logic Programming constraints in rule heads. The
underlying proof procedure, named SCIFF, is inspired by the IFF proof
procedure, and had been implemented in Constraint Handling Rules [
        <xref ref-type="bibr" rid="ref16">16</xref>
        ]. The SCIFF
system has already been used for modeling and implementing several knowledge
representation frameworks, also providing an e ective reasoning system.
      </p>
      <p>Here we have considered Datalog ontologies, and shown how the SCIFF
language can be a useful knowledge representation and reasoning framework for
them. In fact, the underlying abductive proof procedure can be directly exploited
as an ontological reasoner for query answering and consistency check. To the best
of our knowledge, this is the rst application of ALP to model and reason upon
ontologies.</p>
      <p>Moreover, the considered SCIFF language smoothly supports the integration
of rules, expressed in a Logic Programming language, with ontologies expressed
in Datalog , since a logic program can be added as (non-empty) KB to the set
of ICs, therefore considering deductive rules besides the forward ICs themselves.
Moreover, through dynamic acquisition of events in its HAP set, SCIFF might
also supports inline incrementality of the extensional part of the knowledge base
(namely, the ABox).</p>
      <p>Many issues have not been addressed in this paper, and they will be subject
of future work. First of all, we have not focused here on complexity results.
Future work will be devoted to identify syntactic conditions guaranteeing tractable
ontologies in SCIFF, in the style of what has been done for Datalog .</p>
      <p>A second issue for future work concerns experimentation and comparison
with other approaches, even not Logic Programming (LP, for short) based, on
real-size ontologies.</p>
      <p>Finally, SCIFF language is richer than the subset here used to represent
Datalog ontologies. It can support, in fact, negative expectations in rule heads,
with universally quanti ed variables too, which basically represent the fact that
something ought not to happen, and the proof procedure can identify violations
to them.</p>
      <p>Therefore, the richness of the language, and the potential of its abductive
proof procedure pave the way to add further features to Datalog ontologies.
33. Straccia, U., Lopes, N., Lukacsy, G., Polleres, A.: A general framework for
representing and reasoning with annotated semantic web data. In: Fox, M., Poole,
D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Arti cial
Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press (2010),
http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1590
34. Zese, R., Bellodi, E., Lamma, E., Riguzzi, F.: A description logics tableau
reasoner in Prolog. In: Cantone, D., Asmundo, M.N. (eds.) CILC. CEUR Workshop
Proceedings, vol. 1068, pp. 33{47. CEUR-WS.org (2013)
35. Zese, R., Bellodi, E., Lamma, E., Riguzzi, F., Aguiari, F.: Semantics and
inference for probabilistic description logics. In: Bobillo, F., Carvalho, R.N., da Costa,
P.C.G., d'Amato, C., Fanizzi, N., Laskey, K.B., Laskey, K.J., Lukasiewicz, T.,
Nickles, M., Pool, M. (eds.) Uncertainty Reasoning for the Semantic Web III
ISWC International Workshops, URSW 2011-2013, Revised Selected Papers.
Lecture Notes in Computer Science, vol. 8816, pp. 79{99. Springer (2014)</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Catta</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Chesani</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Montali</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Torroni</surname>
            ,
            <given-names>P.:</given-names>
          </string-name>
          <article-title>A computational logic application framework for service discovery and contracting</article-title>
          .
          <source>International Journal of Web Services Research</source>
          <volume>8</volume>
          (
          <issue>3</issue>
          ),
          <volume>1</volume>
          {
          <fpage>25</fpage>
          (
          <year>2011</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Chesani</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Montali</surname>
            ,
            <given-names>M.:</given-names>
          </string-name>
          <article-title>An abductive framework for a-priori veri cation of web services</article-title>
          . In: Maher, M. (ed.)
          <source>Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming</source>
          . pp.
          <volume>39</volume>
          {
          <fpage>50</fpage>
          . ACM Press, New York, USA (Jul
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Chesani</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Torroni</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Security protocols veri cation in Abductive Logic Programming: a case study</article-title>
          . In: Dikenelli,
          <string-name>
            <given-names>O.</given-names>
            ,
            <surname>Gleizes</surname>
          </string-name>
          ,
          <string-name>
            <given-names>M.P.</given-names>
            ,
            <surname>Ricci</surname>
          </string-name>
          ,
          <string-name>
            <surname>A</surname>
          </string-name>
          . (eds.)
          <source>Proceedings of ESAW'05, Lecture Notes in Arti cial Intelligence</source>
          , vol.
          <volume>3963</volume>
          , pp.
          <volume>106</volume>
          {
          <fpage>124</fpage>
          . Springer-Verlag (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Chesani</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Torroni</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Veri able agent interaction in abductive logic programming: the SCIFF framework</article-title>
          .
          <source>ACM Transactions on Computational Logic</source>
          <volume>9</volume>
          (
          <issue>4</issue>
          ) (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          :
          <article-title>The CHR-based implementation of the SCIFF abductive system</article-title>
          .
          <source>Fundamenta Informaticae</source>
          <volume>124</volume>
          (
          <issue>4</issue>
          ),
          <volume>365</volume>
          {
          <fpage>381</fpage>
          (
          <year>2013</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sartor</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Torroni</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Mapping deontic operators to abductive expectations</article-title>
          .
          <source>Computational and Mathematical Organization Theory</source>
          <volume>12</volume>
          (
          <issue>2</issue>
          {3),
          <volume>205</volume>
          { 225 (Oct
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <surname>Alberti</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gavanelli</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mello</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Torroni</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Speci cation and veri cation of agent interactions using social integrity constraints</article-title>
          .
          <source>Electronic Notes in Theoretical Computer Science</source>
          <volume>85</volume>
          (
          <issue>2</issue>
          ) (
          <year>2003</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <surname>Beckert</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Posegga</surname>
          </string-name>
          , J.: leanTAP:
          <article-title>Lean tableau-based deduction</article-title>
          .
          <source>J. Autom. Reasoning</source>
          <volume>15</volume>
          (
          <issue>3</issue>
          ),
          <volume>339</volume>
          {
          <fpage>358</fpage>
          (
          <year>1995</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <surname>Cal</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kifer</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          :
          <article-title>Taming the in nite chase: Query answering under expressive relational constraints</article-title>
          .
          <source>In: International Conference on Principles of Knowledge Representation and Reasoning</source>
          . pp.
          <volume>70</volume>
          {
          <fpage>80</fpage>
          . AAAI Press (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <surname>Cal</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lukasiewicz</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>A general datalog-based framework for tractable query answering over ontologies</article-title>
          .
          <source>In: Symposium on Principles of Database Systems</source>
          . pp.
          <volume>77</volume>
          {
          <fpage>86</fpage>
          .
          <string-name>
            <surname>ACM</surname>
          </string-name>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <surname>Cal</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lukasiewicz</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>Tractable query answering over ontologies with Datalog</article-title>
          .
          <source>In: International Workshop on Description Logics. CEUR Workshop Proceedings</source>
          , vol.
          <volume>477</volume>
          .
          <string-name>
            <surname>CEUR-WS.org</surname>
          </string-name>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>Cal</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lukasiewicz</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Marnette</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Pieris</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Datalog : A family of logical knowledge representation and query languages for new applications</article-title>
          .
          <source>In: IEEE Symposium on Logic in Computer Science</source>
          . pp.
          <volume>228</volume>
          {
          <fpage>242</fpage>
          . IEEE Computer Society (
          <year>2010</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <surname>Cal</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Pieris</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Tractable query answering over conceptual schemata</article-title>
          .
          <source>In: International Conference on Conceptual Modeling. LNCS</source>
          , vol.
          <volume>5829</volume>
          , pp.
          <volume>175</volume>
          {
          <fpage>190</fpage>
          . Springer (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14.
          <string-name>
            <surname>Calvanese</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Giacomo</surname>
            ,
            <given-names>G.D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lembo</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lenzerini</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Rosati</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          :
          <article-title>Tractable reasoning and e cient query answering in description logics: The dl-lite family</article-title>
          .
          <source>J. Autom. Reasoning</source>
          <volume>39</volume>
          (
          <issue>3</issue>
          ),
          <volume>385</volume>
          {
          <fpage>429</fpage>
          (
          <year>2007</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <surname>Faizi</surname>
          </string-name>
          , I.:
          <article-title>A Description Logic Prover in Prolog</article-title>
          .
          <source>Bachelor's thesis</source>
          ,
          <source>Informatics Mathematical Modelling</source>
          , Technical University of Denmark (
          <year>2011</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16. Fruhwirth, T.:
          <article-title>Theory and practice of constraint handling rules</article-title>
          .
          <source>Journal of Logic Programming</source>
          <volume>37</volume>
          (
          <issue>1-3</issue>
          ),
          <volume>95</volume>
          {138 (Oct
          <year>1998</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          17.
          <string-name>
            <surname>Fung</surname>
            ,
            <given-names>T.H.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kowalski</surname>
            ,
            <given-names>R.A.</given-names>
          </string-name>
          :
          <article-title>The IFF proof procedure for abductive logic programming</article-title>
          .
          <source>Journal of Logic Programming</source>
          <volume>33</volume>
          (
          <issue>2</issue>
          ),
          <volume>151</volume>
          {165 (Nov
          <year>1997</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          18.
          <string-name>
            <surname>Gottlob</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lukasiewicz</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Simari</surname>
            ,
            <given-names>G.I.</given-names>
          </string-name>
          :
          <article-title>Conjunctive query answering in probabilistic Datalog+/- ontologies</article-title>
          .
          <source>In: International Conference on Web Reasoning and Rule Systems. LNCS</source>
          , vol.
          <volume>6902</volume>
          , pp.
          <volume>77</volume>
          {
          <fpage>92</fpage>
          . Springer (
          <year>2011</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          19.
          <string-name>
            <surname>Haarslev</surname>
            ,
            <given-names>V.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Hidde</surname>
            ,
            <given-names>K.</given-names>
          </string-name>
          , Moller, R.,
          <string-name>
            <surname>Wessel</surname>
            ,
            <given-names>M.:</given-names>
          </string-name>
          <article-title>The racerpro knowledge representation and reasoning system</article-title>
          .
          <source>Semantic Web</source>
          <volume>3</volume>
          (
          <issue>3</issue>
          ),
          <volume>267</volume>
          {
          <fpage>277</fpage>
          (
          <year>2012</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref20">
        <mixed-citation>
          20. Herchenroder, T.:
          <article-title>Lightweight Semantic Web Oriented Reasoning in Prolog: Tableaux Inference for Description Logics</article-title>
          .
          <source>Master's thesis</source>
          , School of Informatics, University of Edinburgh (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref21">
        <mixed-citation>
          21.
          <string-name>
            <surname>Hitzler</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          , Krotzsch,
          <string-name>
            <given-names>M.</given-names>
            ,
            <surname>Rudolph</surname>
          </string-name>
          ,
          <string-name>
            <surname>S.</surname>
          </string-name>
          :
          <article-title>Foundations of Semantic Web Technologies</article-title>
          .
          <source>CRCPress</source>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref22">
        <mixed-citation>
          22.
          <string-name>
            <surname>Hustadt</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Motik</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sattler</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          :
          <article-title>Deciding expressive description logics in the framework of resolution</article-title>
          .
          <source>Inf. Comput</source>
          .
          <volume>206</volume>
          (
          <issue>5</issue>
          ),
          <volume>579</volume>
          {
          <fpage>601</fpage>
          (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref23">
        <mixed-citation>
          23.
          <string-name>
            <surname>Ja</surname>
            <given-names>ar</given-names>
          </string-name>
          , J.,
          <string-name>
            <surname>Maher</surname>
            ,
            <given-names>M.:</given-names>
          </string-name>
          <article-title>Constraint logic programming: a survey</article-title>
          .
          <source>Journal of Logic Programming 19-20</source>
          ,
          <issue>503</issue>
          {
          <fpage>582</fpage>
          (
          <year>1994</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref24">
        <mixed-citation>
          24.
          <string-name>
            <surname>Kakas</surname>
            ,
            <given-names>A.C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kowalski</surname>
            ,
            <given-names>R.A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Toni</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>Abductive Logic Programming</article-title>
          .
          <source>Journal of Logic and Computation</source>
          <volume>2</volume>
          (
          <issue>6</issue>
          ),
          <volume>719</volume>
          {
          <fpage>770</fpage>
          (
          <year>1993</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref25">
        <mixed-citation>
          25.
          <string-name>
            <surname>Lukacsy</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Szeredi</surname>
            ,
            <given-names>P.:</given-names>
          </string-name>
          <article-title>E cient description logic reasoning in Prolog: The DLog system</article-title>
          .
          <source>TPLP</source>
          <volume>9</volume>
          (
          <issue>3</issue>
          ),
          <volume>343</volume>
          {
          <fpage>414</fpage>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref26">
        <mixed-citation>
          26.
          <string-name>
            <surname>Meissner</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>An automated deduction system for description logic with ALCN language</article-title>
          .
          <source>Studia z Automatyki i Informatyki 28-29</source>
          ,
          <issue>91</issue>
          {
          <fpage>110</fpage>
          (
          <year>2004</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref27">
        <mixed-citation>
          27.
          <string-name>
            <surname>Meissner</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>A simple distributed reasoning system for the connection calculus</article-title>
          .
          <source>Vietnam Journal of Computer Science</source>
          <volume>1</volume>
          (
          <issue>4</issue>
          ),
          <volume>231</volume>
          {
          <fpage>239</fpage>
          (
          <year>2014</year>
          ), http://dx.doi.org/ 10.1007/s40595-014-0023-8
        </mixed-citation>
      </ref>
      <ref id="ref28">
        <mixed-citation>
          28.
          <string-name>
            <surname>Posegga</surname>
            ,
            <given-names>J.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Schmitt</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Implementing semantic tableaux</article-title>
          . In: DAgostino,
          <string-name>
            <given-names>M.</given-names>
            ,
            <surname>Gabbay</surname>
          </string-name>
          ,
          <string-name>
            <given-names>D.</given-names>
            , Hahnle, R.,
            <surname>Posegga</surname>
          </string-name>
          ,
          <string-name>
            <surname>J</surname>
          </string-name>
          . (eds.)
          <source>Handbook of Tableau Methods</source>
          , pp.
          <volume>581</volume>
          {
          <fpage>629</fpage>
          . Springer Netherlands (
          <year>1999</year>
          ), http://dx.doi.org/10.1007/
          <fpage>978</fpage>
          -94-017-1754-0_
          <fpage>10</fpage>
        </mixed-citation>
      </ref>
      <ref id="ref29">
        <mixed-citation>
          29.
          <string-name>
            <surname>Reiter</surname>
          </string-name>
          , R.:
          <article-title>A theory of diagnosis from rst principles</article-title>
          .
          <source>Artif. Intell</source>
          .
          <volume>32</volume>
          (
          <issue>1</issue>
          ),
          <volume>57</volume>
          {
          <fpage>95</fpage>
          (
          <year>1987</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref30">
        <mixed-citation>
          30.
          <string-name>
            <surname>Ricca</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gallucci</surname>
            ,
            <given-names>L.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Schindlauer</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Dell'Armi</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Grasso</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Leone</surname>
          </string-name>
          , N.:
          <article-title>OntoDLV: An ASP-based system for enterprise ontologies</article-title>
          .
          <source>J. Log. Comput</source>
          .
          <volume>19</volume>
          (
          <issue>4</issue>
          ),
          <volume>643</volume>
          {
          <fpage>670</fpage>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref31">
        <mixed-citation>
          31.
          <string-name>
            <surname>Shearer</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Motik</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Horrocks</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>Hermit: A highly-e cient owl reasoner</article-title>
          .
          <source>In: OWLED</source>
          (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref32">
        <mixed-citation>
          32.
          <string-name>
            <surname>Sirin</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Parsia</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Cuenca-Grau</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kalyanpur</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Katz</surname>
            ,
            <given-names>Y.</given-names>
          </string-name>
          :
          <article-title>Pellet: A practical OWL-DL reasoner</article-title>
          .
          <source>Journal of Web Semantics</source>
          <volume>5</volume>
          (
          <issue>2</issue>
          ),
          <volume>51</volume>
          {
          <fpage>53</fpage>
          (
          <year>2007</year>
          )
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>