First-Order Disjunctive Logic Programming vs Normal Logic Programming

1 Introduction

Answer Set Programming (ASP) has become a predominant declarative programming paradigm [Niemel¨a, 1999; Marek and Truszczynski, 1999] and has been used in many application domains [Baral, 2003] due to its convenience for modeling [Gebser et al., 2012] and its efficient implementations such as clasp.

Although the syntax of ASP is normally presented in a first-order way, the original stable model/answer set semantics is essentially propositional as it is defined by grounding on the Hebrand universe [Gelfond and Lifschitz, 1988; 1991]. More importantly, it enforces the Unique Name Assumption and does not consider unknown objects, which is inadequate for certain application domains to reason about open worlds, e.g., the semantic Web [Eiter, 2007].

To address this issue, a number of approaches have been developed to define the stable model/answer set semantics directly on a first-order level [Bartholomew et al., 2011; Bartholomew and Lee, 2013; Chen et al., 2006; Denecker et al., 2012; Ferraris et al., 2011; Lee and Meng, 2011; Lifschitz, 2012; Lin and Zhou, 2011; Pearce and Valverde, 2004; Shen et al., 2014; Zhang and Zhou, 2010]. Based on which, a new method for answer set solving has been developed [Asuncion et al., 2012a; 2012b].

Similar to classical first-order logic, the answer sets of a first-order logic program are structures. Then, a fundamental problem arises what are the expressive power of different first-order ASP formalisms? In this paper, we study this problem for two of the most important fragments of first-order ASP, namely disjunctive logic programming (DLP) and normal logic programming (NLP). Clearly, NLP is a subclass of DLP. The question is the other way around, that is, whether there exists an equivalent (i.e., having the same set of answer sets) normal program for any given disjunctive program. This problem is not only of theoretical importance but also of practical relevances as it can be applied to utilizing NLP solvers for computing the answer sets of disjunctive programs.

The answer is yes in the propositional case. Eiter et al. [2004] showed that the set of stable models of any propositional disjunctive program can be captured by a normal program. Recently, Zhou [2014] proposed a syntactic translation for this purpose via unfolding and shifting.

However, the answer is no in the first-order case. In this paper, we show that first-order DLP is strictly more expressive than NLP. That is, there exists a first-order disjunctive program, which is not equivalent to any normal program over the same vocabulary.

What if we allow to introduce auxiliary predicates? Note that this is a quite common technique in the KR community. Normally, to encode a problem in ASP, one needs to use auxiliary predicates. We show that, on finite structures, DLP has the same expressive power as NLP by allowing auxiliary predicates if and only if NP = coNP, which is generally believed to be false in the complexity theory.

The above negative results point out that it seems impossible to translate first-order DLP to NLP. Hence, we consider to weaken the conditions. One approach is to consider partially correct translations. In this paper, we propose such a translation based on unfolding and shifting. More precisely, given a disjunctive program, we can add some unfolded rules then shift the program. We show that, the answer sets of the resulting program, which is a normal one, are also answer sets of the original disjunctive program, but not necessarily vice versa. In this sense, this method suggests a sound yet incomplete DLP solver by simply calling NLP solvers.

Another approach is to identify certain translatable subclasses. In this paper, we investigate several NLP-definable subclasses, including head-cycle-free programs and choicebounded programs. We conjecture that, on arbitrary structures, a disjunctive program can be translated into a normal one iff this can be done via unfolding and shifting.

2 Preliminaries

We consider a first-order language with equality but without function symbols. We assume the readers are familiar with some basic notions and notations in classical first-order logic. An atom is called an equality atom if it is of the form t1 = t2, where t1 and t2 are terms. Otherwise, it is called a proper atom. A substitution is a vector x1/t1 · · · , xn/tn, where xi, 1 ≤ i ≤ n are variables and ti, 1 ≤ i ≤ n are terms. A structure is called finite if its domain is finite. Let M be a structure whose vocabulary contains another vocabulary σ. The restriction of M on σ, denoted by M|σ, is the σ-structure that agree with M on all interpretations of predicates and constants in σ. Let M1 andM2 be two structures of two disjoint vocabularies σ1 and σ2 respectively, by M1 ∪M2, we denote the σ1 ∪ σ2-structure that agree with M1 (M2) on all interpretations of predicates and constants in σ1 (σ2 resp.).

Let A be a domain. A ground atom on A is of the form P(-→a ), where P is a predicate and -→a a tuple of elements that matches the arity of P. For convenience, we also use P(-→a ) ∈ M, or M |= P(-→a ), to denote -→a ∈ P M. Let H be a set of ground atoms. We use H ⊆ M, or M |= H, to denote that for every P(-→a ) ∈ H, M |= P(-→a ). For convenience, we also use M ∪ H to denote the structure obtained from M by extending every interpretation of predicates with the corresponding ground atoms in H, i.e., for every P, P M∪H = P M ∪ {-→a | P(-→a ) ∈ H}.

A disjunctive rule (rule for short) is of the form:

where 0 ≤ m ≤ n ≤ k, αi, 1 ≤ i ≤ m is a proper atom, βj (m+1 ≤ j ≤ n) and γs (n+1 ≤ s ≤ k) are atoms. Let r be a rule of the form (1). The head of r, denoted by Head(r), is {α1, . . . , αm}; the body of r, denoted by Body(r), is {βm+1, . . . , βn, not γn+1, . . . , not γk}. For convenience, we use Pos(r) to denote {βm+1, . . . , βn}, the positive body of r, and Neg(r) to denote {not γn+1, . . . , not γk}, the negative body of r respectively. A disjunctive logic program (program for short if clear from the context) is a finite set of rules. A rule is said to be normal if m = 1, and datalog if m = 1 and k = n. Consequently, a program is said to be normal (datalog) if all rules in it are normal (datalog resp.). Let r be a rule of the form (1) and η an assignment from variables and constants to domain elements. A ground rule of r on η is the following rule

We distinguish between intensional and extensional predicates. A predicate P in a program Π is said to be intensional if P occurs in the head of some rules in Π, and extensional otherwise. Let Π be a program. We use τ(Π), τint(Π) and τext(Π) to denote the vocabulary, the intensional vocabulary and the extensional vocabulary of Π respectively.

A number of approaches have been proposed to define the stable model/answer set semantics for disjunctive programs directly on a first-order level. Here, we briefly review the translations to second-order logic [Ferraris et al., 2011] and the progress semantics [Zhou and Zhang, 2011] as they will be needed in our paper.

Given a program Π. Let τint(Π)∗ = {Q∗1 , . . . ,Q∗n} be a new set of predicates corresponding to τint(Π). Given a rule r in Π of the form (1), by ̂ r, we denote the universal closure of the following formula

by r∗ , we denote the universal closure of

By ̂Π, we denote the first-order sentence ∧r∈Π ˆ r; by Π∗ , we denote the first-order sentence ∧r∈Π r∗ .

Let Π be a program. We use SM(Π) to denote the following second-order sentence:

where τint(Π)∗ < τint(Π) is the abbreviation of the formula

Definition 1 A structureMof τ(Π) is called an answer set (or a stable model) of Π if it is a model of SM(Π).

We use AS(Π) to denote the set of answer sets of a program Π. Two programs are said to be equivalent if they have the same set of answer sets. Note that the second-order sentence SM(Π) presented here is slightly different from the one in [Ferraris et al., 2011], mainly because we do not consider nested expressions and quantifiers in this paper. Nevertheless, they are equivalent when restricted into first-order disjunction logic programs.

Now we turn into the progression semantics. Let S be a set and σ = {S1, . . . , St, . . . } a collection of subsets of S. A subset H ⊆ S is a hitting set of σ if for all i, H ∩ Si ̸= ∅. Furthermore, H is said to be a minimal hitting set of σ if H is a hitting set of σ and there is no H′ ⊂ H such that H′ is also a hitting set of σ. Let Π be a program and M a structure of τ(Π). An evolution sequence of Π based on M, denoted by σM(Π), is a sequence σ0M(Π), σ1M(Π), . . . , σtM(Π), . . . of structures of τ(Π) such that

• σ0M(Π) = M|τext(Π) ∪ E|τint(Π), where E is the empty structure in which all predicates are interpreted as empty;
• σt+1 M (Π) = σtM(Π) ∪Ht , where Ht ⊆Mand Ht is a minimal hitting set of the collection of

where there exists a rule r and an assignment η such that Head(r)η ∩ σtM (Π) = ∅, σtM(Π) |= Pos(r)η and M |= Neg(r)η.

An evolution sequence starts with the extensional database. In each step, the structure is expanded by a collection of ground atoms that is a minimal hitting set of the heads of ground rules applicable at the current step. Here, a ground rule is applicable at stage t if its head is not satisfied by the current structure σtM(Π) in the evolution sequence, its positive body is satisfied by σtM(Π) and its negative body is satisfied by the original structure M itself. Notice that at a certain stage, there could be many minimal hitting sets. In this sense, there could be many evolution sequences of a program Π based on a candidate structure M. Nevertheless, if the program is normal, then there is only one minimal hitting set, which is the collection of all heads of ground rules applicable at the current stage. Hence, for normal logic programs, the progression yields a unique evolution sequence.

Definition 2 (Progression semantics) Let Π be a program and M a structure of τ(Π). M is called a stable model (or an answer set) of Π iff there exists at least one evolution sequence, and for all evolution sequence σ of Π based on M, σ∞M(Π) = M, where σ∞M(Π) = ⋃t≥0 σtM(Π).

The progression semantics coincides with the translation stable model semantics [Zhou and Zhang, 2011].

Example 1 [Originated from Example 2 in [Eiter et al., 1997]] Consider the following program 3 - color

This disjunctive program defines the 3-colorability of a graph, whose edges are represented by E(x, y). It can be checked that a stable model of 3-color is corresponding to a 3-coloring solution of the graph, where R(x), G(x) and B(x) mean that the node x should be colored by red, green and blue respectively, and NC means that the graph is not 3-colored.

If we replace the last rule with the following rules

Then, the new program non-3-color defines non-3colorability of the graph. That is, a graph is non-3-colorable iff non - 3 - color has a stable model, which must contain NC. As we shall show later in the paper, while the program 3-color can be converted into a normal one, the program non - 3 - color cannot.

3 NLP<DLP

The same as in classic first-order logic, stable models/answer sets of programs are standard first-order structures. Then, a fundamental problem arises what are the expressive power of different first-order ASP formalisms. The expressiveness problem is one of the most fundamental problems both in the logic community (particularly in model theory and finite model theory) and in the knowledge representation and reasoning community. Moreover, this problem is not only theoretically important but also practically relevant. If one formalism can be expressed by another, then we can use solvers for the latter to solve the former.

In this section, we study the expressive power between first-order DLP and NLP. Clearly, NLP is a subclass of DLP.

The question is the other way around whether DLP can be expressed by NLP, more precisely, for any given disjunctive program, whether there always exists an equivalent normal program, i.e., having the same set of answer sets.

If we consider the propositional case, the answer is yes. Eiter et al. [1994] showed that, from the class of answer sets of a propositional disjunctive program, one can always construct a corresponding normal program. Nevertheless, this translation is purely semantical as the construction needs to know all answer sets in advance. Recently, Zhou [2014] proposed a syntactic translation. More precisely, by adding sufficiently enough unfolded rules into a disjunctive program, the shifted program, which is a normal one, must have the same answer sets.

Now we show that this is not the case for the first-order case. That is, there exists a first-order disjunctive program whose answer sets cannot be captured by any normal program over the same vocabulary.

Theorem 1 NLP < DLP.

Proof: sketch We show that the program non-3-color presented in Example 1 cannot be encoded into NLP over the same vocabulary. Assume that Π0 is equivalent to non-3-color. Then, given a graph represented by the only extensional predicate E, if it is 3-colorable, then Π0 has no answer sets, else if it is non-3-colorable, then Π0 has exactly one answer set, whose intensional database contains NC and the full interpretations of R, G and B. The following two lemmas are needed in our proof.

Lemma 1 Suppose that G1, . . . ,Gn are non-3-colorable graphs. There exists a non-3-colorable graph G such that for any Gi, 1 ≤ i ≤ n, Gi is not a subgraph of G.

Proof: By the Haj´os construction [Jensen and Toft, 2011], there are infinite number of 4-critical graphs, which are non-3-colorable graphs but any subgraph is 3-colorable. □

Lemma 2 Let G1 = 〈V1,E1〉 and G2 = 〈V2,E2〉 be two 3colorable graphs such that V1 ∩V2 is a singleton a. Then, the union G1 ∪G2 = 〈V1 ∪ V2, E1 ∪E2)〉 is 3-colorable as well.

Step 1: The program obtained from Π0 by adding the following rules is also equivalent to non-3-color:

We denote this program by Π1.

Step 2: Let Π2 be the program obtained from Π1 by deleting all rules not from the above ones but whose negative parts mention some intensional predicates. Then, Π2 is also equivalent to non-3-color.

A stable model M of a program containing the rules above must have full interpretations on all intensional predicates. For a ground rule r whose negative part mentions some intensional predicates, its negative part will never be satisfied by M. Hence, M |= ˆ r. Therefore, M is a model of a program ̂ Π1 iff M is a model of ̂ Π1\{r}.

Step 3: Consider the rules in Π2. Other than the above added rules in Step 1, Π2 only has rules in which the negative bodies mention no intensional predicates. Let r be a ground rule of some rule in Π2. Notice that the extensional ground atoms in the positive body of r form a graph whose nodes are the mentioned domain elements and whose edges are specified by the positive extensional ground atoms in the body of r. In this case, we say that this is the graph represented by r. Moreover, we say that r represents a non-3-colorable graph if the graph represented by r is non-3-colorable. Otherwise, we say that r represents a 3-colorable graph.

By Lemma 1, there exists a sufficiently large graph G0, which is non-3-colorable and any non-3-colorable graph represented by some ground rule in Π2 is not a subgraph of G0. However, the structure G+0 , which takes all edges in G0 for the extensional predicate E and the full interpretations for all intensional predicates, is an answer set of Π2 since G0 is non3-colorable. Note that for any ground rule r that represents a non-3-colorable graph, r will not be used in the progression of Π2 based on G+0 . In other words, all ground rules applicable in the progression of Π2 based on G+0 must represent some 3-colorable graph.

Now we consider the earliest stage deriving NC in the progression of Π2 based on G+0 . Suppose that NC is justified by such a ground rule r1 whose positive body contains some intensional ground atoms of the form R(a) (or G(a), B(a)) and r1 represents a 3-colorable graph G1. Then, those ground atoms in the positive body of r1 will be justified by other ground rules earlier in the progression, and those ground rules represent 3-colorable graphs as well. Furthermore, the ground atoms in those rules will be justified even earlier. Then, this forms a tree, where each node is a ground atom and each edge forms a justification/dependency relationship. Nevertheless, the depth of this tree is bounded since NC is justified at a finite step in the progression. We construct a graph GNC associated with this tree. Started from G1, if one ground atom R(a) in r1 is justified by another rule r2 with a G2 to represent its body, then we consider the union of G1 ∪ G′2 , where G′2 is G2 with all nodes except node a renamed to new constants. By Lemma 2, G1 ∪ G′2 is 3-colorable as well. Hence, we obtain a finite graph GNC to justify NC. By induction on the structures and Lemma 2, GNC is 3-colorable since all Gi's in the rules are 3-colorable.

Similarly, we can obtain a 3-colorable graph GR(a) (GG(a) and GB(a) respectively) to justify an intensional ground atom R(a) (G(a) and B(a) respectively). Finally, we construct a graph G recursively as follows. The construction starts from GNC. At each step, for each node b in the current graph, we construct a graph GR(b) (GG(b) and GB(b) respectively), which is obtained from GR(a) (GG(a) and GB(a) respectively) by renaming the node a to b and other nodes to new constants. Then, we take the union of the current graph and all such newly constructed graphs together. On one side, G is a 3-colorable graph by Lemma 2. On the other side, G+, the structure expanded form G by full interpretations on all intensional predicates, is a stable model since all intensional ground atoms can be justified, a contradiction. □

Theorem 1 is only concerned with the expressive power over the same vocabulary, which is the standard concept of expressiveness from a (finite) model theory point of view.

Nevertheless, from a knowledge representation and reasoning point of view, auxiliary predicates are often allowed when talking about translations from one KR formalism to another. Using auxiliary predicates is a quite common technique in the ASP community. Normally, to encode a problem in ASP, one needs to use auxiliary predicates, e.g. the predicate otherroute in the well known Hamiltonian circuit program [Niemel¨a, 1999].

A problem arises whether Theorem 1 still holds if auxiliary predicates are allowed. On finite structures, this is not possible providing some general assumptions in the complexity theory. As shown in the literature, while normal logic programming under the stable model semantics exactly captures the complexity class NP [Sacc`a, 1997; Schlipf, 1995; Marek and Remmel, 2003; Dantsin et al., 2001], disjunctive logic programming under the stable model semantics exactly captures the complexity class ΣP2 [Eiter et al., 1997; Dantsin et al., 2001]. Hence, on finite structures, NLP =∗ DLP if and only if NP = Σ P 2 if and only if NP = coNP.

4 A Partial Translation via Unfolding and Shifting

The previous section shows that, unlike the propositional case, first-order DLP is strictly more expressive than firstorder NLP, even if auxiliary predicates are allowed. Hence, it seems impossible to develop a faithful translation T from first-order DLP to NLP in the sense that for any disjunctive program Π, T (Π) is a normal program and AS(Π) = AS(T (Π)|τ (Π)).

In order to still utilizing NLP solvers for implementing first-order DLP, we consider to weaken the conditions. We investigate two approaches in this direction. One is to consider partially correct translations and another is to consider NLP definable subclasses of first-order DLP.

In this section, we propose a sound but incomplete translation via unfolding [Brass and Dix, 1999; Sakama and Seki, 1997] and shifting [Gelfond et al., 1991; Ben-Eliyahu and Dechter, 1994]. Unfolding and shifting are two classical operators in the literature that have been widely used. Interestingly, it is only till recently to observe that these two operators can be used to fully translate propositional disjunctive programs to normal ones [Zhou, 2014]. More precisely, by unfolding sufficiently enough rules in any given propositional disjunctive program, its shifted program, which is a normal one, must have the same answer sets.

Nevertheless, according to Theorem 1, this result cannot be lifted into the first-order case. It remains an interesting question why this is the case. Let us recall the proof ideas in the propositional case, which can be divided into three assertions. First, adding any unfolded rule into a program does not affect the answer sets. Second, for programs closed under unfolding, i.e., any unfolded rule must be in the program itself, the shifted program has the same answer sets. Finally, by adding sufficiently enough unfolded rules, a propositional disjunctive programmust be closed under unfolding. In this section, we shall show that, while the first two assertions remain true in the first-order case, the last one is not.

Let r1 and r2 be two rules, P(-→t ) an atom in Head(r1)

and η a substitution such that P(-→t )η ∈ Pos(r2). Then, the rule obtained by unfolding P(-→t ) on r1 and r2 with respect to η, denoted by Unfold(r1, r2, P(-→t )η) is a new rule whose head is (Head(r1)\P(-→t ))η ∪Head(r2) and whose body is Body(r1)η∪(Body(r2)\P(-→t )η). Let r be a rule of the form (1). The result of shifting r, denoted by Shift(r), is the set of following rules {αi ← Body(r), not {Head(r)\αi}}, where 1 ≤ i ≤ m and not {Head(r)\αi} is the set {notα | α ∈ Head(r), α ̸= αi}.

Example 2 Consider the following program:

Clearly, it has a unique answer set, which contains full interpretations of both P and Q. Shifting the program, the first rule will be replaced by

The shifted program has no answer sets. Nevertheless, if we add the unfolded rule (i.e., P(x)) of the first two rules w.r.t. the substitution from ⃗x to itself into the program, then the shifted program has the same answer sets.

Theorem 2 Let Π be a first-order disjunctive program. Let Π′ be a program obtained from Π by iteratively adding some unfolded rules. Then, AS(Shift(Π′ )) ⊆ AS(Π).

Proof: sketch This assertion follows from a) for all programs Π and all unfolded rules Unfold(r1, r2, P(-→t )η), AS(Π) = AS(Π ∪ Unfold(r1, r2, P(-→t )η)); and b) for all programs Π, AS(Shift(Π)) ⊆ AS(Π). For a), we show that |= SM(Π) ≡ SM(Π ∪ Unfold(r1, r2, P(-→t )η)), which follows from the fact that |= ̂Π ≡ ̂ Π∪ Unfold(r1, r2, P(-→t )η) and τint(Π)∗ < τint(Π) |= ̂ Π∗ ≡ ̂ (Π∪ Unfold(r1, r2, P(-→t )η))∗ . For b), we are able to show that |= SM(Shift(Π)) → SM(Π). □

Theorem 3 Let Πbe a first-order disjunctive programclosed under unfolding. Then, AS(Shift(Π)) = AS(Π).

Proof: sketch It suffices to show that AS(Π) ⊆ AS(Shift(Π)). If Π is closed under unfolding, then for any answer set M of Π, there exists a unique evolution sequence σ such that σ1M(Π) = M = σ∞M(Π). Then, it can be checked that for Shift(Π), σ1M(Shift(Π)) = σ1M(Π) = M = σ∞M(Shift(Π)). Hence, M is an answer set of Shift(Π) as well. □

Theorem 2 shows that one can still use unfolding and shifting to convert a first-order disjunctive program into a normal one. However, this is just a partially correct translation. In case that the program is closed under unfolding by adding a number of unfolded rules, Theorem 3 guarantees that the converse holds as well. Nevertheless, unlike the propositional case that the program will eventually be closed under unfolding since the number of propositional rules are finite, for firstorder programs, unfolding may never end.

Example 3 Consider again the program non - 3 - color in Example 1. It can be shown that for any non-3-colorable graph G, the rule NC ← BodyG can be obtained from non-3-color by iteratively unfolding some rules. By Lemma 1, there are infinitely many non-3-colorable graphs. Hence, for the non-3-color program, no matter how many unfolded rules are added, it is not closed under unfolding. Therefore, the converse of Theorem 2 does not hold for non - 3 - color as there are always bigger non-3-colorable graphs that cannot be covered by the unfolded rules.

Theorem 2 enables us to develop a sound yet incomplete first-order disjunctive ASP solver by calling an NLP solver. The basic idea is to perform the unfolding operation for some rules in a given disjunctive program and then perform the shifting operation. Calling an NLP solver for the shifted program, if there exists an answer set, then, guaranteed by Theorem 2, it must be an answer set of the original disjunctive program. In case that no answer sets is found, one can obtain some information in the solving process. Based on which, one can construct new rules to be unfolded and continue the above processes. As shown in Example 3, this process might not end in the first-order case so that the procedure might be incomplete. The key issue is how to deliberately select those rules to be unfolded based on the information obtained when failing to find an answer set for the shifted program. We leave this as one of our focuses for future investigations.

5 NLP Definable Subclasses

In this section, we consider to identify some NLP definable subclasses for DLP. Of course, the class NLP itself is a trivial case. Also, all propositional disjunctive programs form another class [Eiter et al., 2004; Zhou, 2014]. Pointed out by Theorem 3, the class of all disjunctive programs closed under unfolding is an NLP definable class as well.

In the literature, particularly for propositional disjunctive programs, a well known class that has attracted much attention is so-called head-cycle-free programs [Ben-Eliyahu and Dechter, 1994]. It is shown that, in the propositional case, all head-cycle-free programs can be encoded in NLP, in particular, by its shifted program. One can lift this into the firstorder case. Let Π be a disjunctive program. The predicate dependency graph of Π, is a directed graph whose nodes are intensional predicates in Π, and there is an edge from a predicate P to another predicate Q iff there exists r ∈ Π such that Head(r) mentions P and Body(r) mentions Q. A loop L of the program Π is a cycle in the predicate dependency graph going through all nodes in L. Then, Π is said to be head-cycle-free if there is no loop L and rule r such that L contains two or more occurrences of predicates mentioned in Head(r). Clearly, all NLP programs are head-cycle-free.

Example 4 The program 3-color presented in Example 1 is head-cycle-free, while the program non-3-color is not since {NC,R,G,B} forms a loop that contains 3 predicates in the first disjunctive rule. The program presented in Example 2 is not head-cycle-free either.

It is shown that, in the propositional case, all head-cyclefree disjunctive programs are equivalent to their shifted programs [Ben-Eliyahu and Dechter, 1994]. This result can be lifted into the first-order case by using a similar technique. Nevertheless, head-cycle-free is a sufficient but not necessary condition for NLP definability. For instance, the program presented in Example 2 is not head-cycle-free but NLP definable. In this section, we consider whether we can characterize NLP definability for first-order disjunctive programs, similar to the notion of boundedness to characterize first-order definability for datalog programs [Ajtai and Gurevich, 1994] and NLP programs [Zhang and Zhou, 2010]. Recall the notion of boundedness for normal logic programs [Zhang and Zhou, 2010]. A normal program Π is said to be bounded if there exists a natural number k such that for all answer setsMof Π, the progression of Π based on M will end within k-steps. On arbitrary structures, a normal program is first-order definable if and only if it is bounded [Zhang and Zhou, 2010].

Analogously, we can extend the notion of boundedness for disjunctive programs. Naturally, a disjunctive program Π is said to be bounded if there exists a natural number k such that for all answer sets M of Π, the progression of Π based on M will end within k-steps. However, boundedness itself alone can capture neither first-order definability nor NLP definability for disjunctive programs. For instance, the non-3-color program presented in Example 1 is bounded within 2 steps, but it is neither first-order definable nor NLP definable over the same vocabulary.

Let us consider the differences between first-order disjunctive programs and normal programs from a progression semantics point of view. It can be observed that a key point is that, for normal programs, there is a unique evolution sequence, while for disjunctive programs, there could be many. In this sense, the number of (nondeterministic) choices in progression indeed makes a big difference. The following theorem states that if a disjunctive program only has a bounded number of choices, i.e., different evolution sequences, then it can be encoded in NLP. Let Π be a first-order disjunctive program. If there exists a number k such that for all answer setsMof Π, |ES(Π,M)| < k, where ES(Π,M) is the set of all evolution sequences of Π based onM, then we say that Π is choice-bounded.

Theorem 4 Choice-bounded programs are NLP definable.

Proof: sketch We first can show that if |ES(Π,M)| = 1 for all answer sets M of Π, then AS(Π) = AS(Shift(Π)). If there is only one evolution sequence for M on Π, then it must coincide with the unique evolution sequence of Shift(Π) based on M. Then, σ∞M(Shift(Π)) = σ∞M(Π) = M. Next, we show that unfolding can always reduce the number of choices. This is because by unfolding some rules in the program, one can obtain more heads in each progression step so that the number of choices are reduced. Finally, by Theorem 2, this assertion holds. □

In fact, many NLP definable classes mentioned previously belong to this class. Clearly, all NLP programs are choicebounded with a bound to be 1. All programs closed under unfolding are choice-bounded as well. Also, all propositional disjunctive programs are choice bounded since the number of propositional variables in a program is finite. This also provides an alternative proof why all propositional disjunctive programs can be translated into normal ones. However, headcycle-free programs are not necessarily choice-bounded.

Example 5 Consider the following program:

This program is head-cycle-free as the two predicate loops {P, Q} and {P , Q} do not go through two or more predicates in the heads of any rule. On the other side, this program is not choice-bounded as one can have an arbitrary guess of P (or Q) at the first step of progression.

Hence, head-cycle-free and choice-bounded are two disjoint NLP definable subclasses. Interestingly, both of them are highly related to the notion of unfolding and shifting. Head-cycle-free programs are equivalent to their shifted programs, while choice bounded programs can be converted to normal programs via unfolding and shifting. In addition, for first-order definability of NLP programs, unfolding also plays a key role. That is, a normal logic program is first-order definable iff it is bounded by a number k iff it is equivalent to its completion on the program by unfolding all possible rules k times [Zhang and Zhou, 2010]. Based on the evidences, we end up with our discussions with a conjecture.

Conjecture 1 On arbitrary structures, a disjunctive program is NLP definable iff it is equivalent to the shifted program of this program expanded with some unfolded rules.

6 Conclusion

In this paper, we have studied the expressive power of firstorder DLP and first-order NLP. Interestingly, unlike the propositional case, first-order DLP is strictly more expressive than NLP (see Theorem 1). Despite these negative results, we are still able to take advantage of NLP solvers for solving first-order DLP by further weakening the conditions. For instance, we have obtained a partially correct translation from first-order DLP to NLP via unfolding and shifting (see Theorem 2). This enables us to develop a sound but incomplete DLP solver, which is one of our focuses in our future work. Also, we have identified some NLP definable subclasses of DLP, including head-cycle-free programs and choice-bounded programs (see Theorem 4). We conjecture that, on arbitrary structures, a disjunctive program is NLP definable iff this can be done via unfolding and shifting. We leave this problem open to our future investigations.