=Paper=
{{Paper
|id=Vol-1517/JOWO-15_ontolp_paper_4
|storemode=property
|title=∃-ASP
|pdfUrl=https://ceur-ws.org/Vol-1517/JOWO-15_ontolp_paper_4.pdf
|volume=Vol-1517
|dblpUrl=https://dblp.org/rec/conf/ijcai/GarreauGLS15
}}
==∃-ASP==
https://ceur-ws.org/Vol-1517/JOWO-15_ontolp_paper_4.pdf
∃-ASP
Fabien Garreau, Laurent Garcia, Claire Lefèvre and Igor Stéphan
LERIA
University of Angers
{fgarreau,garcia,claire,stephan}@info.univ-angers.fr
Abstract In the first class (like in (Eiter et al. 2008)), the two for-
malisms are handled separately. T is seen as an external
Answer set programming (ASP) is an appropriate for- source of information which can be used by the logic pro-
malism to represent various problems issued from arti- gram through special predicates querying the DL base. The
ficial intelligence and arising when available informa-
two bases are then independent with their own semantics
tion is incomplete. When dealing with information ex-
pressed in terms of ontologies in some tractable descrip- and the link between the two bases is performed using these
tion logic language, ASP must be extended to handle special predicates. (Eiter et al. 2013) uses their extension of
existential variables. We present the syntax and seman- ASP with external atoms to simulate rules with existential
tics of an ASP language with existential variables us- variables in the head (external atoms in the body serve to
ing Skolemization. We formalize its links with standard introduce new null values).
ASP. This work has led to an implementation. The second case (like in (Rosati 2006; Motik and Rosati
2010)) corresponds to an hybrid formalism which integrates
DLs and rules in a consistent semantic framework. Predi-
Introduction cates of T can be used in the rules of the program. Never-
This paper deals with the treatment of ontologies in Answer theless, there are some restrictions: for instance, these pred-
Set Programming (ASP) (Gelfond and Lifschitz 1988). We icates can not be used in the negative part of the body of a
are interested in using ASP technologies for querying large rule.
scale multisource heterogeneous web information. ASP is The last case integrates DLs and rules in a unique for-
considered to handle, by using default negation, inconsis- malism. For instance, (de Bruijn et al. 2010) uses quantified
tencies emerging by the fusion of the sources expressed by equilibrium logic (QEL). In this work, several hybrid knowl-
scalable description logics. Moreover, ASP can enrich the edge bases are defined (with safe restriction, safe restriction
language of ontologies by allowing the expression of de- without unique name assumption or with guarded restric-
fault information (for instance, when expressing inclusion tion) and it is proved that each category and their models
of concepts with exceptions). When dealing with ontologies can be expressed in terms of QEL.
in ASP, the problem stems from the presence of existential A large part of these works concerns the questions of
variables in description logics which are not expressible in complexity and decidability. In these frameworks, existen-
normal logic programs. The present work proposes a defini- tial variables are allowed in the part of the ontological infor-
tion of ASP with existential variables in order to express, in mation but are not allowed in the head of the rules.
a unique formalism, ontologies enriched by default negation Next to these models, (Ferraris, Lee, and Lifschitz 2011)
and rules. Processing existential variables is done in terms proposes a model allowing to cover both stable models se-
of Skolemization. mantics and first-order logic by means of a second-order for-
The study of the combination of ontologies and rules is mula issued from the initial information. Its links with the
not new (Rosati 2006; Eiter et al. 2008; de Bruijn et al. 2010; previously cited works have been established in (Lee and
Motik and Rosati 2010; Ferraris, Lee, and Lifschitz 2011; Palla 2011). (You, Zhang, and Zhang 2013) proposes an ex-
Lee and Palla 2011; Magka, Krötzsch, and Horrocks 2013). tension of ASP with existential variables in rule heads whose
In most of these models, the knowledge base is viewed as semantics corresponds to that of (Ferraris, Lee, and Lifschitz
a hybrid knowledge base composed of two parts (T ,P): T 2011).
is a knowledge base describing the ontological information Other works in logic programming take their origin in
expressed with a fragment of first-order logic, using for ex- Datalog and extend the language for specifying ontologies.
ample description logic, and P describes the rules in terms Datalog+/- is a family of such extensions with syntactical re-
of a logic program. strictions so that decidability is ensured. Several approaches
The miscellaneous attempts to integrate the two for- with existential quantified variables based on Datalog+/-
malisms can be distributed into three classes (Eiter et al. have been proposed in the literature but some have no non
2008; Lee and Palla 2011). monotonic negation (Alviano et al. 2012) and other have
only stratified negation (Cali et al. 2010). Nevertheless, one • if a ∈ PS with ar(a) = 0 then a ∈ A(L),
important and interesting point of these works is that they • if p ∈ PS with ar(p) = n > 0 and t1 , . . . , tn ∈ T(L)
focus on queries which is an important issue when dealing then p(t1 , . . . , tn ) ∈ A(L).
with ontologies.
In (Magka, Krötzsch, and Horrocks 2013), the knowledge The set GA(L) denotes the set of ground atoms of a lan-
base is a single one allowing existential variables and default guage L = (CS, FS, PS) defined as follows:
negation in the same rule. This work studies some conditions • if a ∈ PS with ar(a) = 0 then a ∈ GA(L),
of acyclicity and stratification that must be verified by the • if p ∈ PS with ar(p) = n > 0 and t1 , . . . , tn ∈ GT(L)
base ensuring the existence of a unique finite stable model. then p(t1 , . . . , tn ) ∈ GA(L).
The work is both theoretical and practical but it is concerned
with a limited extension of ASP. A substitution over a language L is a mapping from the
As far as we know, the only works leading to an imple- set of variables to the set of the terms T(L). Let t be a term
mentation are those of (Ianni et al. 2005; Eiter et al. 2005), (resp. a an atom) and σ a substitution, σ(t) (resp. σ(a)) is
based on (Eiter et al. 2008), and of (Magka, Krötzsch, and an instance of t (resp. a).
Horrocks 2013) which has been applied to information about A ground substitution over a language L is a mapping
biochemistry. from the set of variables to the set of the ground terms
The aim of our present work is to describe knowledge in a GT(L). Let t be a term (resp. a an atom) and σ a ground
single framework which can lead to useful implementation. substitution, σ(t) (resp. σ(a)) is a ground instance of t (resp.
We focus on ASP because it is a powerful framework for a).
knowledge representation and provides efficient solvers. The A partial ground substitution for a set of variables V over
work consists in enriching the ASP framework to take into a language L is a mapping from V to the set of ground terms
account existential variables. It can be seen as the other side GT(L). Let t be a term (resp. a an atom) and σ a partial
of the work consisting in introducing nonmonotonicity in ground substitution for a set of variables V , σ(t) (resp. σ(a))
existential rules (Baget et al. 2014b; 2014a). is a partial ground instance of t (resp. a) w.r.t. the set of
Next section gives the preliminary notions and definitions variables V .
useful for the paper. Then, we define programs expressed in
∃-ASP, an extension of ASP allowing existential variables, Syntax and semantics of ∃-ASP
and answer sets on this kind of programs. Last, we give the In this section, we define a variant of ASP allowing the use
links between ∃-ASP and standard ASP with a method to of existentially quantified variables (called existential vari-
translate a program expressed in ∃-ASP into a program ex- ables in the sequel). The rules proposed here extend classical
pressed in (standard) ASP and proofs about the transforma- safe rules (without disjunction) of the form:
tion.
H ← B1 , . . . , Bm , not N1 , . . . , not Ns .
Preliminaries where H, B1 , . . . , Bm , N1 , . . . , Ns are atoms. Safety im-
In this section, we give the formal definitions of the language poses that all variables that appear in a rule also appear in
and some notions useful in the following of the paper. the positive part of its body. In such a rule, all variables are
The set V denotes the infinite countable set of variables. interpreted as universally quantified. In the sequel, univer-
A language L is defined as a triplet (CS, FS, PS) which sally quantified variables will be called universal variables.
denotes respectively the set of constant symbols, the set of These classical rules are extended in two ways. First, the
function symbols and the set of predicate symbols of the lan- head of the rule, atom H, is replaced by a conjunction of
guage. It is assumed that the sets V, CS, FS and PS of any atoms and each negated atom Ni is also replaced by a con-
language are disjoint. Function ar denotes the arity function junction of atoms. These conjunctions allow multiple atoms
from FS to N∗ and from PS to N which associates to each to refer to the same existential variable. Second, the safety
function or predicate symbol its arity. condition is relaxed by allowing these new conjunctions of
The set T(L) denotes the set of terms of a language L = atoms to contain variables that do not appear in the positive
(CS, FS, PS) defined by induction as follows: part of the rule. These variables are interpreted as existential
• if v ∈ V then v ∈ T(L), ones.
For example, in the rule (p(X, Y ) ←
• if c ∈ CS then c ∈ T(L),
q(X), not r(X, Z).), variable X is interpreted as uni-
• if f ∈ FS with ar(f ) = n > 0 and t1 , . . . , tn ∈ T(L) versal, and Y and Z are interpreted as existential. The rule
then f (t1 , . . . , tn ) ∈ T(L). can be read as: “for all X, if q(X) is true and there does not
The set GT(L) denotes the set of ground terms of a lan- exist Z such that r(X, Z) is true, then one can conclude that
guage L = (CS, FS, PS) defined by induction as follows: there exists Y such that p(X, Y ) is true”.
• if c ∈ CS then c ∈ GT(L), Definition 1 (∃-rule and ∃-program) An ∃-program P of
• if f ∈ FS with ar(f ) = n > 0 and t1 , . . . , tn ∈ GT(L) language L = (CS, FS, PS) is a set of ∃-rules r defined as
then f (t1 , . . . , tn ) ∈ GT(L). follows (m, s ≥ 0, n, u1 , . . . , us ≥ 1):
The set A(L) denotes the set of atoms of a language L = H1 , . . . , H n ←
(CS, FS, PS) defined as follows: B1 , . . . , Bm , not (N11 , . . . , Nu11 ), . . . , not (N1s , . . . , Nuss ).
with H1 , . . . , Hn , B1 , . . . , Bm , N11 , . . . , Nu11 , . . . , N1s , . . . , The rule r2 means that for a person X there exists a direc-
Nuss ∈ A(L). tor D and X is a phD student of D, unless X is a lecturer and
We use the following notations: it exists a course given by X.
• head(r) = {H1 , . . . , Hn }. We have VH∀ (r) = {X}, VH∃ (r) = {D},
• body + (r) = {B1 , . . . , Bm }. V∃ (r)(l(X), gC(X, Y )) = {Y }, VN ∃ (r) = {X, D}.
• body − (r) = {{N11 , . . . , Nu11 }, . . . , {N1s , . . . , Nuss }}. For each program P , we consider that its language LP =
• V(r) the variables, (CS, FS, PS) consists of exactly the constant symbols,
• VH∃ (r) the variables which are in H1 , . . . , Hn but which function symbols and predicate symbols appearing in P .
are not in B1 , . . . , Bm (i.e. existential variables of the Proposition 1 Any (first-order classical) ASP program is an
head of r), ∃-program.
• V∃ (r)(N1i , . . . , Nui i ) variables which are in N1i , . . . , Nui i
Proof 1 This is a direct consequence of Definition 1.
but not in B1 , . . . , Bm , 1 ≤ i ≤ s (i.e. existential vari-
ables of N1i , . . . , Nui i ). The semantics of ∃-programs uses Skolemization of exis-
• VN ∃ (r) = 1≤i≤s V∃ (r)(N1i , . . . , Nui i ),
S tential variables appearing in the heads of the rules. We now
define this Skolemization.
• VN ∃ (r) = V(r) \ VN ∃ (r),
• V∃ (r) = VH∃ (r) VN ∃ (r)
S Definition 2 (Skolem symbols) Let r be an ∃-rule, n the
cardinality of VH∀ (r) and Y ∈ VH∃ (r) an existential vari-
• VH∀ (r) the variables which are at least in H1 , . . . , Hn able of r then skYn is a Skolem function symbol of arity n (if
and in B1 , . . . , Bm (i.e. universal variables of the head of n = 0 then skY is a Skolem constant symbol).
r, the frontier variables).
1
• V∀ (r)(N1i , . . . , Nui i ) the variables which are at least in Example 2 (Example 1 continued) Symbol skD is a
N1i , . . . , Nui i and in B1 , . . . , Bm (i.e. universal variables Skolem function symbol of arity 1 for the existential
variable D of the head of the rule r2 .
of N1i , . . . , Nui i ).
Definition 3 (Skolem Program) Let P be an ∃-program of
Moreover, the sets V∃ (r)(N1i , . . . , Nui i ) for every 1 ≤ i ≤ s
language LP .
must be disjoint and the sets VH∃ (r) and VN ∃ (r) must
Let s be an ordered sequence of the variables VH∀ (r) of
also be disjoint. (If a variable appears in several of the
an ∃-rule r of P . sk(r) denotes a Skolem rule obtained from
N1i , . . . , Nui i or if it appears in H1 , . . . , Hn and in one of the
r as follows: every existential variable v ∈ VH∃ (r) is sub-
N1i , . . . , Nui i , 1 ≤ i ≤ s, then it must appear in B1 , . . . , Bm stituted by the term skvn (s) with skvn the Skolem function
and it is a universal variable.) (constant) symbol associated to v and n = ar(skvn ) the size
For all rules r of a program P , V∃ (r) must be disjoint (i.e. of s (zero if VH∀ (r) = ∅). The Skolem program sk(P) of an
all the names of the existential variables of the program are ∃-program P is defined by sk(P ) = {sk(r)|r ∈ P }.
different).
A rule r is a definite rule if body − (r) = ∅ and a program Example 3 (Example 1 continued) The Skolem rule of r2
is a definite program if all the rules are definite. is the rule:
1 1
sk(r2 ) = (phdS(X, skD (X)), d(skD (X)) ←
Let us note that in such a rule r, several atoms are allowed p(X), not(l(X), gC(X, Y )).)
in head(r) and in each set of body − (r). In this case, a list of
Hence sk(PU ) = {r0 , r1 , sk(r2 )} and Lsk(PU ) =
atoms must be seen as the conjunction of each atom of the 1
list. ({a}, {skD }, {p, phdS, d, l, gC}).
Concerning the variables involved in the rule, they can be Skolem rules are still not safe: existential variables re-
quantified universally or existentially. The quantifiers are not main in the negative bodies. The grounding of such a rule
explicitly expressed in the rule but they depend on the posi- is a partial grounding restricted to the universal variables
tion in the rule: the variables appearing in body + (r) are uni- of the rule, the existential ones remaining not ground. In-
versally quantified while the ones not appearing in body + (r) deed, a non-ground rule (p(X) ← q(X), not r(X, Z).)
are existentially quantified. Let us note that the existential could be fired for some constant a if q(a) is true and, for all
variables, in the head or in each negative part of the body, z, r(a, z) is not true. Suppose two constants a and b. Then
are locally quantified. (p(a) ← q(a), not r(a, a).) and (p(a) ← q(a), not r(a, b).)
Example 1 Let PU be an ∃-program of language LU = are not equivalent to the non-ground rule for X = a be-
({a}, ∅, {p, phdS, d, l, gC}) with ar(p) = ar(d) = ar(l) = cause the first instance could be fired if r(a, b) is true (but not
1 and ar(phdS) = ar(gC) = 2. p stands for person, phdS r(a, a)) and the second could be fired if r(a, a) is true (but
for phDStudent, d for director, l for lecturer and gC for not r(a, b)). Yet neither r(a, b) nor r(a, a) should be true for
givesCourses. the initial rule to be fired. We thus define a partial ground-
ing, only concerning universal variables. For instance, a par-
PU = { tial ground instance of the above non-ground rule would be:
r0 : p(a)., (p(a) ← q(a), not r(a, Z).).
r1 : l(a).,
r2 : phdS(X, D), d(D) ← Definition 4 (Partial Ground Program) Set PG(r) for a
p(X), not(l(X), gC(X, Y )).} rule r of an ∃-program P of language LP denotes the set
of all partial ground instances of r over the language LP that is included in X2 . Thus, the rule is excluded from the
for VN ∃ (r). The partial ground program
S PG(P ) of an ∃- reduct. Other rules are kept. The obtained program is then:
program P is defined by PG(P ) = r∈P PG(r).
Example 4 (Example 1 continued) The language of the PG(sk(PU ∪ {gC(a, m).}))X∪{gC(a,m)} = {
Skolem program sk(PU ) contains only one constant, a, and gC(a, m).,
1
only one function symbol, skD . The set of ground terms is p(a).,
infinite and the partial grounding leads then to the following l(a).,
infinite program: phdS(skD 1 1
(a), skD 1
(skD 1
(a))), d(skD 1
(skD (a))) ←
1
PG(sk(PU )) = { p(skD (a)).,
p(a)., ...}
l(a).,
phdS(a, skD 1 1
(a)), d(skD (a)) ← Note that the reduct of a program that is Skolemized and
p(a), not (l(a), gC(a, Y ))., partially grounded is a definite ground program: it no longer
phdS(skD 1 1
(a), skD 1
(skD 1
(a))), d(skD 1
(skD (a))) ← contains variables. The consequence operator can then be
1 1 1 defined as usual, the only difference is that rules can have a
p(skD (a)), not (l(skD (a)), gC(skD (a), Y )).,
conjunction of atoms as head.
...}
Proposition 2 The partial ground program of an ∃-program Definition 6 (TP consequence operator and Cn its closure)
with no multiple head, no multiple default negation and no Let P be a definite partial ground program of an ∃-program
existential variable is a ground (classical) ASP program. of language LP . The operator TP : 2GA(LP ) → 2GA(LP )
is defined by
Proof 2 This is a direct consequence of Definitions 1 and 4.
TP (X) = {a|r ∈ P, a ∈ head(r), body + (r) ⊆ X}.
Definition 5 (Reduct) Let P be an ∃-program of language
LP and X ⊆ GA(Lsk(P ) ). The reduct of the partial ground Sn=+∞
Cn(P ) = n=0 TPn (∅) is the least fix-point of the conse-
program PG(sk(P )) w.r.t. X is the definite partial ground quence operator TP .
program
Example 6 (Example 1 continued)
PG(sk(P ))X = Cn(PG(sk(PU ))X ) = X but Cn(PG(sk(PU ∪
{ head(r) ← body + (r).|r ∈ PG(sk(P )), {gC(a, m).}))X∪{gC(a,m)} ) = {p(a), l(a), gC(a, m)}.
for all N ∈ body − (r) and
for all ground substitution σ over Lsk(P ) , σ(N ) 6⊆ X} Definition 7 (∃-answer set) Let P be an ∃-program of lan-
guage LP and X ⊆ GA(Lsk(P ) ). X is an ∃-answer set of
Example 5 (Example 1 continued) Let
P if and only if X = Cn(PG(sk(P ))X ).
1 1
X1 = {p(a), l(a), phdS(a, skD (a)), d(skD (a))}.
Example 7 (Example 1 continued) X is an ∃-answer set
Then, for the rule of PU and {p(a), l(a), gC(a, m)} is an ∃-answer set of PU ∪
1
phdS(a, skD 1
(a)), d(skD (a)) ← {gC(a, m).}.
p(a), not (l(a), gC(a, Y )). Proposition 3 Let P be a (classical) ASP program of lan-
there is no ground instance of l(a),gC(a, Y ) that is included guage LP and X ⊆ GA(LP ). X is an answer set of P
in X1 (since X1 does not contain any atom with gC) and the if and only if X is an ∃-answer set of P considered as an
positive part of the rule is kept. Other rules are kept for the ∃-program.
same reason. The obtained program is then: Proof 3 Since P is a classical ASP program, sk(P ) = P
and its (classical) ground ASP program corresponds ex-
PG(sk(PU ))X1 = { actly to PG(P ) = PG(sk(P )). Hence X ∈ GA(LP ) =
p(a)., GA(Lsk(P ) ) is an answer set of ground P , by Definition 7,
l(a)., if and only if it is an ∃-answer set of P considered as an
phdS(a, skD1 1
(a)), d(skD (a)) ← p(a)., ∃-program.
1 1 1 1 1
phdS(skD (a), skD (skD (a))), d(skD (skD (a))) ←
1
p(skD (a))., From ∃-ASP to ASP
...} In this section, we give the translation of an ∃-ASP program
into a standard ASP program and we show that the ∃-answer
sets of the initial program correspond to the answer sets of
Now, let X2 = X1 ∪ {gC(a, m)} and PU 2 = PU ∪ the new program.
{gC(a, m).}. The first step of the translation is the normalization whose
Here, l(a),gC(a, m) is a ground instance of the negative goal is twofold: to remove the conjunctions of atoms from
body of the rule negative parts of the rules and to remove existential variables
1 1 from these negative parts. The obtained program is equiva-
phdS(a, skD (a)), d(skD (a)) ←
p(a), not (l(a), gC(a, Y )). lent in terms of answer sets.
Definition 8 Let P be an ∃-program of language LP . Let r and r‡ =Ns ← N1s , . . . , Nuss . A program P with the rule
be an ∃-rule of P (m, s ≥ 0, n, u1 , . . . , us ≥ 1): r and the program P where the rule r is replaced by the
H1 , . . . , H n ← rules r† and r‡ have the same answer sets except for Ns .
B1 , . . . , Bm , not (N11 , . . . , Nu11 ), . . . , not (N1s , . . . , Nuss ). The proof can be constructed by induction by applying the
lemma to each part of the negative body of r and, then, to
with H1 , . . . , Hn , B1 , . . . , Bm , N11 , . . . , Nu11 , . . . , N1s , . . . , each rule of the program.
Nuss ∈ A(LP ). Let N be a set of new predicate symbols
(i.e. N ∩ PS = ∅). Proof 4 The proof is by induction on the following lemma:
The normalization of such an ∃-rule is the set of ∃-rules Let P be an ∃-program of language LP , r = (H ←
N(r) = C, not (N1 , . . . , Nu ).) ∈ PG(sk(P )), P 0 = PG(sk(P )) \
{ H1 , . . . , Hn ← B1 , . . . , Bm , not N1 , . . . , not Ns ., {r}, r† = (H ← C, not N.) ∈ PG(sk(N(P ))), R‡ =
PG(N ← N1 , . . . , Nu .) ⊆ PG(sk(N(P ))) and X ⊆
N1 ← N11 , . . . , Nu11 .,
GA(Lsk(P ) ).
...
If there exists a substitution θ such that
Ns ← N1s , . . . , Nuss .}
{θ(N1 ), . . . , θ(Nu )} ⊆ X then Cn((P 0 ∪ {r})X ) = X
with Ni the new atom pNi (X1 , . . . , Xv ), pNi ∈ N a new if and only if Cn((P 0 ∪ {r† } ∪ R‡ )X∪{N } ) = X ∪ {N }.
predicate symbol for every Ni and V∀ (r)(N1i , . . . , Nui i ) = If for all substitutions θ, {θ(N1 ), . . . , θ(Nu )} 6⊆ X
{X1 , . . . , Xv }. then Cn((P 0 ∪ {r})X ) = X if and only if
S The normalization of P is defined as N(P ) = Cn((P 0 ∪ {r† } ∪ R‡ )X ) = X.
r∈P N(r). Let us remark that N 6∈ Cn(P 0X ) ∪ X.
Set GAN(Lsk(P ) ) is the set of Skolem ground atoms for
the new predicate symbols defined as follows: • If there exists a substitution θ such that
{θ(N1 ), . . . , θ(Nu )} ⊆ X then (P 0 ∪ {r})X = P 0X =
• if a ∈ N with ar(a) = 0 then a ∈ GAN(Lsk(P ) ),
(P 0 ∪ {r† })X∪{N } then Cn((P 0 ∪ {r})X ) = Cn(P 0X )
• if p ∈ N with ar(p) > 0 and t1 , . . . , tn ∈ GT(Lsk(P ) ) and Cn((P 0 ∪ {r† } ∪ R‡ )X∪{N } ) = Cn(P 0X ) ∪ {N }.
then p(t1 , . . . , tn ) ∈ GAN(Lsk(P ) ). Then Cn((P 0 ∪ {r})X ) = X iff Cn(P 0X ) = X iff
Example 8 (Example 1 continued) Let pN be a new Cn(P 0X ) ∪ {N } = X ∪ {N } iff Cn((P 0 ∪ {r† } ∪
predicate symbol. The negative part of the rule r2 : R‡ )X∪{N } ) = X ∪ {N }.
not(l(X), gC(X, Y )) has only one universal variable, X. • If for all substitutions θ, {θ(N1 ), . . . , θ(Nu )} 6⊆ X then
It is replaced by not pN (X) (rule r2† ). And a new rule r2‡ (P 0 ∪ {r})X = (P 0 ∪ {H ← C.})X and (P 0 ∪ {r† } ∪
is added where Y that was an existential variable in r2 be- R‡ )X = (P 0 ∪ {H ← C.})X ∪ R‡ . Then Cn((P 0 ∪
comes a universal one in r2‡ . {r})X ) = Cn((P 0 ∪ {H ← C.})X ) = Cn((P 0 ∪ {H ←
N(r2 ) = { C.})X ∪ R‡ ) = Cn((P 0 ∪ {r† } ∪ R‡ )X ). Then Cn((P 0 ∪
{r})X ) = X iff Cn((P 0 ∪ {r† } ∪ R‡ )X ) = X.
r2† : phdS(X, D), d(D) ← p(X), not pN (X).
r2‡ : pN (X) ← l(X), gC(X, Y ).} Example 9 (Example 1 continued) Program PU , after
normalization, is Skolemized and grounded. After normal-
and N(PU ) = {r0 , r1 , r2† , r2‡ }. ization and Skolemization, the program no longer contains
The following proposition shows that normalization pre- existential variables. Thus, after grounding, it does not
serves answer sets of an ∃-program: it only adds some atoms contain any more variables.
formed with the new predicate symbols from N .
PG(sk(N(PU ))) = {
Proposition 4 Let P be an ∃-program of language LP and p(a).,
X ⊆ GA(Lsk(P ) ). If X is an ∃-answer set of P then there l(a),
exists Y ⊆ GAN(Lsk(P ) ) such that X ∪ Y is an ∃-answer phdS(a, skD 1
(a)), d(skD1
(a)) ← p(a), not pN (a).
set of N(P ). If X is an ∃-answer set of N(P ) then X \ N
p (a) ← l(a), gC(a, a).,
GAN(Lsk(P ) ) is an ∃-answer set of P . pN (a) ← l(a), gC(a, skD 1
(a)).,
The lemma used in the following proof shows that if the . . .,
normalization is applied on only one rule r and only one part 1 1 1 1 1
phdS(skD (a), skD (skD (a))), d(skD (skD (a))) ←
of the negative body of this rule, then the answer sets of the 1 N 1
p(skD (a)), not p (skD (a)).,
original program are preserved up to the added atom. If r pN (skD1
(a)) ← l(skD 1
(a)), gC(skD 1
(a), a).,
has the following form: N 1 1
p (skD (a)) ← l(skD (a)), gC(skD 1 1
(a), skD (a)).,
H1 , . . . , H n ← ...}
B1 , . . . , Bm , not (N11 , . . . , Nu11 ), . . . , not (N1s , . . . , Nuss ).
The following proposition shows that Skolemization and
then the ”partial normalization” of r for (N1s , . . . , Nuss ) grounding preserve answer sets of a normalized ∃-program.
leads to the rules
r † = H1 , . . . , H n ← Proposition 5 Let P be a normalized ∃-program of lan-
B1 , . . . , B m , guage LP and X ⊆ GA(Lsk(P ) ). X is an ∃-answer set
not (N11 , . . . , Nu11 ), . . . , not (N1s−1 , . . . , Nus−1 ), not Ns . of P if and only if X is an ∃-answer set of PG(sk(P )).
s−1
Proof 5 Since for all r ∈ PG(sk(P )), VN ∃ (r) = ∅ (since Proposition 6 Let P be a ground Skolemized normalized
r is normalized), VN ∃ (r) = V(r) and VH∃ (r) = ∅ (since ∃-program of language LP and X ⊆ GA(LP ). X is an
r is Skolemized) then PG(sk(P )) = sk(PG(sk(P ))) = ∃-answer set of P if and only if X is an ∃-answer set of
PG(sk(PG(sk(P )))). Exp(P ).
By Definition 7, X is an ∃-answer set of P iff X = Proof 6 The only difference is on the computation of the fix-
Cn(PG(sk(P ))X ) iff X = Cn(PG(sk(PG(sk(P ))))X ) point of (classical) TP operator and new TP operator de-
iff X is an ∃-answer set of PG(sk(P )). fined in Definition 6 and clearly enough fix-point are identi-
Once an ∃-program is normalized and Skolemized, the cal since P is ground.
only non-standard parts that remain are the conjunctions of Proposition 7 Let P be an ∃-program.
atoms in rule heads. The last step of the translation is the Exp(PG(sk(N(P )))) is an (ground classical) ASP
expansion where we remove the sets of atoms in each head program.
while keeping the link between the existential variables. It
simply consists to duplicate a rule as many time as the rule Proof 7 This proposition is a direct consequence of Defini-
contains atoms in its head, each new rule having only one tions 3, 4, 8, 9 and Proposition 2.
of these atoms in its head. Preceding Skolemization allows The last proposition establishes equivalence, up to new
to preserve the links between the existential variables of the atoms introduced by normalization, between ∃-answer sets
head. The obtained program is equivalent in terms of answer of an ∃-program and classical answer sets of the program
sets. after normalization, Skolemization and expansion.
Definition 9 Let P be a ground Skolemized normalized pro- Proposition 8 Let P be an ∃-program of language LP and
gram and r ∈ P (m, s ≥ 0, n > 0): X ⊆ GA(Lsk(P ) ). If X is an ∃-answer set of P then
H1 , . . . , Hn ← B1 , . . . , Bm , not N1 , . . . , not Ns . there exists Y ⊆ GAN(Lsk(P ) ) such that X ∪ Y is a
(classical) answer set of Exp(PG(sk(N(P )))). If X is
with H1 , . . . , Hn , B1 , . . . , Bm , N1 , . . . , Ns ∈ GA(LP ). a (classical) answer set of Exp(PG(sk(N(P )))), then
The expansion of such a rule is the set defined by: X \ GAN(Lsk(P ) ) is an ∃-answer set of P .
Exp(r) = Proof 8 Let P be an ∃-program and X ⊆ GA(Lsk(P ) ).
{ H1 ← B1 , . . . , Bm , not N1 , . . . , not Ns ., • if X is an ∃-answer set of P then, by proposition 4,
... there exists Y ⊆ GAN(Lsk(P ) ) such that X ∪ Y is
Hn ← B1 , . . . , Bm , not N1 , . . . , not Ns .} an ∃-answer set of N(P ). By proposition 5, X ∪ Y is
an ∃-answer set of PG(sk(N(P ))). By proposition 6,
S The expansion of P is defined as Exp(P ) =
X ∪ Y is an ∃-answer set of Exp(PG(sk(N(P )))).
r∈P Exp(r). By propositions 3 and 7, X ∪ Y is an answer set of
Example 10 (Example 1 continued) The following rule of Exp(PG(sk(N(P )))).
the program from Example 9: • If X is a (classical) answer set of Exp(PG(sk(N(P ))))
1 1
phdS(a, skD (a)), d(skD (a)) ← p(a), not pN (a). is then, by propositions 3 and 7, X is an ∃-answer set
splitted into the two rules: of Exp(PG(sk(N(P )))). By proposition 6, X is an
1
phdS(a, skD (a)) ← p(a), not pN (a). and ∃-answer set of PG(sk(N(P ))). By proposition 5, X
d(skD (a)) ← p(a), not pN (a).
1
is an ∃-answer set of N(P ). By proposition 4, X \
The same treatment is applied to the other rules with both GAN(Lsk(P ) ) is an ∃-answer set of P .
predicates phdS and d in the head.
The following program is obtained: Conclusion
This paper is a first step of formalisation of ASP allowing
Exp(PG(sk(N(PU )))) = { the use of existential variables. It is well suited to integrate
p(a)., ontologies and rules in a unique formalism.
l(a)., From a practical point of view, the proposed translation
phdS(a, skD 1
(a)) ← p(a), not pN (a)., from ∃-ASP to ASP allows us to use any solver. But let us
d(skD1
(a)) ← p(a), not pN (a)., note that we have implemented this translation as a front-
pN (a) ← l(a), gC(a, a)., end of the solver ASPeRiX which uses on-the-fly grounding
pN (a) ← l(a), gC(a, skD 1
(a))., (Lefèvre et al. 2015). This should help, in the future, for
..., dealing with variables in a more efficient way.
phdS(skD 1 1
(a), skD (skD1
(a))) ← An in-depth comparison with other formalisms remains
to be done. One of the closest work is (Baget et al. 2014b)
p(skD (a)), not pN (skD
1 1
(a)).,
dealing with existential rules extended with non monotonic
d(skD (skD (a))) ← p(skD (a)), not pN (skD
1 1 1 1
(a))., negation. In this work, existential variables are only allowed
N 1 1 1
p (skD (a)) ← l(skD (a)), gC(skD (a), a)., in the rule heads, not in the negative bodies. ASPeRiX se-
pN (skD1
(a)) ← l(skD 1
(a)), gC(skD 1
(a), sk(a))., mantics (defined via a notion of computation inspired from
...} (Liu et al. 2010)) is adapted for defining different chases
(forward chaining algorithms) for non monotonic existen- Bowen, K., eds., Proceedings of the Fifth International Con-
tial rules. Our present work should be linked to one of these ference and Symposium on Logic Programming (ICLP’88),
chases, the Skolem-chase. 1070–1080. Cambridge, Massachusetts: The MIT Press.
Another ongoing work is to deal efficiently with queries in Ianni, G.; Eiter, T.; Tompits, H.; and Schindlauer, R. 2005.
this framework. This is not obvious due to the nonmonotonic Nlp-dl: A kr system for coupling nonmonotonic logic pro-
aspect of ASP and the potential inconsistency of an ASP grams with description logics. In The Forth International
program. It seems that very little work has been done on Semantic Web Conference (ISWC2005).
these aspects. Lee, J., and Palla, R. 2011. Integrating rules and ontolo-
gies in the first-order stable model semantics (preliminary
Acknowledgements report). In Logic Programming and Nonmonotonic Reason-
This work received support from ANR (French National Re- ing - 11th International Conference, LPNMR 2011, Vancou-
search Agency), ASPIQ project reference ANR-12-BS02- ver, Canada, May 16-19, 2011. Proceedings, 248–253.
0003. Lefèvre, C.; Béatrix, C.; Stéphan, I.; and Garcia, L. 2015.
Asperix, a first order forward chaining approach for answer
References set computing. CoRR abs/1503.07717:(to appear in TPLP).
Liu, L.; Pontelli, E.; Son, T. C.; and Truszczynski, M. 2010.
Alviano, M.; Faber, W.; Leone, N.; and Manna, M. 2012.
Logic programs with abstract constraint atoms: The role of
Disjunctive datalog with existential quantifiers: Semantics,
computations. Artificial Intelligence 174(3-4):295–315.
decidability, and complexity issues. Theory Pract. Log. Pro-
gram. 12(4-5):701–718. Magka, D.; Krötzsch, M.; and Horrocks, I. 2013. Computing
stable models for nonmonotonic existential rules. In IJCAI
Baget, J.-F.; Garreau, F.; Mugnier, M.-L.; and Rocher, S. 2013, Proceedings of the 23rd International Joint Confer-
2014a. Extending acyclicity notions for existential rules. In ence on Artificial Intelligence, Beijing, China, August 3-9,
ECAI 2014 - 21st European Conference on Artificial Intelli- 2013.
gence, 18-22 August 2014, Prague, Czech Republic, 39–44.
Motik, B., and Rosati, R. 2010. Reconciling description
Baget, J.-F.; Garreau, F.; Mugnier, M.-L.; and Rocher, logics and rules. J. ACM 57(5).
S. 2014b. Revisiting Chase Termination for Existential
Rules and their Extension to Nonmonotonic Negation. In Rosati, R. 2006. Dl+log: Tight integration of description
Konieczny, S., and Tompits, H., eds., NMR’2014: 15th Inter- logics and disjunctive datalog. In Proceedings, Tenth Inter-
national Workshop on Non-Monotonic Reasoning, volume national Conference on Principles of Knowledge Represen-
INFSYS Research Report Series. tation and Reasoning, Lake District of the United Kingdom,
June 2-5, 2006, 68–78.
Cali, A.; Gottlob, G.; Lukasiewicz, T.; Marnette, B.; and
Pieris, A. 2010. Datalog+/-: A family of logical knowledge You, J.-H.; Zhang, H.; and Zhang, Y. 2013. Disjunctive
representation and query languages for new applications. In logic programs with existential quantification in rule heads.
25th Annual IEEE Symposium on Logic in Computer Sci- Theory and Practice of Logic Programming 13:563–578.
ence (LICS), 2010, 228–242.
de Bruijn, J.; Pearce, D.; Polleres, A.; and Valverde, A.
2010. A semantical framework for hybrid knowledge bases.
Knowl. Inf. Syst. 25(1):81–104.
Eiter, T.; Ianni, G.; Schindlauer, R.; and Tompits, H. 2005.
Dlv-hex: Dealing with semantic web under answer-set pro-
gramming. In 4th International Semantic Web Conference
(ISWC 2005) - Posters Track, Galway, Ireland, November
2005. System poster.
Eiter, T.; Ianni, G.; Lukasiewicz, T.; Schindlauer, R.; and
Tompits, H. 2008. Combining answer set programming with
description logics for the semantic web. Artif. Intell. 172(12-
13):1495–1539.
Eiter, T.; Fink, M.; Krennwallner, T.; and Redl, C. 2013.
hex-programs with existential quantification. In Hanus, M.,
and Rocha, R., eds., Declarative Programming and Knowl-
edge Management, KDPD 2013, volume 8439 of Lecture
Notes in Computer Science, 99–117.
Ferraris, P.; Lee, J.; and Lifschitz, V. 2011. Stable models
and circumscription. Artificial Intelligence 175:236–263.
Gelfond, M., and Lifschitz, V. 1988. The stable model se-
mantics for logic programming. In Kowalski, R. A., and