Abstract

Answer set programming (ASP) is an appropriate formalism to represent various problems issued from artificial intelligence and arising when available information is incomplete. When dealing with information expressed in terms of ontologies in some tractable description logic language, ASP must be extended to handle existential variables. We present the syntax and semantics of an ASP language with existential variables using Skolemization. We formalize its links with standard ASP. This work has led to an implementation.

Introduction

This paper deals with the treatment of ontologies in Answer Set Programming (ASP) (Gelfond and Lifschitz 1988) . We are interested in using ASP technologies for querying large scale multisource heterogeneous web information. ASP is considered to handle, by using default negation, inconsistencies emerging by the fusion of the sources expressed by scalable description logics. Moreover, ASP can enrich the language of ontologies by allowing the expression of default information (for instance, when expressing inclusion of concepts with exceptions). When dealing with ontologies in ASP, the problem stems from the presence of existential variables in description logics which are not expressible in normal logic programs. The present work proposes a definition of ASP with existential variables in order to express, in a unique formalism, ontologies enriched by default negation and rules. Processing existential variables is done in terms of Skolemization.

The study of the combination of ontologies and rules is not new (Rosati 2006; Eiter et al. 2008; de Bruijn et al. 2010; Motik and Rosati 2010 ; Ferraris, Lee, and Lifschitz 2011; Lee and Palla 2011; Magka, Kro¨tzsch, and Horrocks 2013). In most of these models, the knowledge base is viewed as a hybrid knowledge base composed of two parts (T ,P): T is a knowledge base describing the ontological information expressed with a fragment of first-order logic, using for example description logic, and P describes the rules in terms of a logic program.

The miscellaneous attempts to integrate the two formalisms can be distributed into three classes (Eiter et al. 2008; Lee and Palla 2011) .

In the first class (like in (Eiter et al. 2008) ), the two formalisms are handled separately. T is seen as an external source of information which can be used by the logic program through special predicates querying the DL base. The two bases are then independent with their own semantics and the link between the two bases is performed using these special predicates. (Eiter et al. 2013) uses their extension of ASP with external atoms to simulate rules with existential variables in the head (external atoms in the body serve to introduce new null values).

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. Predicates of T can be used in the rules of the program. Nevertheless, there are some restrictions: for instance, these predicates can not be used in the negative part of the body of a rule.

The last case integrates DLs and rules in a unique formalism. For instance, (de Bruijn et al. 2010) uses quantified equilibrium logic (QEL). In this work, several hybrid knowledge bases are defined (with safe restriction, safe restriction without unique name assumption or with guarded restriction) and it is proved that each category and their models can be expressed in terms of QEL.

A large part of these works concerns the questions of complexity and decidability. In these frameworks, existential variables are allowed in the part of the ontological information but are not allowed in the head of the rules.

Next to these models, (Ferraris, Lee, and Lifschitz 2011) proposes a model allowing to cover both stable models semantics and first-order logic by means of a second-order formula issued from the initial information. Its links with the previously cited works have been established in (Lee and Palla 2011) . (You, Zhang, and Zhang 2013) proposes an extension of ASP with existential variables in rule heads whose semantics corresponds to that of (Ferraris, Lee, and Lifschitz 2011) .

Other works in logic programming take their origin in Datalog and extend the language for specifying ontologies. Datalog+/- is a family of such extensions with syntactical restrictions so that decidability is ensured. Several approaches with existential quantified variables based on Datalog+/have been proposed in the literature but some have no non monotonic negation (Alviano et al. 2012) and other have only stratified negation (Cali et al. 2010) . Nevertheless, one important and interesting point of these works is that they focus on queries which is an important issue when dealing with ontologies.

In (Magka, Kro¨tzsch, and Horrocks 2013) , the knowledge base is a single one allowing existential variables and default negation in the same rule. This work studies some conditions of acyclicity and stratification that must be verified by the base ensuring the existence of a unique finite stable model. The work is both theoretical and practical but it is concerned with a limited extension of ASP.

As far as we know, the only works leading to an implementation are those of (Ianni et al. 2005; Eiter et al. 2005) , based on (Eiter et al. 2008) , and of (Magka, Kro¨tzsch, and Horrocks 2013) which has been applied to information about biochemistry.

The aim of our present work is to describe knowledge in a single framework which can lead to useful implementation. We focus on ASP because it is a powerful framework for knowledge representation and provides efficient solvers. The work consists in enriching the ASP framework to take into account existential variables. It can be seen as the other side of the work consisting in introducing nonmonotonicity in existential rules (Baget et al. 2014b; 2014a) .

Next section gives the preliminary notions and definitions useful for the paper. Then, we define programs expressed in 9-ASP, an extension of ASP allowing existential variables, and answer sets on this kind of programs. Last, we give the links between 9-ASP and standard ASP with a method to translate a program expressed in 9-ASP into a program expressed in (standard) ASP and proofs about the transformation.

Preliminaries

In this section, we give the formal definitions of the language and some notions useful in the following of the paper.

The set V denotes the infinite countable set of variables. A language L is defined as a triplet (CS; F S; PS) which denotes respectively the set of constant symbols, the set of function symbols and the set of predicate symbols of the language. It is assumed that the sets V, CS, F S and PS of any language are disjoint. Function ar denotes the arity function from F S to N and from PS to N which associates to each function or predicate symbol its arity.

The set T(L) denotes the set of terms of a language L = (CS; F S; PS) defined by induction as follows: if v 2 V then v 2 T(L), if c 2 CS then c 2 T(L), if f 2 F S with ar(f ) = n > 0 and t1; : : : ; tn 2 T(L) then f (t1; : : : ; tn) 2 T(L).

The set GT(L) denotes the set of ground terms of a language L = (CS; F S; PS) defined by induction as follows: if c 2 CS then c 2 GT(L), if f 2 F S with ar(f ) = n > 0 and t1; : : : ; tn 2 GT(L) then f (t1; : : : ; tn) 2 GT(L).

The set A(L) denotes the set of atoms of a language L = (CS; F S; PS) defined as follows: if a 2 PS with ar(a) = 0 then a 2 A(L), if p 2 PS with ar(p) = n > 0 and t1; : : : ; tn 2 T(L) then p(t1; : : : ; tn) 2 A(L).

The set GA(L) denotes the set of ground atoms of a language L = (CS; F S; PS) defined as follows: if a 2 PS with ar(a) = 0 then a 2 GA(L), if p 2 PS with ar(p) = n > 0 and t1; : : : ; tn 2 GT(L) then p(t1; : : : ; tn) 2 GA(L).

A substitution over a language L is a mapping from the set of variables to the set of the terms T(L). Let t be a term (resp. a an atom) and a substitution, (t) (resp. (a)) is an instance of t (resp. a).

A ground substitution over a language L is a mapping from the set of variables to the set of the ground terms GT(L). Let t be a term (resp. a an atom) and a ground substitution, (t) (resp. (a)) is a ground instance of t (resp. a).

A partial ground substitution for a set of variables V over a language L is a mapping from V to the set of ground terms GT(L). Let t be a term (resp. a an atom) and a partial ground substitution for a set of variables V , (t) (resp. (a)) is a partial ground instance of t (resp. a) w.r.t. the set of variables V .

Syntax and semantics of 9-ASP

In this section, we define a variant of ASP allowing the use of existentially quantified variables (called existential variables in the sequel). The rules proposed here extend classical safe rules (without disjunction) of the form:

H where H; B1; : : : ; Bm; N1; : : : ; Ns are atoms. Safety imposes that all variables that appear in a rule also appear in the positive part of its body. In such a rule, all variables are interpreted as universally quantified. In the sequel, universally quantified variables will be called universal variables.

These classical rules are extended in two ways. First, the head of the rule, atom H, is replaced by a conjunction of atoms and each negated atom Ni is also replaced by a conjunction of atoms. These conjunctions allow multiple atoms to refer to the same existential variable. Second, the safety condition is relaxed by allowing these new conjunctions of atoms to contain variables that do not appear in the positive part of the rule. These variables are interpreted as existential ones.

For example, in the rule (p(X; Y ) q(X); not r(X; Z):), variable X is interpreted as universal, and Y and Z are interpreted as existential. The rule can be read as: “for all X, if q(X) is true and there does not exist Z such that r(X; Z) is true, then one can conclude that there exists Y such that p(X; Y ) is true”.

Definition 1 (9-rule and 9-program) An 9-program P of

language L = (CS; F S; PS) is a set of 9-rules r defined as follows (m; s 0, n; u1; : : : ; us 1): body (r) = ffN11; : : : ; Nu11 g; : : : ; fN1s; : : : ; Nuss gg. V(r) the variables, VH9(r) the variables which are in H1; : : : ; Hn but which are not in B1; : : : ; Bm (i.e. existential variables of the head of r), V9(r)(N1i; : : : ; Nuii ) variables which are in N1i; : : : ; Nuii but not in B1; : : : ; Bm, 1 i s (i.e. existential variables of N1i; : : : ; Nuii ).

VN9(r) = S1 i s V9(r)(N1i; : : : ; Nuii ), VN9(r) = V(r) n VN9(r), V9(r) = VH9(r) S VN9(r) VH8(r) the variables which are at least in H1; : : : ; Hn and in B1; : : : ; Bm (i.e. universal variables of the head of r, the frontier variables).

V8(r)(N1i; : : : ; Nuii ) the variables which are at least in N1i; : : : ; Nuii and in B1; : : : ; Bm (i.e. universal variables of N1i; : : : ; Nuii ).

Moreover, the sets V9(r)(N1i; : : : ; Nuii ) for every 1 i s must be disjoint and the sets VH9(r) and VN9(r) must also be disjoint. (If a variable appears in several of the N1i; : : : ; Nuii or if it appears in H1; : : : ; Hn and in one of the N1i; : : : ; Nuii , 1 i s, then it must appear in B1; : : : ; Bm and it is a universal variable.)

For all rules r of a program P , V9(r) must be disjoint (i.e. all the names of the existential variables of the program are different).

A rule r is a definite rule if body (r) = ; and a program is a definite program if all the rules are definite.

Let us note that in such a rule r, several atoms are allowed in head(r) and in each set of body (r). In this case, a list of atoms must be seen as the conjunction of each atom of the list.

Concerning the variables involved in the rule, they can be quantified universally or existentially. The quantifiers are not explicitly expressed in the rule but they depend on the position in the rule: the variables appearing in body+(r) are universally quantified while the ones not appearing in body+(r) are existentially quantified. Let us note that the existential variables, in the head or in each negative part of the body, are locally quantified.

Example 1 Let PU be an 9-program of language LU = (fag; ;; fp; phdS; d; l; gCg) with ar(p) = ar(d) = ar(l) = 1 and ar(phdS) = ar(gC) = 2. p stands for person, phdS for phDStudent, d for director, l for lecturer and gC for givesCourses.

PU = f r0 : p(a):; r1 : l(a):; r2 : phdS(X; D); d(D) p(X); not(l(X); gC(X; Y )):g

The rule r2 means that for a person X there exists a director D and X is a phD student of D, unless X is a lecturer and it exists a course given by X.

We have VH8(r) = fXg, VH9(r) = fDg, V9(r)(l(X); gC(X; Y )) = fY g, VN9(r) = fX; Dg.

For each program P , we consider that its language LP = (CS; F S; PS) consists of exactly the constant symbols, function symbols and predicate symbols appearing in P . Proposition 1 Any (first-order classical) ASP program is an 9-program.

Proof 1 This is a direct consequence of Definition 1.

The semantics of 9-programs uses Skolemization of existential variables appearing in the heads of the rules. We now define this Skolemization. n = 0 then skY is a Skolem constant symbol).

Definition 2 (Skolem symbols) Let r be an 9-rule, n the

caabrledionfarlittyheonf VskHYn8(irs)aaSnkdolYem2fuVnHct9io(rn)syamnbeoxilsotefnatriaitlyvnar(ii-f

Example 2 (Example 1 continued) Symbol skD1 is a

Skolem function symbol of arity 1 for the existential variable D of the head of the rule r2.

Definition 3 (Skolem Program) Let P be an 9-program of

language LP .

Let s be an ordered sequence of the variables VH8(r) of an 9-rule r of P . sk(r) denotes a Skolem rule obtained from r as follows: every existential variable v 2 VH9(r) is substituted by the term skvn(s) with skvn the Skolem function (constant) symbol associated to v and n = ar(skvn) the size of s (zero if VH8(r) = ;). The Skolem program sk(P) of an 9-program P is defined by sk(P ) = fsk(r)jr 2 P g. Example 3 (Example 1 continued) The Skolem rule of r2 is the rule: sk(r2) = (phdS(X; skD1(X)); d(sk1 (X))

D p(X); not(l(X); gC(X; Y )):) =

Hence sk(PU ) = fr0; r1; sk(r2)g and Lsk(PU ) (fag; fskD1g; fp; phdS; d; l; gCg).

Skolem rules are still not safe: existential variables remain in the negative bodies. The grounding of such a rule is a partial grounding restricted to the universal variables of the rule, the existential ones remaining not ground. Indeed, a non-ground rule (p(X) q(X); not r(X; Z):) could be fired for some constant a if q(a) is true and, for all z, r(a; z) is not true. Suppose two constants a and b. Then (p(a) q(a); not r(a; a):) and (p(a) q(a); not r(a; b):) are not equivalent to the non-ground rule for X = a because the first instance could be fired if r(a; b) is true (but not r(a; a)) and the second could be fired if r(a; a) is true (but not r(a; b)). Yet neither r(a; b) nor r(a; a) should be true for the initial rule to be fired. We thus define a partial grounding, only concerning universal variables. For instance, a partial ground instance of the above non-ground rule would be: (p(a) q(a); not r(a; Z):).

Definition 4 (Partial Ground Program) Set PG(r) for a rule r of an 9-program P of language LP denotes the set of all partial ground instances of r over the language LP for VN9(r). The partial ground program PG(P ) of an 9program P is defined by PG(P ) = Sr2P PG(r). Example 4 (Example 1 continued) The language of the Skolem program sk(PU ) contains only one constant, a, and only one function symbol, sk1 . The set of ground terms is

D infinite and the partial grounding leads then to the following infinite program:

PG(sk(PU )) = f p(a):; l(a):; phdS(a; skD1(a)); d(skD1(a))

p(a); not (l(a); gC(a; Y )):; phdS(skD1(a); skD1(skD1(a))); d(skD1(skD1(a)))

p(skD1(a)); not (l(skD1(a)); gC(skD1(a); Y )):; : : : g Proposition 2 The partial ground program of an 9-program with no multiple head, no multiple default negation and no existential variable is a ground (classical) ASP program. Proof 2 This is a direct consequence of Definitions 1 and 4. Definition 5 (Reduct) Let P be an 9-program of language LP and X GA(Lsk(P )). The reduct of the partial ground program PG(sk(P )) w.r.t. X is the definite partial ground program PG(sk(P ))X = f head(r) body+(r):jr 2 PG(sk(P )); for all N 2 body (r) and for all ground substitution Example 5 (Example 1 continued) Let

X1 = fp(a); l(a); phdS(a; skD1(a)); d(skD1(a))g: Then, for the rule phdS(a; skD1(a)); d(skD1(a))

p(a); not (l(a); gC(a; Y )): there is no ground instance of l(a),gC(a; Y ) that is included in X1 (since X1 does not contain any atom with gC) and the positive part of the rule is kept. Other rules are kept for the same reason. The obtained program is then: over Lsk(P ); (N ) 6

Xg PG(sk(PU ))X1 = f p(a):; l(a):; phdS(a; skD1(a)); d(skD1(a)) p(a):; phdS(skD1(a); skD1(skD1(a))); d(skD1(skD1(a)))

p(skD1(a)):; : : : g

Now, let X2 = X1 [ fgC(a; m)g and PU2 = PU [ fgC(a; m):g.

Here, l(a),gC(a; m) is a ground instance of the negative body of the rule phdS(a; skD1(a)); d(skD1(a)) p(a); not (l(a); gC(a; Y )): that is included in X2. Thus, the rule is excluded from the reduct. Other rules are kept. The obtained program is then: PG(sk(PU [ fgC(a; m):g))X[fgC(a;m)g = f gC(a; m):; p(a):; l(a):; phdS(skD1(a); skD1(skD1(a))); d(skD1(skD1(a)))

p(skD1(a)):; : : : g

Note that the reduct of a program that is Skolemized and partially grounded is a definite ground program: it no longer contains variables. The consequence operator can then be defined as usual, the only difference is that rules can have a conjunction of atoms as head.

Definition 6 (TP consequence operator and Cn its closure) Let P be a definite partial ground program of an 9-program of language LP . The operator TP : 2GA(LP ) ! 2GA(LP ) is defined by

TP (X) = fajr 2 P; a 2 head(r); body+(r) Xg: Cn(P ) = Sn=+1 TPn(;) is the least fix-point of the consen=0 quence operator TP .

Example 6 (Example 1 continued) Cn(PG(sk(PU ))X ) = X but Cn(PG(sk(PU [ fgC(a; m):g))X[fgC(a;m)g) = fp(a); l(a); gC(a; m)g.

Definition 7 (9-answer set) Let P be an 9-program of lan

guage LP and X GA(Lsk(P )). X is an 9-answer set of P if and only if X = Cn(PG(sk(P ))X ).

Example 7 (Example 1 continued) X is an 9-answer set

of PU and fp(a); l(a); gC(a; m)g is an 9-answer set of PU [ fgC(a; m):g.

Proposition 3 Let P be a (classical) ASP program of language LP and X GA(LP ). X is an answer set of P if and only if X is an 9-answer set of P considered as an 9-program.

Proof 3 Since P is a classical ASP program, sk(P ) = P and its (classical) ground ASP program corresponds exactly to PG(P ) = PG(sk(P )). Hence X 2 GA(LP ) = GA(Lsk(P )) is an answer set of ground P , by Definition 7, if and only if it is an 9-answer set of P considered as an 9-program.

From 9-ASP to ASP

In this section, we give the translation of an 9-ASP program into a standard ASP program and we show that the 9-answer sets of the initial program correspond to the answer sets of the new program.

The first step of the translation is the normalization whose goal is twofold: to remove the conjunctions of atoms from negative parts of the rules and to remove existential variables from these negative parts. The obtained program is equivalent in terms of answer sets.

Definition 8 Let P be an 9-program of language LP . Let r be an 9-rule of P (m; s 0, n; u1; : : : ; us 1): with H1; : : : ; Hn; B1; : : : ; Bm; N11; : : : ; Nu11 ; : : : ; N1s; : : : ; Nuss 2 A(LP ). Let N be a set of new predicate symbols (i.e. N \ PS = ;).

The normalization of such an 9-rule is the set of 9-rules

N1s; : : : ; Nuss :g N(r) = f H1; : : : ; Hn B1; : : : ; Bm; not N1; : : : ; not Ns:; N1 N11; : : : ; Nu11 :; : : :

Ns with Ni the new atom pNi (X1; : : : ; Xv), pNi 2 N a new predicate symbol for every Ni and V8(r)(N1i; : : : ; Nuii ) = fX1; : : : ; Xvg.

The normalization of P is defined as N(P ) = Sr2P N(r).

Set GAN(Lsk(P )) is the set of Skolem ground atoms for the new predicate symbols defined as follows: if a 2 N with ar(a) = 0 then a 2 GAN(Lsk(P )), if p 2 N with ar(p) > 0 and t1; : : : ; tn 2 GT(Lsk(P )) then p(t1; : : : ; tn) 2 GAN(Lsk(P )).

Example 8 (Example 1 continued) Let pN be a new predicate symbol. The negative part of the rule r2: not(l(X); gC(X; Y )) has only one universal variable, X. It is replaced by not pN (X) (rule r2y). And a new rule rz 2 is added where Y that was an existential variable in r2 becomes a universal one in r2z.

N(r2) = f r2y : phdS(X; D); d(D) p(X); not pN (X): r2z : pN (X) l(X); gC(X; Y ):g and N(PU ) = fr0; r1; r2y; r2zg.

The following proposition shows that normalization preserves answer sets of an 9-program: it only adds some atoms formed with the new predicate symbols from N . Proposition 4 Let P be an 9-program of language LP and X GA(Lsk(P )). If X is an 9-answer set of P then there exists Y GAN(Lsk(P )) such that X [ Y is an 9-answer set of N(P ). If X is an 9-answer set of N(P ) then X n GAN(Lsk(P )) is an 9-answer set of P .

The lemma used in the following proof shows that if the normalization is applied on only one rule r and only one part of the negative body of this rule, then the answer sets of the original program are preserved up to the added atom. If r has the following form: then the ”partial normalization” of r for (N1s; : : : ; Nuss ) leads to the rules ry = H1; : : : ; Hn

B1; : : : ; Bm; not (N11; : : : ; Nu11 ); : : : ; not (N1s 1; : : : ; Nuss 11 ); not Ns: and rz=Ns N1s; : : : ; Nuss . A program P with the rule r and the program P where the rule r is replaced by the rules ry and rz have the same answer sets except for Ns. The proof can be constructed by induction by applying the lemma to each part of the negative body of r and, then, to each rule of the program.

Proof 4 The proof is by induction on the following lemma: Let P be an 9-program of language LP , r = (H C; not (N1; : : : ; Nu):) 2 PG(sk(P )), P 0 = PG(sk(P )) n frg, ry = (H C; not N:) 2 PG(sk(N(P ))), Rz = PG(N N1; : : : ; Nu:) PG(sk(N(P ))) and X GA(Lsk(P )).

If there exists a substitution such that f (N1); : : : ; (Nu)g X then Cn((P 0 [ frg)X ) = X if and only if Cn((P 0 [ fryg [ Rz)X[fNg) = X [ fN g. If for all substitutions , f (N1); : : : ; (Nu)g 6 X then Cn((P 0 [ frg)X ) = X if and only if Cn((P 0 [ fryg [ Rz)X ) = X.

Let us remark that N 62 Cn(P 0X ) [ X.

If there exists a substitution such that f (N1); : : : ; (Nu)g X then (P 0 [ frg)X = P 0X = (P 0 [ fryg)X[fNg then Cn((P 0 [ f g r )X ) = Cn(P 0X ) and Cn((P 0 [ fryg [ Rz)X[fNg) = Cn(P 0X ) [ fN g. Then Cn((P 0 [ frg)X ) = X iff Cn(P 0X ) = X iff Cn(P 0X ) [ fN g = X [ fN g iff Cn((P 0 [ fryg [ Rz)X[fNg) = X [ fN g.

If for all substitutions , f (N1); : : : ; (Nu)g 6 X then (RPz0)X[ frg)X = (P 0 [ fH C:g)X and (P 0 [ fryg [ = (P 0 [ fH C:g)X [ Rz. Then Cn((P 0 [ frg)X ) = Cn((P 0 [ fH C:g)X ) = Cn((P 0 [ fH Cr:g))XX)[=RXz) =iff CCnn((((PP00 [ fryg [ Rz)X ) = X.

[ fryg [ Rz)X ). Then Cn((P 0 [ f g Example 9 (Example 1 continued) Program PU , after normalization, is Skolemized and grounded. After normalization and Skolemization, the program no longer contains existential variables. Thus, after grounding, it does not contain any more variables.

PG(sk(N(PU ))) = f p(a):; l(a); phdS(a; skD1(a)); d(skD1(a)) p(a); not pN (a): pN (a) l(a); gC(a; a):; pN (a) l(a); gC(a; skD1(a)):; : : :; phdS(skD1(a); skD1(skD1(a))); d(skD1(skD1(a))) p(skD1(a)); not pN (skD1(a)):; pN (skD1(a)) l(skD1(a)); gC(skD1(a); a):; pN (skD1(a)) l(skD1(a)); gC(skD1(a); skD1(a)):; : : : g

The following proposition shows that Skolemization and grounding preserve answer sets of a normalized 9-program. Proposition 5 Let P be a normalized 9-program of language LP and X GA(Lsk(P )). X is an 9-answer set of P if and only if X is an 9-answer set of PG(sk(P )). Proof 5 Since for all r 2 PG(sk(P )); VN9(r) = ; (since r is normalized), VN9(r) = V(r) and VH9(r) = ; (since r is Skolemized) then PG(sk(P )) = sk(PG(sk(P ))) = PG(sk(PG(sk(P )))).

By Definition 7, X is an 9-answer set of P iff X = Cn(PG(sk(P ))X ) iff X = Cn(PG(sk(PG(sk(P ))))X ) iff X is an 9-answer set of PG(sk(P )).

Once an 9-program is normalized and Skolemized, the only non-standard parts that remain are the conjunctions of atoms in rule heads. The last step of the translation is the expansion where we remove the sets of atoms in each head while keeping the link between the existential variables. It simply consists to duplicate a rule as many time as the rule contains atoms in its head, each new rule having only one of these atoms in its head. Preceding Skolemization allows to preserve the links between the existential variables of the head. The obtained program is equivalent in terms of answer sets.

Definition 9 Let P be a ground Skolemized normalized program and r 2 P (m; s 0, n > 0):

H1; : : : ; Hn with H1; : : : ; Hn; B1; : : : ; Bm; N1; : : : ; Ns 2 GA(LP ).

The expansion of such a rule is the set defined by: Exp(r) = f H1 : : : Hn

B1; : : : ; Bm; not N1; : : : ; not Ns:;

B1; : : : ; Bm; not N1; : : : ; not Ns:g The expansion of P is defined as Exp(P ) = Sr2P Exp(r).

Example 10 (Example 1 continued) The following rule of the program from Example 9:

phdS(a; skD1(a)); d(skD1(a)) p(a); not pN (a): is splitted into the two rules: phdS(a; skD1(a)) p(a); not pN (a): and d(skD1(a)) p(a); not pN (a):

The same treatment is applied to the other rules with both predicates phdS and d in the head.

The following program is obtained: Exp(PG(sk(N(PU )))) = f p(a):; l(a):; phdS(a; skD1(a)) p(a); not pN (a):; d(skD1(a)) p(a); not pN (a):; pN (a) l(a); gC(a; a):; pN (a) l(a); gC(a; skD1(a)):; : : : ; phdS(skD1(a); skD1(skD1(a)))

p(skD1(a)); not pN (skD1(a)):; d(skD1(skD1(a))) p(skD1(a)); not pN (skD1(a)):; pN (skD1(a)) l(skD1(a)); gC(skD1(a); a):; pN (skD1(a)) l(skD1(a)); gC(skD1(a); sk(a)):; : : : g Proposition 6 Let P be a ground Skolemized normalized 9-program of language LP and X GA(LP ). X is an 9-answer set of P if and only if X is an 9-answer set of Exp(P ).

Proof 6 The only difference is on the computation of the fixpoint of (classical) TP operator and new TP operator defined in Definition 6 and clearly enough fix-point are identical since P is ground.

Proposition 7 Let P be an 9-program. Exp(PG(sk(N(P )))) is an (ground classical) ASP program.

Proof 7 This proposition is a direct consequence of Definitions 3, 4, 8, 9 and Proposition 2.

The last proposition establishes equivalence, up to new atoms introduced by normalization, between 9-answer sets of an 9-program and classical answer sets of the program after normalization, Skolemization and expansion. Proposition 8 Let P be an 9-program of language LP and X GA(Lsk(P )). If X is an 9-answer set of P then there exists Y GAN(Lsk(P )) such that X [ Y is a (classical) answer set of Exp(PG(sk(N(P )))). If X is a (classical) answer set of Exp(PG(sk(N(P )))), then X n GAN(Lsk(P )) is an 9-answer set of P .

Proof 8 Let P be an 9-program and X GA(Lsk(P )). if X is an 9-answer set of P then, by proposition 4, there exists Y GAN(Lsk(P )) such that X [ Y is an 9-answer set of N(P ). By proposition 5, X [ Y is an 9-answer set of PG(sk(N(P ))). By proposition 6, X [ Y is an 9-answer set of Exp(PG(sk(N(P )))). By propositions 3 and 7, X [ Y is an answer set of Exp(PG(sk(N(P )))).

If X is a (classical) answer set of Exp(PG(sk(N(P )))) then, by propositions 3 and 7, X is an 9-answer set of Exp(PG(sk(N(P )))). By proposition 6, X is an 9-answer set of PG(sk(N(P ))). By proposition 5, X is an 9-answer set of N(P ). By proposition 4, X n GAN(Lsk(P )) is an 9-answer set of P .

Conclusion

This paper is a first step of formalisation of ASP allowing the use of existential variables. It is well suited to integrate ontologies and rules in a unique formalism.

From a practical point of view, the proposed translation from 9-ASP to ASP allows us to use any solver. But let us note that we have implemented this translation as a frontend of the solver ASPeRiX which uses on-the-fly grounding (Lefe`vre et al. 2015) . This should help, in the future, for dealing with variables in a more efficient way.

An in-depth comparison with other formalisms remains to be done. One of the closest work is (Baget et al. 2014b) dealing with existential rules extended with non monotonic negation. In this work, existential variables are only allowed in the rule heads, not in the negative bodies. ASPeRiX semantics (defined via a notion of computation inspired from (Liu et al. 2010) ) is adapted for defining different chases (forward chaining algorithms) for non monotonic existential rules. Our present work should be linked to one of these chases, the Skolem-chase.

Another ongoing work is to deal efficiently with queries in this framework. This is not obvious due to the nonmonotonic aspect of ASP and the potential inconsistency of an ASP program. It seems that very little work has been done on these aspects.

Acknowledgements

This work received support from ANR (French National Research Agency), ASPIQ project reference ANR-12-BS020003.

References

Alviano , M. ; Faber , W. ; Leone, N.; and Manna, M. 2012 .

Disjunctive datalog with existential quantifiers: Semantics, decidability, and complexity issues . Theory Pract . Log. Program. 12 ( 4-5 ): 701 - 718 .

2014a. Extending acyclicity notions for existential rules . In ECAI 2014 - 21st European Conference on Artificial Intelligence , 18 -22 August 2014 , Prague, Czech Republic, 39 - 44 .

Baget , J.-F. ; Garreau , F. ; Mugnier , M.-L.; and Rocher , S. 2014b . Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation . In Konieczny, S., and Tompits , H., eds., NMR'2014: 15th International Workshop on Non-Monotonic Reasoning, volume INFSYS Research Report Series.

Cali , A. ; Gottlob , G. ; Lukasiewicz, T. ; Marnette , B. ; and Pieris , A. 2010 . Datalog+/ -: A family of logical knowledge representation and query languages for new applications . In 25th Annual IEEE Symposium on Logic in Computer Science (LICS) , 2010 , 228 - 242 .

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 programming . 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 Knowledge 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 semantics for logic programming . In Kowalski, R. A., and Bowen , K., eds., Proceedings of the Fifth International Conference and Symposium on Logic Programming (ICLP'88) , 1070 - 1080 . Cambridge, Massachusetts: The MIT Press.

Ianni , G. ; Eiter, T. ; Tompits , H.; and Schindlauer, R. 2005 .

Nlp-dl: A kr system for coupling nonmonotonic logic programs with description logics . In The Forth International Semantic Web Conference (ISWC2005).

Lee , J. , and Palla , R. 2011 . Integrating rules and ontologies in the first-order stable model semantics (preliminary report) . In Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011 , Vancouver, Canada, May 16 -19, 2011 . Proceedings, 248 - 253 .

Lefe `vre, C.; Be´atrix, C.; Ste´phan, I.; and Garcia , L. 2015 .

Asperix , a first order forward chaining approach for answer set computing . CoRR abs/1503 .07717:(to appear in TPLP).

Liu , L. ; Pontelli , E. ; Son , T. C.; and Truszczynski, M. 2010 .

Logic programs with abstract constraint atoms: The role of computations . Artificial Intelligence 174 ( 3-4 ): 295 - 315 .

Magka , D. ; Kro¨tzsch, M.; and Horrocks , I. 2013 . Computing stable models for nonmonotonic existential rules . In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence , Beijing, China, August 3-9 , 2013 .

Motik , B. , and Rosati , R. 2010 . Reconciling description logics and rules . J. ACM 57 ( 5 ).

Rosati , R. 2006 . Dl+log: Tight integration of description logics and disjunctive datalog . In Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning , Lake District of the United Kingdom, June 2-5 , 2006 , 68 - 78 .

You , J.-H. ; Zhang, H.; and Zhang, Y. 2013 . Disjunctive logic programs with existential quantification in rule heads .

Theory and Practice of Logic Programming 13 : 563 - 578 .