First-Order Expressibility and Boundedness of Disjunctive Logic Programs

1 Introduction

Disjunctive logic programming enhances the traditional logic programming in both the expressive power and the ability to represent indefinite knowledge. It has been widely recognized as a powerful formalism for database querying [Eiter et al., 1997], knowledge representation and declarative problem solving [Baral, 2003]. The dominating semantics for it in these areas is the stable model semantics [Gelfond and Lifschitz, 1988; Ferraris et al., 2011; Lin and Zhou, 2011], or equivalently the minimal model semantics if no default negation is involved [Lobo et al., 1992].

However, a main drawback of this formalism is its high undecidability or intractability [Chomicki and Subrahmanian, 1990; Eiter and Gottlob, 1997; Eiter et al., 1997]. Therefore, one of the central issues of this formalism is to find tractable or manageable fragments. Identifying first-order expressible fragments is a rather natural way to achieve this goal. In this way, we can then reduce the computations for disjunc-

ample, first-order theorem provers for Prolog-style inference, and SAT or SMT solvers for answer-set solving on finite domains.

Recently, a lot of works have been devoted to this task. For example, the first-order expressibility via a single sentence without and with auxiliary predicates were studied by [Cabalar et al., 2009; Bartholomew and Lee, 2010; Zhang and Ying, 2010; Zhang and Zhou, 2010; Chen et al., 2010; 2011; Ferraris et al., 2011; Lee and Meng, 2011; Lifschitz and Yang, 2012] and [Asuncion et al., 2012a; 2012b] respectively, and the first-order expressibility via a possibly infinite theory on finite structures was studied by [Chen et al., 2006]. However, almost all of these works were focusing on only sufficient or only necessary conditions for the first-order expressibility. Unlike them, we are interested in finding conditions that exactly capture the three kinds of first-order expressibility mentioned above. To assure these conditions are useful in identifying first-order expressible fragments, we hope it is intuitively easy to verify whether or not they are satisfied.

The candidate that we choose for such conditions, the boundedness, originally comes from the area of mathematical logic [Moschovakis, 1974; Barwise and Moschovakis, 1978], and has then been thoroughly studied by the community of Datalog as a valuable tool for Datalog optimization [Abiteboul et al., 1995]. An elegant boundedness characterization of the first-order expressibility for Datalog was independently obtained by [Kolaitis and Papadimitriou, 1990] and [Ajtai and Gurevich, 1994]. Therefore, a natural problem is whether or not it can be generalized to the disjunctive case. As the progression on a disjunctive logic program is significantly different from that on a definite one, it is a challenging problem.

In this paper, we first show that the three kinds of first-order expressibility coincide under the stable model semantics. To solve the problem mentioned above, a fixed point semantics, which was proposed in [Lobo et al., 1992] for negation-free disjunctive logic programs over Herbrand structures, is then generalized to disjunctive logic programs with default negation over arbitrary structures. By using the technique of ultraproducts, we prove that a disjunctive logic program without default negation is bounded based on this semantics if and only if it is equivalent to a first-order sentence. For the case with default negation, we also propose a definition for the boundedness and show that it implies the first-order expressibility.

2 Preliminaries

Vocabularies are assumed to be sets of predicate constants and function constants. Every constant is equipped with a natural number, its arity. Nullary function constants are also called individual constants, and nullary predicate constants are called proposition constants. For some technical reasons, a vocabulary is allowed to contain an arbitrary infinite set of proposition constants. Logical symbols are defined as usual, including a countable set of predicate variables and a countable set of individual variables. Predicate constants and variables are simply called predicates if no confusion occurs. Terms, formulae, and sentences of a vocabulary υ (or shortly, υ-terms, υ-formulae, and υ-sentences) are built from υ, equality, and variables in a standard way. The only thing which may be special is that we treat ¬ϕ as a shorthand of ϕ → ⊥, and ϕ ↔ ψ as the conjunction of ϕ → ψ and ψ → ϕ.

For all formulae ϕ and theories Σ, let υ(ϕ) and υ(Σ) be the sets of all constants occurring in ϕ and Σ respectively. If ¯x = x1 · · · xm, τ is the set of Xj for all 1 ≤ j ≤ n, xi and Xj are individual and predicate variables respectively, by Q¯x and Qτ we denote quantifier blocks Qx1 · · · Qxm and QX1 · · · QXn respectively, where Q is ∀ or ∃. A first-order (second-order) formula of the form ∀¯xϑ (∀τϑ, respectively) is universal if ϑ is first-order (second-order, respectively) quantifier-free.

Every structure A of a vocabulary υ (or shortly, υ-structure A) is accompanied by a nonempty set A, the domain of A, and interprets each n-ary predicate constant P in υ as an nary relation P A on A, and interprets each n-ary function constant f in υ as an n-ary function f A on A. A structure is finite if its domain is finite; otherwise it is infinite. Given two υ-structures A, B with the same domain and a set τ of predicates, we write A ≼τ B if the interpretation of each predicate from τ in A is a subset of that in B, and interpretations of the other predicates and functions in A are the same as that in B; we write A ≺τ B if A ≼τ B holds but B ≼τ A does not.

Every assignment in a structure A is a function α that maps each individual variable to an element of A and that maps each predicate variable to a relation on A of the same arity. Given an υ-formula ϕ and an assignment α in A, we write (A, α) |= ϕ if α satisfies ϕ in A in the standard way. In particular, if ϕ is a sentence, we simply write A |= ϕ, and say A is a model of ϕ, or in other words, A satisfies ϕ.

Let τ be a set of predicates and let ϕ be any first-order sentence. We say ϕ is positive with respect to τ if it is in the smallest set that contains all atoms, and the negation of atoms not involving any predicate in τ , and that is closed under connectives ∧, ∨ and first-order quantifiers ∃, ∀; ϕ is negative with respect to τ if ¬ϕ is equivalent to a sentence positive with respect to τ. By a routine induction on the structure of formulae, we can then obtain the following property:

Proposition 1. Let τ be a set of predicates and let A,B be two structures such that A ≼τ B. Let ϕ be any first-order sentence which is positive (negative) with respect to τ. Then B is a model of ϕ if (only if, respectively) A is a model ϕ.

For the propositional case, a slightly stronger version of the above proposition is still true. A positive clause is defined to be a finite disjunction of atoms. Given a vocabulary υ, let PC(υ) be the set of all positive clauses of υ. Now, we give the following property without a proof since it is in fact the same as that of Theorem 1.2.16 in [Chang and Keisler, 1990].

Proposition 2. Let υ be a set of proposition constants and suppose M, N ⊆ υ. Then M ⊆ N iff for all positive clauses γ ∈ PC(υ), N is a model of γ whenever M is a model of γ.

2.1 Circumscription

For the notion of circumscription we follow [Lifschitz, 1985], but do not use varying constants. Let ϕ be a first-order sentence and τ a finite set of predicate constants. For each predicate P in τ we introduce a new predicate variable P ∗ of the same arity. Let τ ∗ be the set of all predicate variables P ∗ where P is in τ . For the sake of convenience, we write τ ∗ = τ for the formula ∧P∈τ∀¯x(P ∗ (¯x) ↔ P(¯x)), write τ ∗ ≤ τ for the formula ∧P∈τ∀¯x(P ∗ (¯x) → P(¯x)), and write τ ∗ < τ for the formula τ ∗ ≤ τ ∧ ¬(τ ∗ = τ). The circumscription CIRC(ϕ; τ) of ϕ with respect to τ is defined to be the secondorder sentence ϕ ∧ ∀τ ∗ (τ ∗ < τ → ¬ϕ(τ ∗ )), where ϕ(τ ∗ ) is the formula obtained from ϕ by substituting the variable P ∗ for each constant P of τ . A structure A is called a τ -minimal model of ϕ if A is a model of ϕ, and no model B of ϕ satisfies B ≺τ A. The following well-known property shows that translation CIRC captures the minimal model semantics.

Proposition 3. Let ϕ be a first-order sentence. A structure A is a τ-minimal model of ϕ iff it is a model of CIRC(ϕ; τ).

2.2 General Stable Model Semantics

Similarly, the stable model semantics is also defined by a second-order translation. Given a first-order sentence ϕ and a finite set τ of predicate constants, let SM(ϕ; τ) stand for the second-order sentence ϕ ∧ ∀τ ∗ (τ ∗ < τ → ¬ST(ϕ; τ)), where the formula ST(ϕ; τ) is defined recursively as follows:

• ST(P(¯ t); τ ) = P ∗ (¯ t) if P is a predicate in τ.
• ST(ψ; τ) = ψ if ψ is an atom not in the previous case.
• ST(ψ ◦ χ; τ) = ST(ψ; τ) ◦ ST(χ; τ) if ◦ ∈ {∧, ∨}.
• ST(ψ →χ; τ) = (ψ →χ) ∧ (ST(ψ; τ) → ST(χ; τ)).
• ST(Qxψ; τ) = QxST(ψ; τ) if Q ∈ {∀, ∃}.

A structure A is called a τ-stable model of ϕ if it is a model of SM(ϕ; τ). A predicate constant is said to be intensional if it occurs in τ. Otherwise, it is extensional. For more information about this, please refer to [Ferraris et al., 2011].

2.3 Logic Programs

Every disjunctive logic program is a set of rules of the form

where 1 ≤ m ≤ n, and for each integer m < i ≤ n, ζi is an atom without equality; for each integer 1 ≤ j ≤ m, ζj is a literal, i.e., an atom or its negation. The disjunctive part of the rule is called its head, and the conjunctive part called its body. Let Π be a disjunctive logic program. Then each intensional predicate of Π is a predicate constant that occurs in the head of some rule in Π. We say Π is normal if the head of each rule contains at most one literal, Π is plain if no negative literal involving an intensional predicate occurs in any of its rules, Π is propositional if no predicate of positive arity occurs in any of its rules, and Π is finite if it contains only a finite set of rules. In particular, unless mentioned otherwise, a logic program is always assumed to be finite.

For convenience, we regard each disjunctive logic program as the conjunction of all sentences ∀¯xγ such that γ is a rule in it and that ¯x consists of all individual variables occurring in γ. Let Π be a finite disjunctive logic program Π and let τ be the set of all intensional predicates of Π, we let CIRC(Π) and SM(Π) denote the formulae CIRC(Π; τ) and SM(Π; τ) respectively. Every τ-minimal (τ-stable) model of Π is simply called a minimal (stable, respectively) model of Π. It is easy to see that SM(Π) is equivalent to CIRC(Π) if Π is plain.

Let A be a structure and τ a set of predicates. For every kary predicate P in τ and every k-tuple ¯a on A, we introduce P¯a as a new proposition constant. Define INS(A, τ) to be the set of proposition constants P¯a such that P (¯a) is true in A and P is in τ . Given a rule γ and an assignment α in A, let γ[α] be the rule obtained from γ by substituting P¯a for all atoms P (¯ t) such that ¯a = α(¯ t), let γB be the set of all literals in the body in which no intensional predicate positively occurs, and let γ+ be the rule obtained from γ by removing all literals in γB . Given a disjunctive logic program Π, let ΠA be the set of rules γ+[α] for all assignments α in A and all rules γ in Π such that α satisfies γB in A. The following proposition asserts that the general stable model semantics for logic programs can be redefined by the first-order GL-reduction defined above.

Proposition 4. Let Π be a disjunctive logic program with a set τ of intensional predicates. Then an υ(Π)-structure A is a stable model of Π iff INS(A, τ) is a minimal model of ΠA .

Proof. Similar to Theorem 1 in [Ferraris et al., 2011].

3 First-Order Expressibility

As mentioned in the first section, there are three kinds of firstorder expressibility having been studied. In this section, we study the relationship among them over arbitrary structures.

Definition 1. Given a second-order formula ϕ, we say ϕ is first-order expressible if it is equivalent to a first-order formula, ϕ is pseudo-first-order expressible if it is equivalent to an existential second-order formula, and ϕ is weak-first-order expressible if it is equivalent to a first-order theory.

Intuitively, the last two kinds of expressibility are strictly stronger than the first one. But surprisingly, the following result shows this is not true for a large family of semantics.

Proposition 5. Let ϕ be a universal second-order formula. Then the following statements are equivalent:

1. ϕ is first-order expressible;
2. ϕ is weak-first-order expressible;
3. ϕ is pseudo-first-order expressible.

Proof. Clearly, both "1=⇒2" and "1=⇒3" are trivial, and "3=⇒1" follows from the fact that every universal secondorder formula whose negation is equivalent to a universal second-order formula should be first-order expressible. This fact is an immediate consequence of Craig's interpolation theorem for first-order logic. Please refer to Subsection 2.5.2 of [vanBenthem and Doets, 1983] for a statement. Now, it remains to show "2=⇒1". Assume there is a first-order theory Σ that is equivalent to ϕ, and suppose ϕ is of the form ∀τϑ where ϑ is quantifier-free and τ a finite set of predicates. From Σ ⊨ ϕ we have Σ ⊨ ϑ. By the compactness, there exists a finite subset Σ0 of Σ such that Σ0 ⊨ ϑ, which implies Σ0 ⊨ ϕ. On the other hand, by the assumption, it is clearly true that ϕ ⊨ Σ0. Let ψ be the conjunction of all formulae in Σ0. Then ψ is a first-order formula equivalent to ϕ.

Remark 1. By the above proposition, the three kinds of firstorder expressibility then coincide for both circumscription and the general stable model semantics (so also for disjunctive logic programming) since their syntax-translation definitions are universal second-order. In the rest of this paper, we will only consider the standard first-order expressibility.

4 Progression and Boundedness

Firstly, we generalize the fixed point semantics in [Lobo et al., 1992] to non-Herbrand disjunctive logic programs with default negation, and show the new semantics coinciding with the general stable model semantics.

In order to simplify the presentation, each clause and clauses obtained from it by applying the laws of commutation, association and identity for ∨ are regarded as the same.

Definition 2. Given a propositional, possibly infinite and plain disjunctive logic program Π, and given a subset Σ of PC(υ(Π)), let ΓΠ(Σ) be the set of all clauses H∨C1∨· · ·∨Ck such that k ≥ 0 and there are a rule p1 ∧ · · · ∧ pk → H in Π and a sequence of positive clauses C1 ∨p1, . . . , Ck ∨pk in Σ.

From the definition, ΓΠ is clearly a function on the subsets of PC(υ(Π)). Now by the first-order GL-reduction, a progressional operator for first-order logic programs is then defined.

Definition 3. Let Π be a disjunctive logic program and let A be a structure of υ(Π). We define ΓAΠ as the function ΓΠA.

Assume Γ is a unary function on a set. For convenience, we let Γ ↑ 0 denote the empty set ∅, and let Γ ↑ n be the union of Γ ↑ n-1 and Γ(Γ ↑ n-1) for all integers n > 0. Moreover, we define Γ ↑ ω as the union of Γ ↑ n for all integers n ≥ 0.

Example 1. Let Π be the logic program consisting of rules

and let A be a {c}-structure. Then ΓAΠ ↑ 1 = {Pa} where a = cA , and for 1 < k ≤ |A|, ΓAΠ ↑ k is the set of all clauses of the form Pa1 ∨ · · · ∨Pak such that a1, . . . , ak ∈ A. □

Given a propositional theory Σ, let Λ(Σ) denote the set of clauses {γ ∈ PC(υ(Σ)) : Σ ⊨ γ}. The following proposition can be regarded as a simulation of Theorem 3.14 in [Lobo et al., 1992] which asserts the soundness and completeness of their fixed point semantics over Herbrand structures.

Proposition 6. Let Π be a propositional, possibly infinite and plain disjunctive logic program. Then ΓΠ ↑ ω ≡ Λ(Π).

This proposition can be proved in a way similar to Theorem 3.14 in [Lobo et al., 1992]. The only thing should be careful is: logic programs in this paper may involve an uncountable number of proposition constants. But it is not a real obstacle since many properties of the propositional logic, including the completeness and compactness, still hold for the uncountable language (see Section 1.2 of [Chang and Keisler, 1990]).

The above proposition implies that our semantics is indeed a generalization of the fixed point semantics in [Lobo et al., 1992]. To achieve our goal, however, more results are needed.

Proposition 7. Let Π be a propositional, possibly infinite and plain disjunctive logic program without extensional propositions. Then Π and Λ(Π) have the same set of minimal models.

Proof. "Subset": Suppose M is a minimal model of Π. As M is clearly a model of Π, by the definition of Λ, M should satisfy each clause in Λ(Π). To obtain a contradiction, we assume M is not a minimal model of Λ(Π). This means that there must be a model N of Λ(Π) such that N ⊊ M. Let Σ be the set {¬C : C ∈ PC(υ(Π)) ∧ N |= ¬C}. We claim that Π∪Σ is satisfiable. Let us first assume the claim is true. Let N′ be a model of Π∪Σ. For every clause C ∈ PC(υ(Π)), it is clear that, if N satisfies ¬C, then ¬C ∈ Σ, which implies N′ satisfies ¬C too. By Proposition 2, it implies N′ ⊆ N ⊊ M. But this is impossible since M is a minimal model of Π.

Now we prove the claim. To obtain a contradiction, assume that Π∪Σ is unsatisfiable. By the compactness, there is then a finite subset Σ0 of Σ such that Π∪Σ0 is unsatisfiable. Suppose Σ0 = {¬C1, . . . , ¬Ck} for some integer k. It must hold that Π ⊨ C1∨· · ·∨Ck. Let C0 = C1∨· · ·∨Ck. It is obvious that C0 ∈ PC(υ(Π)). By the definition of Λ and the previous conclusion, we then have that C0 ∈ Λ(Π). Since N is a model of Λ(Π), C0 should be satisfied by N. Consequently, there should be an integer 1 ≤ i ≤ k such that N satisfies Ci, which leads to a contradiction since Ci ∈ Σ.

"Superset": Suppose M is a minimal model of Λ(Π). Let N be any proper subset of M. By the assumption, N does not satisfy Λ(Π). By the definition of Λ, we can then conclude that N does not satisfy Π too. Therefore, it remains to show that M is a model of Π. Let Σ = {¬C : C ∈ PC(υ(Π)) ∧ M |= ¬C}. By a similar argument using in the proof of the above claim, we can show that Π ∪ Σ is satisfiable. Let N′ be a model of Π ∪ Σ. For every clause C ∈ PC(υ(Π)), if M |= ¬C, we have C ∈ Σ by the definition, which implies that N′ satisfies ¬C. By Proposition 2, we can then conclude N′ ⊆ M. As we just proved, any proper subset of M is not a model of Π. So, it must be true that N′ = M, which implies that M is a model of Π. This then completes the proof.

Now we show that the stable model semantics for disjunctive logic programs has a progression characterization.

Theorem 1. Let Π be a disjunctive logic program and let τ be the set of all intensional predicates of Π. Let A be an arbitrary structure of υ(Π). Then A is a stable model of Π if and only if INS(A, τ) is a minimal model of ΓAΠ ↑ ω.

Proof. Simply by the equivalence of following statements:

1. A is a stable model of Π;
2. INS(A, τ) is a minimal model of ΠA ;
3. INS(A, τ) is a minimal model of Λ(ΠA);
4. INS(A, τ) is a minimal model of ΓΠA ↑ ω;
5. INS(A, τ) is a minimal model of ΓAΠ ↑ ω.

Herein, the equivalence of statements 1 and 2 is immediate by Proposition 4; 2 and 3 by Proposition 7; 3 and 4 by Proposition 6; and 4 and 5 by the definition.

Next, we show that the progression can be defined in a firstorder way. This will play an important role in the proof of our main result. Some definitions and notations are given firstly.

Every individual variable that will be used in logic programs is supposed to be among v0, v1, v2, . . . . For each variable vi, i is called its index. Let V be any set of individual variables. A renaming function of V is an injective mapping that maps each variable in V to an individual variable. Given a renaming function λ of V and an expression (including a term or a formula) ϖ, let λ(ϖ) be the expression obtained from ϖ by substituting λ(x) for all variables x in V .

In many cases, what variables are used in a logic program is not important, and different renaming functions may play the same role. Therefore, a method is then needed to make choices among such kinds of renaming functions. A natural way to do this is by arming with a linear order on renaming functions and then choosing the least one satisfying a certain condition. We define a linear order on renaming functions as follows. Let λ1 and λ2 be two renaming function of V . Given k = 1 or 2, let Sk be the sequence of all indices of λk(x) for all x ∈ V which is ordered by the index of x, i.e., if i < j and vi, vj ∈ V , then the position of index of λk(vi) in Sk should be in front of that of λk(vj). We say λ1 is less than λ2 iff the sequence S1 is less than S2 in the lexicographic order.

Definition 4. Let Π be a disjunctive logic program. We let ∆0 (Π) = ∅, and for each integer n > 0, let ∆n (Π) be the union of ∆n-1 (Π) and the set of all rules

that satisfy all the following conditions:

1. there is a rule γ = P1(¯ t1) ∧ · · · ∧ Pk(¯ tk) ∧ η → ϑ in Π such that no intensional predicate positively occurs in η,
2. for each integer 1 ≤ i ≤ k, there is a rule γi = ηi → ϑi ∨ Pi(¯ si) in ∆n-1 (Π), and
3. for each integer 1 ≤ i ≤ k, λi is the least renaming function of V such that no individual variable occurring in the formulae λ1(γ1), . . . , λi(γi) occurs in γ, and η∗ i is the formula λi(ηi) ∧ (λi(¯ si) = ¯ ti), where V is the set of all individual variables occurring in γ, γ1, . . . , γk.

Moreover, let ∆(Π) denote the union of ∆n (Π) for all n ≥ 0.

Example 2. (Example 1 continued) Let Π be the same as Example 1 and suppose x, y, z are v0, v1, v2 respectively. Then

and so on. Clearly, ∆n (Π) is a finite set for each n ≥ 0. □

Intuitively, ∆n (Π) is the set of formulae derivable in n steps by some rules. The following property is not surprise.

Proposition 8. Let Π be a disjunctive logic program. Let A be an υ(Π)-structure. Then ΓAΠ ↑n = ∆n (Π)A for all n ≥ 0.

The proof of this proposition is slightly tedious, but its intuitive meaning is very clear. Due to the limit of space, we omit the proof here. A complete proof through an induction on n will be available in the full version of this paper.

Now, we define the boundedness of a logic program.

Definition 5. Let Π be a plain disjunctive logic program and τ the set of all intensional predicates of Π. Let C be a class of τ -structures. Given an integer k ≥ 0, Π is k-bounded on C if for every structure A in C, ΓAΠ ↑ ω is equivalent to ΓAΠ ↑ k. Π is bounded on C if it is k-bounded on C for some integer k ≥ 0. If C is the class of all τ-structures and Π is bounded (k-bounded) on C, we simply say Π is bounded (k-bounded).

In this definition, please notice that ΓAΠ ↑ ω and ΓAΠ ↑ n are required to be equivalent. It seems more natural to define boundedness by the set-identity relation. But the following example shows that this is not enough to capture the firstorder expressibility of plain disjunctive logic programs.

Example 3. (Example 1 continued) Let Π be the program in Example 1. It is clear that CIRC(Π) is equivalent to the firstorder sentence ∀xP(x). Let A be any {c}-structure. Then ΓAΠ ↑ n is a proper subset of ΓAΠ ↑ ω for each integer n < |A|. On the other hand, ΓAΠ ↑ 2 is equivalent to ΓAΠ ↑ ω since the clause Pa ∈ ΓAΠ ↑ 2 for each a in A. Hence, Π is bounded.□

Definition 6. Let Π be a plain disjunctive logic program. Given an integer k ≥ 0, we say Π is k-finitary with respect to derivation if ∆(Π) is equivalent to ∆k (Π). We say Π is finitary with respect to derivation if it is k-finitary with respect to derivation for some integer k ≥ 0.

The following theorem follows from Proposition 8.

Theorem 2. A plain disjunctive logic program is k-bounded if and only if it is k-finitary with respect to derivation.

Now, let us consider non-plain disjunctive logic programs. Let Π be such a program and let τ be the set of all intensional predicates of Π. Lin's transformation translates Π to a plain disjunctive logic program Π∗ which is obtained from Π by, for each P of τ, substituting P ∗ for all positive occurrences of P in the head or the body of rules [Lin, 1991]. By the second-order translation, it is easy to see that SM(Π) is equivalent to ∃τ ∗ (CIRC(Π∗ ) ∧ τ ∗ = τ). So, a natural definition of boundedness for non-plain programs can be defined by this transformation. Unfortunately, the following example shows that it does not capture the first-order expressibility.

Example 4. Let Π be the following logic program:

It is easy to verify that SM(Π) is equivalent to the first-order sentence ∀xy(E(x, y) ∧ P (x, y) ∧ R(x, y)). Let n > 0 be an integer, and let An be a structure encoding the linear order of length n. Then n is the least integer k such that ΓAn Π∗ ↑ k is equivalent to ΓAn Π∗ ↑ ω, which implies Π∗ is unbounded. □

Therefore, we have to choose a weaker definition for the boundedness of non-plain disjunctive logic programs. By the next proposition, it can assure the first-order expressibility.

Definition 7. Let Π be a non-plain disjunctive logic program and let τ be the set of all intensional predicates of Π. Let S(Π) be the union of the class of stable models of Π and classes of stable models of ∆k (Π) for all integers k ≥ 1. We then say Π is bounded iff Π∗ is bounded on S(Π).

Proposition 9. Let Π be a bounded and plain (non-plain) disjunctive logic program. Then Π and ∆k (Π) have the same class of minimal (stable, respectively) models for some k ≥ 0.

Proof. We only consider the case that Π is a non-plain disjunctive logic program. For the plain case, a similar proof can be easily obtained. By the definition, there must be some integer k ≥ 0 such that Π∗ is k-bounded over S(Π). Now, it suffices to prove the equivalence of following statements:

1. A is a stable model of Π;
2. INS(A, τ) is a minimal model of ΓAΠ ↑ ω;
3. INS(A, τ) is a minimal model of ΓAΠ ↑ k;
4. INS(A, τ) is a minimal model of ∆k (Π)A ;
5. A is a stable model of ∆k (Π).

Herein, the equivalence of statements 1 and 2 follows from Theorem 1; 2 and 3 from the assumption that Π is k-bounded; 3 and 4 from Proposition 8; 4 and 5 from Proposition 4.

5 A Preservation Theorem

Let Π be a disjunctive logic program. The dependency graph of Π is the directed graph whose vertices are predicates in υ(Π) and that consists of all edges from P to Q such that P and Q positively occur in the head and the body of a rule in Π respectively. We say Π is recursion-free if every intensional predicate has no positive occurrence in the body of any rule in Π, and say Π is loop-free if its dependency graph is acyclic.

Now we give the statement of our main theorem. The rest of this section is then devoted to prove the main theorem.

Main Theorem. Let Π be a disjunctive logic program. If Π is plain, the following statements are then equivalent:

1. Π is bounded;
2. Π is finitary with respect to derivation;
3. There is a recursion-free disjunctive logic program Π0 such that SM(Π) ≡ SM(Π0);
4. There is a loop-free disjunctive logic program Π0 such that SM(Π) ≡ SM(Π0);
5. SM(Π) is first-order expressible;
6. SM(Π) is weak-first-order expressible;
7. SM(Π) is pseudo-first-order expressible.

Otherwise, the statements 5-7 are equivalent, and the statement 1 implies all statements among 3-7.

Before proving the theorem, we introduce a tool from classical model theory - the ultraproduct. Let I be a nonempty set and D a set of subsets of I. Then D is a filter over I if:

1. if both X and Y are in D then X ∩ Y is in D, and
2. if X is in D and X ⊆ Y ⊆ I then Y is also in D.

Moreover, D is an ultrafilter over I if D is a filter over I and for every subset X of I, X is in D iff I \ X is not in D.

Assume D is an ultrafilter over I. Let υ be a vocabulary, and let Ai(i ∈ I) be a family of υ-structures. Let ∏i∈I Ai be the set of all functions π with domain I such that π(i) ∈ Ai for all i ∈ I. For all π1, π2 ∈ ∏i∈I Ai, we write π1 ∼D π2 if the set {i ∈ I : π1(i) = π2(i)} is in D. It is clear that ∼D is an equivalence relation. If π ∈ ∏i∈I Ai then let πD be the equivalence class π with respect to ∼D. Let ∏DAi denote the set of equivalence classes πD for all π ∈ ∏i∈I Ai. The ultraproduct of Ai(i ∈ I) module D, written as ∏DAi, is defined to be the υ-structure satisfying the following conditions:

1. the domain of ∏DAi is ∏DAi;
2. for each k-ary predicate P in υ, P ∏D Ai consists of all the tuples (πD 1 , . . . , πD k ) such that πD 1 , . . . , πD k ∈ ∏DAi and {i ∈ I : (π1(i), . . . , πk(i)) ∈ P Ai } ∈ D;

1. for each k-ary function f in υ and for all πD 1 , . . . , πD k in ∏DAi, f ∏D Ai (πD 1 , . . . , πD k ) = πD where π is defined by π(i) = f Ai (π1(i), . . . , πk(i)) for all i ∈ I.

Let C be an arbitrary class of structures. We say C is closed under ultraproducts if ∏DAi is in C whenever D is an ultrafilter over some nonempty set I and Ai is in C for every index i in I. We say C is definable by a first-order sentence ϕ (a first-order theory Σ) if C is exactly the class of all models of ϕ (of Σ). The following proposition immediately follows from Theorem 4.1.12 in [Chang and Keisler, 1990].

Proposition 10. A class of structures is definable by a firstorder sentence if and only if it is definable by a first-order theory and its complement is closed under ultraproducts.

The following property, which says that every consistent universal first-order theory has a minimal model, is an immediate corollary of Property 1.3.2 in [Bossu and Siegel, 1985].

Proposition 11. Let Σ be a possibly infinite set of universal first-order sentences, and let A be a model of Σ. Then there is a minimal model B of Σ such that B ≼τ A.

For the notation ∆(·) defined in the previous section, the following property immediately follows from the definition.

Lemma 1. Let Π be a plain disjunctive logic program. Then for every rule γ in ∆(Π), Π entails γ in classical logic.

With these properties, we can then prove the following result, which plays a critical role in the proof of Main Theorem.

Proposition 12. Let Π be a plain disjunctive logic program. If CIRC(Π) is equivalent to a first-order sentence, then Π is finitary with respect to derivation.

Proof. We first prove the statement that there is a finite subset of ∆(Π) which is equivalent to a first-order sentence. To obtain a contradiction, we assume it is not true. By Proposition 10, there should be an index set I, an ultrafilter D over I and a family of structures Ai(i ∈ I) of υ(Π) such that Ai does not satisfy ∆(Π) for any index i ∈ I, but ∏DAi satisfies ∆(Π). Let τ be the set of all intensional predicates of Π. By Proposition 11, there must be a τ-minimal model B of ∆(Π) such that B ≼τ ∏DAi (∗). For each index i ∈ I, let Bi be a structure obtained from Ai by removing tuples (π1(i), . . . , πk(i)) from P Ai if k ≥ 0, P is a k-ary predicate in τ and the tuple (πD 1 , . . . , πD k ) is in P ∏D Ai but not in P B . Then it is clear that, for all indices i ∈ I, we have Bi ≼τ Ai. By Proposition 1, we conclude that, for each i ∈ I, Bi does not satisfy ∆(Π). According to Lemma 1, this implies that Bi does not satisfy Π. Consequently, B cannot be any model of CIRC(Π). According to the assumption, CIRC(Π) is equivalent to a firstorder sentence. So, by Proposition 10 again, ∏DBi is not a model of CIRC(Π) too. On the other hand, by the definition of ultraproduct, it is easy to check that ∏DBi = B, which contradicts with the conclusion (∗).

With this statement, there is then a first-order sentence ϕ that is equivalent to ∆(Π). And by the compactness, there must be a finite subset Φ of ∆(Π) such that Φ ⊨ φ, which immediately implies that Φ ≡ φ. Let n be the smallest integer such that Φ ⊆ ∆n (Π), then ∆n (Π) should be equivalent to ∆(Π). Hence, Π is finitary with respect to derivation.

Now we are in the position to prove Main Theorem.

Proof of Main Theorem. The equivalence of statements 57 immediately follows from Proposition 5 and Remark 1. The direction of "3=⇒4" is trivially true, "1=⇒3" follows from Proposition 9, "4=⇒5" follows from Theorem 11 of [Ferraris et al., 2011] and the fact that every loop-free program is tight. In particular, for the case that Π is plain, the equivalence of statements 1 and 2 is immediately obtained by Theorem 2, and the direction of "5=⇒2" is by Proposition 12.

Remark 2. For the non-plain programs, Main Theorem shows that the boundedness is a sufficient condition for the firstorder expressibility. However, it is not clear whether or not it is also a necessary condition. The main difficulty of generalizing our preservation theorem to non-plain case is: it seems hard to find a replacement for Proposition 11. Therefore, it is a challenge to find a boundedness-like characterization for the first-order expressibility of non-plain logic programs.

Remark 3. Over finite structures, the boundedness of plain logic programs is not enough to capture the standard firstorder expressibility. A counterexample, which does not involve any default negations and disjunctions, could be found in the proof of Theorem 11.1 in [Ajtai and Gurevich, 1994].

6 RelatedWorks and Conclusion

The boundedness characterization of the first-order expressibility for function-free definite logic programs was independently discovered by [Kolaitis and Papadimitriou, 1990] and [Ajtai and Gurevich, 1994]. Our preservation theorem extends theirs in two directions: allowing disjunctions in the head of rules, and allowing functions in terms. It seems that their approaches cannot be applied to either extension.

Minker et al. developed a fixed point semantics for plain disjunctive logic programs over Herbrand structures [1990; 1992]; Zhang and Zhou proposed a progression semantics for normal logic programs [2010], and proved their boundedness defined on this semantics is a necessary condition for the firstorder expressibility. Both works are limited to certain classes of logic programs and even a certain class of structures. Our semantics is in fact a natural generalization of both.

There are two kinds of progression semantics which were proposed for disjunctive logic programs with default negation [Leone et al., 1997; Zhou and Zhang, 2011]. The first is based on a technique of unfounded sets and works on Herbrand structures, and the second progresses disjunctive logic programs in a parallel way. Both semantics are significantly different from ours. It is not clear whether or not their semantics can be used to capture the first-order expressibility.

The preservation theorem presented in this paper is an interesting model-theoretic property for disjunctive logic programs, and gives us a precise picture on the relationship between disjunctive logic programs and classical logic. It also provides us a manageable condition for identifying first-order expressible fragments. Moreover, the progression semantics and boundedness proposed here may shed light on the static analysis and optimization of disjunctive logic programs.

Acknowledgement

This publication was made possible by the support of an NPRP grant (NPRP 09-079-1-013) from the Qatar National Research Fund (QNRF). The statements made herein are solely the responsibility of the authors.