From Answer Set Logic Programming to Circumscription via Logic of GK

1 Introduction

Answer Set Programming (ASP) is a new paradigm of constraint-based programming based on logic programming with answer set semantics [Niemel¨a, 1999; Lifschitz, 1999; Marek and Truszczynski, 1999]. It started out with normal logic programs, which are programs that can have negation but not disjunction. Driven by the need of applications, various extensions have been proposed. These include disjunctive logic programs [Gelfond and Lifschitz, 1991; Leone et al., 2006], nested expressions [Lifschitz et al., 1999], cardinality and weight constraints [Niemel¨a; and Simons, 2000], and others. Recently, Ferraris [2005] proposed to view formulas in propositional logic as logic programs and showed that they include as special cases all the above mentioned classes of logic programs. In particular, Ferraris [2005] provided a stable model semantics for these formulas using a transformation similar to the original GelfondLifschitz transformation, and showed that this semantics coincides with Pearce's equilibrium logic [Pearce, 1997].

In this paper, we show that this general stable model semantics can be embedded in Lin and Shoham's logic of knowledge and justified assumptions [Lin and Shoham, 1992], aka logic of GK. Besides showing the generality of Lin and Shoham's logic, which was proposed as a general logic for nonmonotonic reasoning, this embedding allows us to obtain a way to check in classical propositional logic whether any given two logic programs are strongly equivalent in almost the same way as in [Lin, 2002]. It also allows us to obtain a mapping from general logic programs to propositional circumscription in the same way as Lin and Shoham [1992] did for mapping normal logic programs to circumscription. As it turned out, this mapping, when extended to first-order case, yields a semantics to first-order general logic programs that is similar to the one proposed recently by Ferraris et al. [2007].

We first briefly review Lin and Shoham's logic of GK, Ferraris's general logic programs, and Pearce's equilibrium logic.

2 Logic of GK

The language of the logic of GK is a modal propositional language with two modal operators, K, for knowledge, and A, for assumption. Given a set Atom of atoms (also called variables or primitive propositions), formulas in the logic of GK are defined inductively below in BNF notation:

where p ∈ Atom, and ⊥ is a constant standing for falsity. Formulas without modal operators are called base formulas.

The semantics of the logic of GK is defined through Kripke interpretations. A Kripke interpretation M is a tuple 〈W, π,RK,RA, s〉, where W is a nonempty set whose elements are called possible worlds, π a function that maps a possible world to a truth assignment on Atom, RK and RA binary relations over W representing the accessibility relations for K and A, respectively, and s ∈ W, called the actual world of M. The satisfaction relation |= between a Kripke interpretation M = 〈W, π, RK, RA, s〉 and a formula F is defined inductively as follows:

• M ̸|= ⊥;
• M |= p if π(s)(p) = 1, where p ∈ Atom;
• M |= ¬F iff M ̸|= F;
• M |= F ∧ G iff M |= F and M |= G;
• M |= F ∨ G iff M |= F or M |= G;
• M |= F → G iff M ̸|= F or M |= G;
• M |= K(F) iff 〈W, π,RK,RA,w〉 |= F for any w ∈ W, such that (s,w) ∈ RK;
• M |= A(F) iff 〈W, π,RK,RA,w〉 |= F for any w ∈ W, such that (s,w) ∈ RA.

We say that a Kripke interpretation M is a model of a formula F if M satisfies F. In the following, given a Kripke interpretation M, we let

Notice that K(M) and A(M) are always closed under classical logical entailment. In the following, for any set X of formulas, we let Th(X) be the logical closure of X under classical logic.

Definition 2.1 (GK Models) Given a formula F, a Kripke interpretation M is a minimal model of F if M is a model of F and there does not exist another model M1 of F such that A(M1) = A(M) and K(M1) ⊂ K(M). We say that M is a GKmodel 1 if M is a minimal model of F and K(M) = A(M).

Lin and Shoham showed that the logic of GK can be used to capture Reiter's default logic [Reiter, 1980] and Moore's auto-epistemic logic [Moore, 1985]. As a consequence, normal logic programs under stable model semantics can be captured in the logic of GK as well. Specifically, they showed that a normal rule

can be translated into the following sentence in the logic of

They also showed that this translation extends to disjunction logic programs.

In this paper, we shall show that general logic programs proposed by Ferraris [2005] can be captured in the logic of GK as well.

3 General logic programs

Given a set Atom of atoms, general logic programs [Ferraris and Lifschitz, 2005] are formulas defined inductively below in BNF notation:

where p ∈ Atom. Notice that there is no negation in the language. Instead, for any formula F, ¬F is considered to be a shorthand for F → ⊥.

A set X ⊆ Atom of atoms can be considered as a truth assignment in the straightforward way:

and the usual definition for the logical connectives.

The stable models of a formula (general logic program) are defined by a modified extended Gelfond-Lifschitz transformation. Given a general logic program F, and a set X of atoms, the reduct of F under X [Ferraris, 2005], written F X , is the formula obtained from F by replacing each maximal subformula that is not classically satisfied by X with ⊥.

1 In [Lin and Shoham, 1992], GK models are called preferred models.

Now a set X of atoms is a stable model of a general logic program F if:

• (ii) there is no proper subset X1 of X, such that X1 |= F X .

Example 3.1 Consider the following three general logic program.

where p, q are atoms. The maximal subformula in P that is false under {q} is p, thus P {q} is ¬⊥ → q, which is satisfied by {q}, but not by ∅. Therefore, {q} is a stable model of P. On the other hand, P {p} is ⊥ → ⊥, which is satisfied by {p} as well as its subset ∅. Therefore, {p} is not a stable model of P. It can be seen that {q} is the only stable model of P. Similarly, it can be shown that Q has two stable models, {p} and ∅, and R has exactly one stable model ∅.

4 Pearce's equilibrium logic

Pearce's equilibrium logic [Pearce, 1997] is based on the logic of here-and-there, a non-classical logic. Given a set Atom of atoms, formulas of Atom are exactly the same as in the case of general logic programs. Thus, negation in equilibrium logic is considered a shorthand as well.

The semantics of the logic of here-and-there is defined in terms of HT-interpretations, which are pairs 〈X, Y 〉 of sets atoms such that X ⊆ Y . The HT satisfaction relation 2 |= between an HT-interpretation 〈X, Y 〉 and a formula F is defined recursively as follows:

• For p ∈ Atom, 〈X, Y 〉 |= p if p ∈ X;
• 〈X, Y 〉 ̸|= ⊥;
• 〈X, Y 〉 |= F ∧G if 〈X, Y 〉 |= F and 〈X, Y 〉 |= G;
• 〈X, Y 〉 |= F ∨G if 〈X, Y 〉 |= F or 〈X, Y 〉 |= G;
• 〈X, Y 〉 |= F →G if
• (i) 〈X, Y 〉 ̸|= F or 〈X, Y 〉 |= G, and
• (ii) Y |= F →G.

An HT interpretation 〈X, Y 〉 is an equilibrium model of a formula F if X = Y , 〈X, Y 〉 |= F , and there is no proper subset X1 of X, such that 〈X1, Y 〉 |= F. Ferraris [2005] showed that the stable models of a formula are essentially the same as its equilibrium models.

Theorem 1 (Ferraris) Let X be a set of atoms and F a general logic program, X is a stable model of F iff 〈X,X〉 is an equilibrium model of F .

2 We overload |=, and use it to stand for satisfaction relations for modal logic, classical logic, and logic of here-and-there. Which one it stands for should be clear from the context.

5 From general logic program and equilibrium logic to the logic of GK

In this section, we present a translation from a general logic program (also a formula in equilibrium logic) to a formula in the logic of GK, and show that under the translation, stable models (thus equilibrium models) coincide with GK models in the logic of GK.

Given a general logic program F, we define two formulas FA and FGK in the logic of GK as follows:

1. FA is obtained fromF by simultaneously replacing each atom p by Ap.
2. FGK is defined inductively as follows:
3. ⊥GK = ⊥;
4. For p ∈ Atom, pGK = Kp;
5. (F ⊙G)GK = FGK ⊙GGK (⊙ is ∧ or ∨).
6. (F →G)GK = (FGK →GGK) ∧ (F →G)A.

It can be shown that for a normal logic program F , FGK is equivalent to the translation by Lin and Shoahm [1992] given in Section 2 under

and that for any formula W in the logic of GK, M is a GK model of W iff M is a GK model of W ∧ (2).

This translation is also similar to the mapping from formulas in equilibrium logic to quantified boolean formulas given in [Pearce et al., 2001]. We shall discuss this in more detail in a later section.

To illustrate, consider the three programs in Example 3.1. PGK is

which is equivalent (in classical logic) to

which is

Now let M be a model of the above sentence. If p ∈ A(M), then (3) holds no matter what K(M) is, thus its minimal model is K(M) = Th(∅), so cannot be a GK model. Now if p ̸∈ A(M), then (3) is equivalent to (¬Kp → Kq) ∧ Aq. Thus q ∈ A(M). Thus if M is a minimal model, then K(M) = Th({q}). And if A(M) = K(M), then M is a GK model. What we have shown here is that in any GK model M of (3), K(M) = A(M) = Th({q}). The existence of such a model is apparent.

It can be similarly shown that QGK is equivalent to Ap → Kp, and that M is a GK model of QGK iff K(M) = A(M) = Th({p}) or K(M) = A(M) = Th({⊤}). And RGK is equivalent to Kp → Ap, and that M is a GK model of RGK iff K(M) = A(M) = Th({⊤}). Thus for these three programs, their GK models correspond one-to-one with their stable models. In general, we have the following result.

Theorem 2 Let X be a set of atoms and F a general logic program. The following three statements are equivalent.

1. X is a stable model of F.
2. 〈X,X〉 is an equilibriummodel of F.
3. There is a GK model M of FGK such that K(M) = A(M) = T h(X).

Proof sketch: Given a general logic program F, two set of atoms X and Y such that X ⊆ Y and a Kripke structure M such that K(M) = Th(X), A(M) = Th(Y ), by induction on the structure of F, we have X |= F Y iff M |= FGK. From this, 2 ⇔ 3 follows. By Theorem 1, 1 ⇔ 2.

6 From general logic programs and equilibrium logic to circumscription: propositional case

Given their mapping (1) from normal logic program to the logic of GK, Lin and Shoham [1992] showed that stable model semantics for normal logic programs can be captured in circumscription [McCarthy, 1986] as follows. Given a set Atom = {p, q, ...} of atoms, let Atom′ = {p′ , q′ , ...} be a new set of atoms. Given a normal logic program F , let C(F) be the conjunction of the sentences:

for each rule

in F . Lin and Shoham [1992] showed that X is a stable model of F iff X ∪X′ is a model of

where Circum(W;Q) is the circumscription of the atoms in Q in W (with all other atoms fixed). Lin and Shoham also showed that this result can be extended to disjunctive logic programs. Using the same idea, we can capture the stable model semantics of general logic program and equilibrium logic in circumscription as well.

Let Atom be a set of atoms. Again let Atom′ = {p′ | p ∈ Atom} be a set of new atoms. Given any general logic program F in the language Atom, let C(F) be the result obtained from FGK by replacing every Kp in it by p and every Ap in it by p′ , for every p ∈ Atom.

Theorem 3 For any general logic program F in the language Atom, any set X ⊆ Atom, the following four statements are equivalent

1. X is a stable model of F.
2. 〈X,X〉 is an equilibriummodel of F.
3. There is a GK model M of FGK such that K(M) = A(M) = T h(X).
4. X ∪X′ is a model of

Proof sketch: 3 ⇔ 4 follows from the definitions of GK models and circumscription.

Interestingly, our translation C(F) that embeds general logic programs and equilibrium logic in circumscription is exactly the same as the one by Pearce et al. [Pearce et al., 2001] for embedding equilibrium logic in quantified boolean formulas. They showed that 〈X,X〉 is an equilibriummodel of a formula F in equilibrium logic iff X′ is a model of the following quantified boolean formula:

where F ′ is the formula obtained from F by replacing every atom p by p′ , and Atom < Atom′ stands for

While propositional circumscription is also a quantified boolean formula, it is a well studied formalism. There are many known results about circumscription that we can use. Mapping logic programs to circumscription helps understanding both formalisms.

Notice that the formula ∧p∈Atom(p ↔ p′ ) is equivalent to

Thus (4) is equivalent to

which is equivalent to

as the atoms (predicates) to be minimized occur only negatively in ∧p∈Atom(p → p′ ). Putting the formula ∧p∈Atom(p → p′ ) into the theory in the circumscription is good as it can be used to simplify C(F).

Proposition 6.1 If ∧p∈Atom(p → p′ ) |= C(F) ↔ W, then (4) is equivalent to

Consider again the three programs in Example 3.1. For P, C(P) is equivalent to ¬p ∧ ¬p′ → q, which is equivalent to ¬p′ → q under (p → p′ ) ∧ (q → q′ ). Thus for this program, (4) is equivalent to

which is equivalent to

which has a unique model {q, q′ }.

For Q = ¬p ∨ p, C(Q) is equivalent to p′ → p. Thus for this program, (4) is equivalent to

which is equivalent to p ↔ p′ , which has two models p and ¬p.

7 From general logic programs and equilibrium logic to circumscription: first order case

As in [Lin and Shoham, 1992], we can extend the above mapping to the first-order case. First of all, we extend logic programs to first-order case. Let L be a relational first-order language with equality, i.e. it has no proper functions. By an atom, we mean an atomic formula including equality atoms.

In the following, let Σuna be the set of unique names assumptions on constants: c1 ̸= c2 for any two distinct constants c1 and c2.

A first-order general logic program is a first-order sentence in the following set:

where A is an atom, and x a variable. Again, for any general logic program F , ¬F is considered to be a shorthand for F →

⊥.

Now let M be a finite model of Σuna with domain D. Let σ be the mapping from constants to D under M. Clearly, for any distinct constants c1 and c2, σ(c1) ̸= σ(c2). We say that M is a stable model of a first-order general logic program F if T(M), the set of ground facts true inM:

is a stable model of the general logic program FM, which, called the grounding of F on M, is obtained from F and M in two steps:

1. First, replace every constant c in F by σ(c), every subformula of the form ∀xW in it by ∧u∈D W(x/u), and every subformula of the form ∃xW in it by ∨u∈D W(x/u), where W(x/u) is the result of replacing every free occurrence of x in W by u. The order by which these subformulas are replaced does not matter.
2. In the expression obtained by the first step, replace every equality atom u = u by ⊤, and every u = u′ for distinct u and u′ by ⊥.

Example 7.1 Consider the following four programs:

Now consider a structure with two elements {a, b}. The grounding of the four programs on this domain are

respectively. So for this domain, F1 and F3 have the same stable models, {p(a)} and {p(b)}, and F2 and F4 have the same stable models, {p(a), q} and {p(b), q}. It is easy to see that this is the case for any given domain: F1 and F3 have the same stable models, and F2 and F4 have the same stable models.

We now show that the stable models of first-order general logic programs can be captured in circumscription as well.

Let Δ be the set of predicates in the language. Let Δ′ be a set of new predicates, one for each P in Δ with the same arity and denoted by P ′ . Now given a first-order general logic program F, let C(F) be the first-order sentence defined inductively as follows.

• C(⊥) is ⊥.
• If W is an atomic formula, then C(W) is W.
• C(W1 ⊙W2) is C(W1) ⊙ C(W2), where ⊙ ∈ {∧, ∨}.
• C(∀xW) is ∀xC(W), and C(∃xW) is ∃xC(W).
• C(W1 → W2) is (C(W1) → C(W2)) ∧ (W ′1 → W ′2 ), where W ′ is the result of replacing every predicate P in W by P ′ .

The stable models of F is then the circumscription of all the predicates in Δ in C(F), together with the following axiom

Theorem 4 Let M be a finite model of Σuna. M is a stable model of F iff M ′ is a model of

where M ′ is the conservative extension of M under (5).

Similar to Proposition 6.1, we have

Proposition 7.1 If ∧P∈Δ ∀⃗x(P(⃗x) → P ′ (⃗x)) |= C(F) ↔ W, then (6) is equivalent to

Interestingly, Ferraris et al. [2007] also proposed a semantics for general first-order logic programs and showed that their semantics is equivalent to (6) when restricted on the predicates in the original program, that is, when all new predicates P ′ in (6) are existentially quantified.

Example 7.2 Consider the programs in Example 7.1

which is equivalent to ∃xp(x) ∧ (¬∃xp′ (x) → q) under ∀x.p(x) → p′ (x). Therefore, under (5), Circum(C(F1), {p, q}) is equivalent to

thus equivalent to

which can be considered to be the first-order semantics of F1. If D = {a, b}, then there are exactly two models of this sentence, {p(a)} and {p(b)}.

• C(F2) is

which is equivalent to

under ∀x.p(x) → p′ (x). Therefore, Circum(C(F2), {p, q}) is equivalent to

under (5), thus equivalent to

which can be considered to be the first-order semantics of F2. If D = {a, b}, then there are exactly two models of this sentence, {p(a), q} and {p(b), q}.

• C(F3) is

which is equivalent to C(F1) under (5). Thus F1 and F3 are equivalent.

• C(F4) is

∃xp(x) ∧ ∀x[(¬p(x) ∧ ¬p′ (x) → q) ∧ (¬p′ (x) → q′ )], which is equivalent to C(F2). Thus F2 and F4 are equivalent.

8 Strong equivalence

The notion of strong equivalence [Lifschitz et al., 2001] is important in logic programming. For disjunctive logic programs, research by Lin and Chen [2005] and Eiter et al. [2006] show that interesting programs transformation rules can be designed based on the notion.

According to Ferraris and Lifschitz [2005], two general logic programs F and G are said to be strongly equivalent if for any formula F1 that contains an occurrence of F, F1 has the same stable models as the formula obtained from it by replacing an occurrence of F by G. They showed that for any F and G, they are strongly equivalent iff F and G are equivalent in the logic here-and-there.

As it turns out, our mapping from equilibrium logic to logic of GK also embeds logic of here-and-there to modal logic. Thus the problem of deciding whether two programs are strongly equivalent can be reduced to checking whether certain modal logic formulas are valid, and that, because of the special format of these modal formulas, can in turn be reduced to checking whether certain propositional formulas are tautologies.

Theorem 5 Let F be a formula in equilibrium logic, X and Y two sets of atoms such that X ⊆ Y , and M a Kripke interpretation such that K(M) = Th(X) and A(M) = Th(Y ). We have that 〈X, Y 〉 |= F iff M |= FGK.

Theorem 6 Let F and G be two general logic programs. The following conditions are equivalent.

1. F and G are strong equivalent.
2. F is equivalent to G in the logic here-and-there.
3. ∧p∈Atom(Kp →Ap) |= (F ↔G)GK.
4. ∧p∈Atom(Kp →Ap) |= FGK ↔GGK.
5. ∧p∈Atom(p → p′ ) |= C(F ↔G).
6. ∧p∈Atom(p → p′ ) |= C(F) ↔C(G).

Corollary 7 The problem of deciding whether two general logic programs are strongly equivalent is co-NP complete.

9 Conclusion

We showed that the logic of GK proposed by Lin and Shoham is flexible enough to handle stable model semantics of general logic programs. Because of this, the stable model semantics of general logic programs can also be formulated in circumscription, in both propositional and first-order case. For future work, we plan to make use of the expressive power of GK in other applications.

Acknowledgments

We thank Vladimir Lifschitz for stimulating discussions on topics related to this paper, and for his helpful comments on earlier versions of this paper. This work was supported in part by HK RGC under grant HKUST6170/04E, and by China NSFC under grant 60496322.