First-Order Extension of the FLP Stable Model Semantics via Modified Circumscription

1 Introduction

The stable model semantics is the mathematical basis of answer set programming, and is one of the most well-studied knowledge representation formalisms. Lifschitz [2010] surveys thirteen different definitions of a stable model presented in the literature. These definitions are equivalent to each other when they are applied to normal logic programs, but are not necessarily so for more general classes of programs. However, each of them deserves its own attention, as it provides useful insights into the stable model semantics and answer set programming.

The semantics defined by Faber, Leone and Pfeifer [2004; 2011] (called the FLP semantics) deserves special attention as it provides a simple satisfactory solution to the semantics of aggregates, and is implemented in the system DLV (http://www.dlvsystem.com). It is also a basis of HEX programs, which are an extension of answer set programs towards integration of external sources of information that have possibly heterogeneous semantics [Eiter et al., 2005]. Also, Dao-Tran et al. [2009] remark that the FLP semantics provides a more natural basis for their Modular Logic Programs (MLP) than the traditional Gelfond-Lifschitz semantics [Gelfond and Lifschitz, 1988].

The idea of the FLP semantics is based on an interesting modification to the traditional definition of a reduct by Gelfond and Lifschitz [1988]. The FLP-reduct of a program Π

relative to a set X of atoms is obtained from Π by simply removing all rules whose bodies are not satisfied by X. After then the same minimality condition as in the original definition of an answer set applies. For example, consider the following program Π1:

The FLP-reduct of Π1 relative to X = {p, r} is

and X is minimal among the sets of atoms that satisfy (2), and hence is an answer set of Π1. Theorem 3.6 from [Faber et al., 2011] asserts that this definition of an answer set is equivalent to the traditional definition when it is applied to the syntax of usual disjunctive programs. Indeed, the GL-reduct of Π1 relative to X [Gelfond and Lifschitz, 1988] is

and, again, {p, r} is minimal among the sets of atoms that satisfy (3).

The FLP semantics was recently extended to arbitrary propositional formulas by Truszczy´nski [2010], based on the definition of a reduct that is similar to the one proposed by Ferraris [2005]. However, his extension is still limited as it allows neither variables nor aggregates.

In this paper, we extend the FLP semantics and its extension by Truszczy´nski, both syntactically and semantically. We consider the syntax of arbitrary first-order formulas allowing aggregates. Instead of referring to grounding and fixpoints, our generalized semantics are given in terms of modifications to circumscription [McCarthy, 1980], in the same spirit as the first-order stable model semantics by Ferraris, Lee and Lifschitz [Ferraris et al., 2007; 2011]. Such uniform characterizations in the form of modified circumscription tell us how the FLP semantics and its extension by Truszczy´nski are related to circumscription and to the first-order stable model semantics.

In Section 2 we review the original FLP semantics, and present our generalization. Likewise, in Section 3 we review and generalize the extension of the FLP semantics by Truszczy´nski. In Section 4 we compare these generalizations with the first-order stable model semantics.

2 FLP Semantics

2.1 Review: Original FLP Semantics

A disjunctive rule is an expression of the form

A1 ; . . . ; Al ← Al+1, . . . ,Am, not Am+1, . . . , not An (4) (n ≥ m ≥ l ≥ 0) where each Ai is an atomic formula (possibly containing equality and 0-place connectives ⊤ and ⊥). A disjunctive program is a set of disjunctive rules. The FLP semantics for a disjunctive program in [Faber et al., 2011] is given in terms of grounding and fixpoints. By σ(Π) we denote the signature consisting of the object, function and predicate constants occurring in Π. We denote by Ground(Π) the ground instance of Π, that is, the program obtained from Π by replacing every occurrence of object variables with every ground term that can be constructed from σ(Π), and then replacing equality t = t′ with ⊤ or ⊥ depending on whether term t is the same symbol as term t′ . Given a set X of ground atoms of σ(Π), the reduct of Π relative to X, denoted by ΠX , is obtained from Ground(Π) by removing every rule whose body is not satisfied by X. Set X is called an FLP-answer set of Π if X is minimal among the sets of atoms that satisfy ΠX (viewed as a formula in propositional logic). For example, for Π1 and X = {p, r} in the introduction, ΠX1 is (2) and X is an FLP-answer set of Π1.

2.2 Extension: First-Order FLP Semantics

We present a reformulation of the FLP semantics in the firstorder case. First, we consider a program that does not contain aggregates, but allows rules of a more general form than (4). We assume the following set of primitive propositional connectives and quantifiers in forming formulas:

¬F is an abbreviation for F → ⊥, symbol ⊤ stands for ⊥ → ⊥, and F ↔ G stands for (F → G) ∧ (G → F ).

A (general) rule is of the form

where H and B are arbitrary formulas in first-order logic. Rule (4) is a special case of rule (5) when we identify not with ¬, the head H with the disjunction of atomic formulas and the body B with the conjunction of atomic formulas, possibly preceded by negation. A (general) program is a set of (general) rules.

Let p be a list of distinct predicate constants p1, . . . , pn, and let u be a list of distinct predicate variables u1, . . . , un. By u ≤ p we denote the conjunction of the formulas ∀x(ui(x) → pi(x)) for all i = 1, . . . , n where x is a list of distinct object variables of the same length as the arity of pi, and by u < p we denote (u ≤ p) ∧ ¬(p ≤ u). For instance, if p and q are unary predicate constants then (u, v) < (p, q) is

For any formula G and any list p of predicate constants, formula G(u) is obtained from G by replacing all occurrences of predicates from p with the corresponding predicate variables from u.

Let Π be a finite program whose rules have the form (5). The FOL-representation ΠFOL of Π is the conjunction of the universal closures of B → H for all rules (5) in Π. By FLP[Π; p] we denote the second-order formula

where Π△(u) is defined as the conjunction of

for all rules (5) in Π, where x is the list of all (free) variables in (5).

We will often simply write FLP[Π] instead of FLP[Π; p] when p is the list of all predicate constants occurring in Π, and call a model of FLP[Π] an FLP-stable model of Π.

Example 1 Consider the programΠ1 in the introduction. Its FOL-representation ΠFOL 1 is

and Π△1 (u, v,w) is

Formula

can be equivalently rewritten without second-order variables as ¬(p ↔ q) ∧ (r ↔ p ∨ q).

Though rule arrows (←) are treated like usual implications in the FOL-representation of Π, they are distinguished in the definition of Π△(u) because of the presence of 'B∧' in (7). If we modify Π△(u) by dropping 'B∧' from (7), then (6) becomes exactly CIRC[ΠFOL; p] [McCarthy, 1980]. Interestingly, this small change accounts for the differences in the two semantics, one leading to stable models and the other leading to minimal models. For instance, classically equivalent transformations preserve minimal models, but not FLPstable models. Each of the one-rule programs {p ← ¬q}, {q ← ¬p}, and {p ∨ q ← ⊤} are classically equivalent to each other (when we identify them with their FOLrepresentations), but their FLP-stable models are different. Formula FLP[p ← ¬q; p, q] is equivalent to p ∧ ¬q; formula FLP[q ← ¬p; p, q] is equivalent to q ∧ ¬p; formula FLP[p ∨ q ← ⊤; p, q] is equivalent to (p ∨ q) ∨ ¬(p ∧ q), which is also equivalent to CIRC[p ∨ q; p, q].

The following theorem states that our semantics is a proper generalization of the semantics from [Faber et al., 2011].

Theorem 1 Let Π be a finite disjunctive program (consisting of rules of the form (4)) containing at least one object constant. The FLP-answer sets of Π are precisely the Herbrand models of FLP[Π] whose signature is σ(Π).

It is known that the FLP semantics from [Faber et al., 2011] has the anti-chain property: no FLP-answer set is a proper subset of another FLP-answer set. This property is still preserved in our generalized semantics.

Proposition 1 For any finite general program Π, if I is an Herbrand interpretation of σ(Π) that satisfies FLP[Π], then I is a subset-minimal model of Π. 1

1 We identify an Herbrand interpretation I with the set of ground atoms that are satisfied by I.

Clearly, circumscription can be viewed as a special case of the FLP semantics as in the following.

Proposition 2 For any first-order sentence F and any list p of predicate constants, CIRC[F; p] is equivalent to FLP[F ←⊤; p].

The FLP semantics can be represented by circumscription in the following way.

Proposition 3 For any finite general program Π, formula FLP[Π; p] is equivalent to ∃u(CIRC[Π△(u); u] ∧ (u = p)).

2.3 Extension: First-Order FLP Semantics for Programs with Aggregates

The semantics presented in the previous section can be extended to allow aggregates by simply extending the notion of satisfaction to cover aggregate expressions. Below we adopt the definitions of an aggregate formula and satisfaction as given in [Lee and Meng, 2009; Ferraris and Lifschitz, 2010].

Following [Ferraris and Lifschitz, 2010], by a number we understand an element of some fixed set Num. For example, Num is Z ∪ {+∞, -∞}, where Z is the set of integers. An aggregate function is a partial function from the class of multisets to Num. The domain of an aggregate function is defined as usual. For instance, COUNT is defined for any multisets; SUM, TIMES, MIN and MAX are defined for multisets of numbers; SUM is undefined for multisets containing infinitely many positive integers and infinitely many negative integers.

We assume that the signature σ contains symbols for all numbers, and some collection of comparison operators that stands for binary relations over numbers, such as ≤, ≥, <, >, = and ̸=. We assume that symbols for aggregate functions are not part of the signature.

An aggregate expression of signature σ is of the form 2

where

• OP is an aggregate function;
• x is a nonempty list of distinct object variables;
• F(x) is a first-order formula;
• ⪰ is a comparison operator;
• b is a term (as in first-order logic).

We define an aggregate formula as an extension of a firstorder formula by including aggregate expressions as a base case like (standard) atomic formulas (including equality and ⊥). In other words, aggregate formulas are constructed from atomic formulas and aggregate expressions using connectives and quantifiers as in first-order logic. For instance,

is an aggregate formula.

We say that an occurrence of a variable v in an aggregate formula H is bound if the occurrence is in a part of H of the form 〈x : F(x)〉 where v is in x, or in a part of H of the form QvG. Otherwise it is free. We say that v is free in H if H contains a free occurrence of v. An aggregate sentence is an aggregate formula with no free variables.

2 The syntax of an aggregate expression considered in Ferraris and Lifschitz [2010] is more general. The results in this paper can be extended to the general syntax, which we omit for simplicity.

The definition of an interpretation is the same as in firstorder logic. We consider only the interpretations such that each number and each comparison operator is interpreted as itself. Consider an interpretation I of a first-order signature σ that may contain any function constants of positive arity. By σ|I| we mean the signature obtained from σ by adding distinct new object constants ξ ∗ , called names, for all ξ in the universe of I. We identify an interpretation I of σ with its extension to σ|I| defined by I(ξ ∗ ) = ξ.

The definition of satisfaction in first-order logic is extended to aggregate sentences as follows. Let I be an interpretation of signature σ. Consider any aggregate expression (8) that has no free variables. Let SI be the multiset consisting of all ξ∗ [1] (i.e. the first element of ξ∗ ), in the universe of I where

• ξ∗ is a list of object names of σ|I| whose length is the same as the length of x, and
• I satisfies F(ξ∗ ).

An interpretation I satisfies the aggregate expression if SI is in the domain of OP, and OP(SI) ⪰ bI . With this extension, the recursive definition of satisfaction for an aggregate sentence is given in the same way as in first-order logic. We say that an aggregate sentence F is logically valid if every interpretation satisfies it. For instance, an Herbrand interpretation {p(a)} satisfies COUNT〈x : p(x)〉 > 0 but does not satisfy SUM〈x : p(x)〉 > 0 because multiset {{a}} is not in the domain of SUM. Consider the aggregate expression

and an Herbrand interpretation I = {p(-1), p(1)}. SI is {{-1, 1}} and SUM(SI) = 0 ≥ 0, so I satisfies SUM〈x : p(x)〉 ≥ 0.

Once we extend the definition of satisfaction to aggregate sentences, we can simply extend the FLP semantics in Section 2.2 to a general program with aggregates, whose rules have the form

where H and B are aggregate formulas. The AFrepresentation ("Aggregate Formula representation") of a finite general program Π with aggregates is the conjunction of the universal closures of the aggregate formulas B → H for all rules (9) in Π. Formula FLP[Π; p] is defined the same as (6) except that Π is now understood as a general program with aggregates.

Example 2 Consider the following general program Π with aggregates:

The AF-representation of Π, denoted by ΠAF , is the following:

The FLP-stable models of (10) are the models of

where Π△(u) is

Below we show how this semantics is related to the original semantics by Faber et al. [2011]. Their semantics is defined for a special class called disjunctive programs with aggregates, whose rules have the form

(l ≥ 0; n ≥ m ≥ 0), where each Ai is an atomic formula and each Ei is an atomic formula or an aggregate expression.

As before, the original FLP semantics is defined in terms of grounding and fixpoints. Let us assume that b in every aggregate expression (8) is a constant. We extend the notion Ground(Π) to a disjunctive program Π with aggregates by replacing every free occurrence of a variable with every ground term that can be constructed from σ(Π) in all possible ways.

For any disjunctive program Π with aggregates and any Herbrand interpretation X whose signature is σ(Π), the FLPreduct of Π relative to X is obtained from Ground(Π) by removing every rule whose body is not satisfied by X. Set X is an FLP-answer set of Π if it is minimal among the sets of atoms that satisfy the FLP-reduct of Π relative to X [Faber et al., 2011]. For example, in program (10) above, the FLPreduct of (10) relative to {p(-1), p(1)} contains the last two rules only. Set {p(-1), p(1)} is minimal among the sets of atoms that satisfy the reduct, and thus is an FLP-answer set of (10). In fact, this is the only FLP-answer set. Also one can check that {p(-1), p(1)} is the only Herbrand model of σ(Π) that satisfies (12) in Example 2.

Theorem 2 Let Π be a finite disjunctive program with aggregates that contains at least one object constant. The FLP-answer sets of Π are precisely the Herbrand models of FLP[Π] whose signature is σ(Π).

3 Truszczy´nski Semantics

3.1 Review: Original Truszczy´nski Semantics

Truszczy´nski [2010] defined an extension of the FLP semantics to arbitrary propositional formulas, similar to the extension of the stable model semantics to arbitrary propositional formulas by Ferraris [2005], whose idea is also related to [Pearce, 1997; Osorio et al., 2004].

For any propositional formula F , the FLPT-reduct F X relative to a set X of atoms is defined recursively:

• ⊥X = ⊥;

Set X is an FLPT-answer set of F if X is minimal among the sets of atoms that satisfy F X .

3.2 Extension: FLPT Semantics for First-Order Formulas with Aggregates

We extend the FLPT semantics to arbitrary first-order formulas that allow aggregates.

For any first-order formula F with aggregates and any finite list of predicate constants p = (p1, . . . , pn), formula FLPT[F; p] is defined as

where F □(u) is defined recursively, as follows:

• pi(t)□ = ui(t) for any tuple t of terms;
• F □ = F for any atomic formula F that does not contain members of p;

Similar to FLP[Π], we will often simply write FLPT[F] instead of FLPT[F ; p] when p is the list of all predicate constants occurring in F , and call a model of FLPT[F ] an FLPTstable model of F .

The following theorem states that our semantics is a proper extension of the Truszczy´nski semantics to first-order formulas with aggregates. For any formula F, by σ(F) we denote the signature consisting of object, function and predicate constants occurring in F .

Theorem 3 For any propositional formula F, the FLPTanswer sets of F are precisely the interpretations of σ(F) that satisfy FLPT[F].

Also the semantics above coincides with our extension of the FLP semantics in Section 2.3 when it is applied to disjunctive programs with aggregates (having rules of the form (14)).

Proposition 4 For any finite disjunctive program Π with aggregates and the AF-representation F of Π, FLP[Π; p] is equivalent to FLPT[F ; p].

However, the statement of the proposition does not apply to general programs.

Example 3 For general program Π = {p∨¬p ← ⊤} and its FOL-representation F, formula FLP[Π] has only one model, ∅, and FLPT[F ] has two models, ∅ and {p}.

In comparison with Proposition 1, this example illustrates that, unlike the FLP semantics, the FLPT semantics does not keep the anti-chain property. This has to do with the fact the FLP semantics distinguishes between rule arrows and the other implications, while the FLPT semantics does not. The first-order stable model semantics from [Ferraris et al., 2011] also lacks the anti-chain property. In fact, the FLPT semantics has similar properties with that semantics. For instance, the following theorem is similar to Theorem 2 from [Ferraris et al., 2011]. By Choice(p) where p is a list of predicate constants, we denote the conjunction of "choice formulas" ∀x(p(x) ∨ ¬p(x)) for all predicate constants p in p where x is a list of distinct object variables whose length is the same as the arity of p.

Theorem 4 For any first-order formula F with aggregates and any disjoint lists p, q of distinct predicate constants, the following formulas are logically valid:

For example, FLPT[∀x(q(x) → p(x) ∨¬p(x)); p] is equivalent to

The following theorem is similar to Theorem 3 from [Ferraris et al., 2011].

Theorem 5 For any first-order formulas F and G with aggregates and any list of predicate constants p, FLPT[F ∧¬G; p] is equivalent to FLPT[F; p] ∧¬G.

It follows that the FLPT-stable models of F ∧ ¬G can be characterized as the FLPT-stable models of F that satisfy ¬G.

The notion of strong equivalence has turned out to be important in the theory of stable models. Similar to the characterization of strong equivalence in terms of HT-models [Lifschitz et al., 2001; Ferraris et al., 2011], Truszczy´nski [2010] defined "FLP-models," a counterpart of HT-models in the FLPT semantics, and used them to characterize strong equivalence between propositional formulas under the FLPT semantics. In the following, we extend the result to arbitrary first-order formulas with aggregates. 3

Following the definition of strong equivalence in the firstorder stable model semantics in [Ferraris et al., 2011], about first-order formulas with aggregates F and G, we say that F is FLPT-strongly equivalent to G if, for any formula H with aggregates, any occurrence of F in H, and any list p of distinct predicate constants, FLPT[H; p] is equivalent to FLPT[H′ ; p], where H′ is obtained from H by replacing the occurrence of F by G. The following theorem, which is similar to Theorem 9 from [Ferraris et al., 2011], is a proper extension of Theorem 7 from [Truszczy´nski, 2010].

Theorem 6 Let F and G be first-order formulas with aggregates, let pFG be the list of all predicate constants occurring in F or G and let u be a list of distinct predicate variables. The following conditions are equivalent to each other.

• F and G are FLPT-strongly equivalent to each other;
• Formula

is logically valid.

3 Due to lack of space, we do not present the extension of FLP models, but instead present an alternative characterization in terms of F □.

As a special case, Theorem 6 can be applied to checking strong equivalence under the FLP semantics between the programs whose rules have the form (14).

4 Comparing FLP, FLPT and the First-Order Stable Model Semantics

In [Ferraris et al., 2011] the stable models are defined in terms of the SM operator with intensional predicates: for any first-order sentence F and any list of intensional predicates p = (p1, . . . , pn), formula SM[F ; p] is defined as

where F ∗ (u) is defined recursively:

• pi(t)∗ = ui(t) for any list t of terms;
• F ∗ = F for any atomic formula F that does not contain members of p;
• (G⊙H)∗ = G∗ ⊙ H∗ , where ⊙ ∈ {∧, ∨};
• (G→H)∗ = (G∗ → H∗ ) ∧ (G → H);
• (QxG)∗ = QxG∗ , where Q ∈ {∀, ∃};

We often simply write SM[F] in place of SM[F; p] when p is the list of all predicate constants occurring in F , and call a model of SM[F ] simply a stable model of F .

Disregarding aggregate expressions, the main difference among the FLP, the FLPT, and the first-order stable model semantics has to do with the treatment of an implication. It is known that they coincide for programs whose rules have the form (4) [Faber et al., 2011, Theorem 3.6], [Truszczy´nski, 2010, Theorem 3]. However, this is not the case for more general classes of programs (having rules of the form (5)), or for arbitrary formulas. In fact, no one is stronger than another, as the following example shows.

Example 4 For propositional signature {p} and program Π1 = {p ← p ∨¬p}, whose FOL-representation is F1 = p ∨¬p → p, each of FLP[Π1] and FLPT[F1] has {p} as the only model, and SM[F1] has no models.

Formula F1 is strongly equivalent (in the sense of [Ferraris et al., 2011]), but not FLPT-strongly equivalent to F2 = (p → p) ∧ (¬p → p). Again, SM[F2] has no models. Neither does FLP[Π2] nor FLPT[F2], where Π2 is the program corresponding to F2.

For program Π3 = {p ∨¬p ←⊤}, whose FOLrepresentation is F3 = ⊤→ p ∨¬p, both SM[F3] and FLPT[F3] have two models, ∅ and {p}, while FLP[Π3] has only one model, ∅.

Formula F3 is strongly equivalent, but not FLPT-strongly equivalent to F4 = ¬¬p → p. Both FLP[Π4] (Π4 is the program corresponding to F4) and FLPT[F4] have only one model, ∅, while SM[F4] has the same two models as SM[F3].

For program Π5 = {¬¬p ← ⊤, p ∨ ¬p ← ¬¬p}, and its FOL-representation F5, both FLP[Π5] and SM[F5] have only one model {p}, while FLPT[F5] has no models.

We note that FLPT-strong equivalence involves some unintuitive cases. Formulas F ∧G and F ∧ (F → G) are strongly equivalent under the first-order stable model semantics, but this is not the case under the FLPT semantics. The two formulas may not even have the same FLPT-stable models.

Example 5 Similar to program Π5 in the previous example, for propositional signature {p} and F = ¬¬p and G = p ∨¬p, formulas SM[F ∧ G] and FLPT[F ∧ G] are equivalent to each other, having only one model, {p}. Formula SM[F ∧ (F → G)] has the same model as SM[F ∧ G], but FLPT[F ∧ (F → G)] has no models.

We now show the relationships among the three semantics. Roughly speaking, the FLPT semantics is in between the two others in the sense that it treats a "non-strictly positive" occurrence of a subformula same as in the FLP semantics, and treats a "strictly positive" occurrence of a subformula the same way as in the first-order stable model semantics. The definition of a strictly positive occurrence is given below.

First we present a class of programs for which the FLP semantics and the FLPT semantics coincide. Following [Ferraris and Lifschitz, 2010], we say that an aggregate function OP is monotone w.r.t. ⪰ if for any multisets α, β such that α ⊆ β,

• if OP(α) is defined then so is OP(β), and
• for any n ∈ Num, if OP(α) ⪰ n then OP(β) ⪰ n.

For an occurrence of a predicate constant or any other subexpression in a formula F with aggregates, we consider two numbers, k and m.

• k: the number of implications in F that contain that occurrence in the antecedent;
• m: the number of aggregate expressions (8) containing that occurrence such that OP is not monotone w.r.t. ⪰.

We call an occurrence of a subexpression in F strictly positive if k +m for that occurrence in F is 0. For example, in formula (p → q) → p, the second occurrence of p is strictly positive. In ¬(SUM〈x : p(x)〉 < 2), the occurrence of p is not strictly positive (for that occurrence, k = m = 1).

The following theorem presents a class of programs for which the FLP semantics and the FLPT semantics coincide.

Theorem 7 Let Π be a finite general program with aggregates, and let F be the AF-representation of Π. For every rule (9) in Π, if every occurrence of p from p in H is strictly positive in H, then FLP[Π; p] is equivalent to FLPT[F; p].

The theorem is a generalization of Proposition 4. For example, the FLP and the FLPT semantics coincide on the programs whose heads have the form of a disjunction of atoms, regardless of the form of the formulas in the body. In Example 4, programs Π1, Π2 and Π4 satisfy the condition of Theorem 7, and so does program (10).

Next we show the class of programs for which the FLP semantics and the stable model semantics coincide. We first define two notions. We call an aggregate formula semi-positive relative to p if, for every aggregate expression OP〈x : G〉 ⪰ b in it, every occurrence of every predicate p from p is strictly positive in G. We say that an aggregate formula F is canonical relative to a list p of predicate constants if

• F is semi-positive relative to p;
• for every occurrence of every predicate constant p from p in F , we have that k + m ≤ 1;
• if a predicate constant p from p occurs in the scope of a strictly positive occurrence of ∃ or ∨ in F, then the occurrence of p is strictly positive in F .

For any canonical aggregate formula, the following result holds.

Proposition 5 For any aggregate formula F, if F is canonical relative to p, then formula

is logically valid.

From Proposition 5, when F is a first-order formula, it is easy to see that CIRC[F; p] and SM[F; p] are equivalent to each other. This fact is used in [Kim et al., 2009; Lee and Palla, 2010] to compute circumscriptive action formalisms using ASP solvers. Here we generalize the result to formulas containing aggregates and use it to relate the FLP and the FLPT operators to the SM operator.

Theorem 8 Let Π be a finite general program with aggregates and let F be the AF-representation of Π. For every rule (9) in Π, if B is canonical relative to p and every occurrence of p from p in H is strictly positive in H, then FLP[Π; p] is equivalent to SM[F; p].

Among the programs in Example 4, only Π2 satisfies the condition of Theorem 8. Program (10) does not satisfy the condition because ¬(SUM〈x : p(x)〉 < 2) is not canonical relative to {p}. In fact, {p(-1), p(1), p(2)} is an Herbrand interpretation that satisfies SM[(11)], but does not satisfy FLP[(10)].

Next we show the class of formulas F for which FLPT[F ; p] coincides with SM[F ; p].

Theorem 9 Let F be a semi-positive aggregate formula relative to p such that every subformula that has a non-strictly positive occurrence in F is canonical relative to p. Then FLPT[F; p] is equivalent to SM[F; p].

In Example 4, relative to {p}, formulas F2 and F3 satisfy the condition of Theorem 9. In Example 5, relative to {p}, formula F ∧ G satisfy the condition, but F ∧ (F → G) does not. Also formula (11) does not satisfy the condition. Again, {p(-1), p(1), p(2)} is an Herbrand interpretation that satisfies SM[(11)], but it does not satisfy FLPT[(11)].

5 Conclusion

Our work lifts up the mathematical foundations of the FLP and the FLPT semantics to the first-order level; our semantics are applicable to non-Herbrand models allowing arithmetic and arbitrary functions. The fact that these semantics are uniformly characterized in terms of modifications to circumscription provides us useful insights into the relationships among the FLP semantics, the FLPT semantics, circumscription and the first-order stable model semantics. We present the classes of formulas under which the semantics are interchangeable, which would have interesting ramifications. For instance, the FLP semantics is simpler than the first-order stable model semantics, but involves unintuitive cases if arbitrary formulas are used in the head and in the body. Such cases do not arise if the FLP semantics is applied to the class of programs that satisfy the condition of Theorem 8. For the same class of programs, system F2LP [Lee and Palla, 2009], an implementation of the first-order stable model semantics, can be viewed also as an implementation of the general FLP semantics.

Acknowledgements

We are grateful to anonymous referees for their useful comments on this paper. The authors were partially supported by the National Science Foundation under Grant IIS-0916116 and by the Office of the Director of National Intelligence (ODNI), Intelligence Advanced Research Projects Activity (IARPA), through the US Army Research Lab.