Simplifying A Logic Program Using Its Consequences

1 Introduction

Answer Set Programming (ASP) has been considered as one of the most popular nonmonotonic rule-based formalisms, mainly due to the availability of efficient ASP solvers such as smodels [Syrj¨anen and Niemel¨a, 2001], ASSAT [Lin and Zhao, 2004], cmodels [Lierler and Maratea, 2004], clasp [Gebser et al., 2007a], claspD [Drescher et al., 2008], and DLV [Leone et al., 2002].

All of these modern ASP solvers require a preprocessing state for simplifying a logic program by its consequences in their grounding engines, like lparse [Syrj¨anen, 2000], gringo [Gebser et al., 2007b], and the grounding engine for DLV [Leone et al., 2002]. In specific, a consequence is a consistent set of literals that are satisfied by every answer set of the program. Many consequences can be derived using efficient inference rules before computing the answer sets of the program. For instance, a consequence can be computed by applying unit propagation to the set of clauses obtained from Clark's completion [Clark, 1978] of the program, applying the well-founded operator [Leone et al., 1997] to the program, using the loop formulas of loops with at most School of Software Sun Yat-sen University Guangzhou 510006, China wanhai@mail.sysu.edu.cn one external support rule [Chen et al., 2013], and applying the lookahead operator based on previous operations.

∗Corresponding author

These consequences can help computing the answer sets of the program. The notion of consequences is also extended in [Eiter et al., 2004] to simplify logic programs under uniform and strong equivalence. However, not all consequences can be used to simplify the logic program, as simplified programs may have answer sets that are not answer sets of the original program. The best known consequences for simplifying programs are the well-founded models for normal logic programs [Van Gelder et al., 1991] and the results computed by the well-founded operator for disjunctive logic programs [Leone et al., 1997], the approximations of which have been used in grounding engines of most ASP solvers.

To extend the notion of well-founded models, we consider when a consequence can be used to simplify a logic program. In this paper, we provide two notions, called strong reliable set and weak reliable set, so that

• a logic program is strongly equivalent to the simplified program iff the consequence is a strong reliable set,
• they have the same answer sets iff the consequence is a weak reliable set.

We also explore computational complexity on identifying both sets. These notions provide a guideline to explore classes of consequences that could be used to simplify a logic program. As an example, we provide an algorithm to compute some strong reliable sets and show that the approach is an extension of the well-founded model in simplifying logic programs.

2 Preliminaries

In this paper, we consider only fully grounded finite logic programs. A (disjunctive) logic program (DLP) is a finite set of (disjunctive) rules of the form

where n ≥ m ≥ k ≥ 0, n ≥ 1 and a1, . . . , an are atoms. If k ≤ 1, it is a normal rule; if m = n, it is a positive rule; if n = m = k = 1, it is a fact. In particular, a normal logic program (NLP) is a finite set of normal rules and a positive logic program is a finite set of positive rules.

We will also write rule r of form (1) as

where head(r) is a1 ∨ · · · ∨ ak, body(r) = body+(r) ∧ body-(r), body+(r) is ak+1 ∧ · · · ∧ am, and body-(r) is ¬am+1 ∧ · · · ∧ ¬an, and we identify head(r), body+(r), body-(r) with their corresponding sets of atoms.

A set S of atoms satisfies a rule r, if body+(r) ⊆ S and body-(r) ∩ S = ∅ implies head(r) ∩ S ̸= ∅. S satisfies a program P, if S satisfies every rules in P. Let L be a set of literals and F a propositional formula, we write L |= F if L entails F in the sense of classical logic, L = {¬p | p ∈ L} ∪ {p | ¬p ∈ L}, L+ = {p | p ∈ L}, and L- = {p | ¬p ∈ L}.

In the following we recall the basic notions about answer sets [Gelfond and Lifschitz, 1991], SE-models [Turner, 2003], external support rules and loop formulas [Lee and Lifschitz, 2003], the well-founded model [Van Gelder et al., 1991], and the well-founded operator [Leone et al., 1997].

2.1 Answer Set Semantics

Given a DLP P and a set S of atoms, the Gelfond-Lifschitz reduct of P on S, written P S , is obtained from P by deleting:

1. each rule that has a formula not p in its bodywith p ∈ S,
2. all formulas of the form not p in the bodies of the remaining rules.

A set S of atoms is an answer set of P if S is a minimal set satisfying P S .

A SE-interpretation is a pair (X, Y ) where X and Y are sets of atoms and X ⊆ Y . A SE-interpretation (X, Y ) is a SE-model of a DLP P if Y satisfies P and X satisfies P Y . A SE-model (Y, Y ) of P is an equilibrium model of P, if there does not exist another set X such that X ⊂ Y and (X, Y ) is a SE-model of P .

Two DLPs P1 and P2 are strongly equivalent, if for any DLP P ′ , programs P1 ∪P ′ and P2 ∪P ′ have the same set of answer sets.

The SE-models and the answer sets of a DLP have the following proposition [Ferraris, 2005; Lifschitz et al., 2001].

Proposition 1 Let P1, P2 be two DLPs and S a set of atoms.

• S is an answer set of P1 iff (S, S) is an equilibrium model of P1.
• P1 is strongly equivalent to P2 iff P1 and P2 have the same SE-models.

2.2 External Support Rules and Loop Formulas

Given a nonempty set E of atoms, a rule r is an external support of E if head(r) ∩ E ̸= ∅ and E ∩ body+(r) = ∅. Given a DLP P, we use R-(E, P) to denote the set of external support rules of E in P .

The (conjunctive) loop formula of E under P, written LF(E, P), is the following implication

A set S of atoms satisfies LF(E, P), if E ⊆ S implies that there exists a rule r ∈ R-(E, P) such that body+(r) ⊆ S, body-(r)∩S = ∅, and (head(r)\E)∩S = ∅, i.e., S∪{¬p | p /∈ S} |= LF(E, P).

Proposition 2 (Theorem 1 in [Lee and Lifschitz, 2003])

Let P be a DLP and S a set of atoms. If S satisfies P, then following conditions are equivalent to each other:

• S is an answer set of P;
• S satisfies LF(E, P) for every nonempty set E of atoms.

2.3 Well-Founded Semantics

Let P be a DLP and I a set of literals, a set X of atoms is an unfounded set of P w.r.t. I if for each atom p ∈ X and each rule r ∈ P such that p ∈ head(r), at least one of the following conditions holds:

• body(r) ∩ I ̸= ∅,
• X ∩ body+(r) ̸= ∅, or
• (head(r) \X) ∩ I ̸= ∅.

Let I be a set of literals. If P is an NLP, the union of two unfounded sets is also an unfounded set. I is unfoundedfree for a DLP P if I ∩ X = ∅ for each unfounded set X of P w.r.t. I. If I is unfounded-free, then the union of two unfounded sets of P w.r.t. I is also an unfounded set, thus there exists the greatest unfounded set of P w.r.t. I. We use UP (I) to denote such greatest unfounded set, if exists.

We define two operators for a DLP P and a set I of literals:

TP (I) = {p | there exists a rule r ∈ P s.t. p ∈ head(r)

TP , UP , and WP are monotonic operators. We use WFM(P ) to denote the least fixed point of the operator WP . If P is an NLP, WFM(P) is the well-founded model of P as defined in [Van Gelder et al., 1991].

3 Simplifying A Logic Program

A consequence of a program is a consistent set of literals that are satisfied by every answer set of the program. A consequence is positive if it is a set of atoms. Some consequences can simplify the logic program in the manner that, the resulting program consists of two parts, a part without any atoms appearing in the consequence and the facts of the consequence. WFM(P) is such a consequence that is commonly used to simplify the program in the grounding engines, like lparse [Syrj¨anen, 2000], gringo [Gebser et al., 2007b], and the grounding engine for DLV [Leone et al., 2002], of modern ASP solvers. In this section, we consider how to extend the idea to other consequences of the program.

Let L be a consequence of a DLP P , we define trn(P, L) to be the program obtained from P by

1. deleting each rule r that has an atom p ∈ body+(r) with ¬p ∈ L, and
2. replacing each rule r that has an atom p ∈ head(r) or p ∈ body-(r) with ¬p ∈ L by a rule r′ such that head(r′ ) = head(r) \ L-, body+(r′ ) = body+(r), and body-(r′ ) = body-(r) \ L-.

We define trp(P, L) to be the program obtained from P by

1. deleting each rule r that has an atom p ∈ head(r) or p ∈ body-(r) with p ∈ L, and

1. replacing each rule r that has an atom p ∈ body+(r) with p ∈ L by a rule r′ such that head(r′ ) = head(r), body+(r′ ) = body+(r)\L+, and body-(r′ ) = body-(r).

Note that trn(P,L) (resp. trp(P,L)) does not contain any atoms in L- (resp. L+) and trp(trn(P, L), L) does not contain any atoms occurring in L.

The following property explains why WFM(P) can be used to simplify the program P .

Proposition 3 Let P be a DLP and L = WFM(P ).

• (i) P and trp(trn(P,L),L) ∪ {p ← | p ∈ L} have the same set of answer sets.
• (ii) P ∪ {← p | ¬p ∈ L} is strongly equivalent to

Both conditions in Proposition 3 would no longer be true, if L is larger than WFM(P).

Example 1 Consider the logic program P0:

WFM(P0) = ∅, L = {a} is a consequence of P0, and trp(trn(P0, L), L) = {b ← not c, c ← not b}. Notice that, {a, c} is an answer set of trp(trn(P0, L), L)∪{p ← | p ∈ L}, but not an answer set of P0.

Proposition 4 Let L be a consequence of a DLP P .

• P and trn(P, L) have the same set of answer sets.
• P ∪ {← p | ¬p ∈ L} is strongly equivalent to trn(P, L) ∪ {← p | ¬p ∈ L}.
• An answer set of P is always an answer set of trp(P, L)∪{p ←| p ∈ L}, but not vice versa in general.

Proof Sketch: For any nonempty set E of atoms, under L, the loop formula LF(E, P) is equivalent to LF(E, trn(P,L)), and LF(E, P) implies LF (E, trp(P, L) ∪ {p ←| p ∈ L}).

Given a consequence L of a DLP P, we can simplify the program by trn(P, L) which would no longer contain atoms appearing in L-. However, we cannot use trp(P,L) to simplify P in general.

Example 2 Consider the logic program P1:

L = {a, f} is a consequence of P1, and trp(P1, L) is:

The only answer set of P1 is {a, b, c, d, f}. However, trp(P1, L) has two answer sets: {b, c, d} and {b, c, e}.

In the next section, we consider when the conditions in Proposition 3 would be true for a positive consequence L.

4 Strong andWeak Reliable Sets

In this section, we introduce notions of the strong reliable set and the weak reliable set, so that they specify sufficient and necessary conditions when a positive consequence L satisfies condition (ii) and (i) in Proposition 3 respectively. We also explore computational complexity on identifying a strong or a weak reliable set.

Given a DLP P, a set U of atoms is a strong reliable set of P, if for every nonempty subset E of U and every SE-model (X, Y ) of P, there exists a rule r ∈ R-(E, P) such that head(r) ∩ X ⊆ E, body+(r) ⊆ X ∪ U, and body-(r) ∩ (Y ∪ U) = ∅.

Proposition 5 If U is a strong reliable set of a DLP P, then for every SE-model (X, Y ) of P, U ⊆ X, and U is a consequence of P .

Proof Sketch: From the definition, for every SE-model (X, Y ) of P and every nonempty subset E of U, U \ E ⊆ X implies E ∩ X ̸= ∅. P is finite, then U ⊆ X.

Theorem 1 Let P be a DLP and U a set of atoms. P is strongly equivalent to trp(P, U) ∪ {p ←| p ∈ U} if and only if U is a strong reliable set of P .

Proof Sketch: ⇐: From Proposition 5, for every SE-model (X, Y ) of P , U ⊆ X. Then both programs have the same set of SE-models.

• ⇒: Assume that U is not a strong reliable set of P, then there exists a nonempty subset E of U and a SE-model (X, Y ) of P that prevent U to be a strong reliable set. From the definition, X \ E satisfies P Y , so (X \ E, Y ) is also a SE-model of P, which conflicts to the fact that (X\E, Y ) is not a SE-model of trp(P, U)∪{p ←| p ∈ U}.

So given a positive consequence L of a DLP P, the condition (ii) in Proposition 3 is true if and only if L is a strong reliable set of P .

Before defining the notion of the weak reliable set, we introduce a notation. Given a DLP P and a set U of atoms, a SE-model (X, Y ) of P is called a U-equilibrium model of P, if U ⊆ Y , Y \ U = X \ U and there does not exist another set X′ such that X′ \ U ⊂ X \ U and (X′ ∪ U, Y ) is a SE-model of P. We show that, a U-equilibrium model of P is related to an answer set of trp(P, U).

Lemma 1 Let P be a DLP and U a set of atoms. A SEinterpretation (X, Y ) is a SE-model of trp(P, U) if and only if there exists a SE-model (X∗ , Y ∗ ) of P such that X∗ = X ∪U and Y ∗ = Y ∪U.

Proposition 6 Let P be a DLP and U a set of atoms. A set S is an answer set of trp(P,U) if and only if there exists a Uequilibrium model (X, Y ) of P such that X\U = Y \U = S.

Proof Sketch: ⇐: (X, Y ) is a U-equilibrium model of P, then X∪U = Y ∪U and (X∪U, Y ∪U) is a SE-model of P . So (X \ U, Y \ U) is a SE-model of trp(P, U). Meanwhile, there does not exist a set X′ such that X′ \ U ⊂ X \ U and (X′ ∪ U, Y ∪ U) is a SE-model of P. From Lemma 1, (X′ \ U, Y \ U) is a SE-model of trp(P,U). So X \ U is an answer set of trp(P,U).

• ⇒: S is answer set of trp(P,U), then (S ∪ U, S ∪ U) is a SE-model of P and there does not exists a set S′ such

that S′ ⊂ S and (S′ , S) is a SE-model of trp(P,U). From Lemma 1, (S′ ∪ U, S ∪ U) is a SE-model of P. Then (S ∪ U, S ∪ U) is a U-equilibrium model of P .

Given a DLP P, a set U of atoms is a weak reliable set of P, if for every nonempty subset E of U and every Uequilibrium model (X, Y ) of P, there exists a rule r ∈ R-(E, P ) such that head(r) ∩ X ⊆ E, body+(r) ⊆ X ∪ U , and body-(r) ∩ (Y ∪ U) = ∅.

Similar to the proof of Proposition 5, we have the following proposition.

Proposition 7 If U is a weak reliable set of a DLP P, then for every U-equilibrium model (X, Y ) of P , U ⊆ X, and U is a consequence of P .

Theorem 2 Let P be a DLP and U a set of atoms. P and trp(P, U) ∪ {p ←| p ∈ U} have the same set of answer sets if and only if U is a weak reliable set of P .

Proof Sketch: ⇐: From Proposition 7, for every Uequilibrium model (X, Y ) of P , U ⊆ X, then X = Y . From Proposition 6, for every answer set S of trp(P,U), there exists a U-equilibriummodel (S∪U, S∪U) of P , then S∪U is an answer set P . So P and trp(P, U) ∪ {p ←| p ∈ U} have the same set of answer sets.

⇒: If U is not a weak reliable set of P, then there exists a U-equilibrium model (X, Y ) of P and a nonempty subset E of U that prevent U to be a weak reliable set of P . Similar to the proof for Theorem 1, (X \ E, Y ) is also a U-equilibrium model of P. Then Y is not an answer set of P but Y is an answer set of trp(P, U) ∪ {p ←| p ∈ U}.

So given a positive consequence L of a DLP P, the condition (i) in Proposition 3 is true if and only if L is a weak reliable set of P .

Proposition 8 Let P be a DLP and U a set of atoms. If U is a strong reliable set of P , then U is a weak reliable set of P .

Proposition 9 If U1 and U2 are strong (resp. weak) reliable sets of a DLP P, then U1 ∪ U2 is also a strong (resp. weak) reliable set of P.

Given a DLP P, there exists the greatest strong (resp. weak) reliable set of P, denoted by GSRS(P) (resp. GWRS(P)), i.e., the union of all possible strong (resp. weak) reliable sets.

Proposition 10 Let P be a DLP and U a set of atoms.

• Deciding whether U is a strong reliable set of P is coNP-complete.
• Deciding whether U is a weak reliable set of P is coNPhard.
• Deciding whether U is equivalent to GSRS(P) (resp. GWRS(P)) is coNP-hard.
• Deciding whether an atom p is in GSRS(P) (resp. GWRS(P)) is coNP-hard.

Proof Sketch: The first item is a coNP problem, as we can guess a nonempty subset E of U and a SE-model (X, Y ) of P which prevents U to be a strong reliable set.

The hardness is proved by converting the UNSAT problem to these problems. Let t and e be new atoms not appearing in a set C of clauses, and Atoms(C) the set of atoms in C. We can construct a DLP P from C by:

• adding rules t ∨ e ∨ ∨p∈Atoms(C) p ← and t ← e,
• for each clause C ∈ C, adding the rule e ∨ ∨¬p∈C p ← ∧q∈C q, and
• for each atom p ∈ Atoms(C), adding rules t ← p and p ← e.

It can be verified that U = Atoms(C) ∪ {t, e} is a strong reliable set of P if and only if C is not satisfiable. Moreover, U is a strong reliable set of P iff it is a weak reliable set of P iff U = GSRS(P ) = GWRS(P ) iff e ∈ GSRS(P ).

Even when P is an NLP, it is still hard to recognize a strong or a weak reliable set.

Proposition 11 Let P be an NLP and U a set of atoms.

• Deciding whether U is a strong (resp. weak) reliable set of P is coNP-complete.
• Deciding whether U is equivalent to GSRS(P) (resp. GWRS(P)) is coNP-hard.
• Deciding whether an atom p is in GSRS(P) (resp. GWRS(P)) is coNP-hard.

Proof Sketch: As P is an NLP, whether a SE-model (X, Y ) is a U-equilibrium model can be checked in polynomial time. So deciding whether U is a weak reliable set of an NLP P is a coNP-problem.

The hardness is proved by converting the UNSAT problem to these problems.

Let e, t, and t′ be new atoms not appearing in a set C of clauses, and Atoms(C) the set of atoms in C. We can construct an NLP P from C by:

• adding rules e ← t, t ← not t′ , t′ ← not t, and ← t′ , e,
• for each atom p ∈ Atoms(C), adding the rule p ← e, and
• for each clause C ∈ C, adding the rule e ← ∧¬p∈C p ∧ ∧q∈C ¬q.

It can be verified that U = Atoms(C) ∪ {e, t} is a strong reliable set of P if and only if C is not satisfiable. Moreover, U is a strong reliable set of P iff U is a weak reliable set of P iff U = GSRS(P ) = GWRS(P ) iff e ∈ GSRS(P ).

Now we provide an alternative definition of strong reliable sets, which implies an approach to recognize a strong reliable set of a DLP.

Proposition 12 Let P be a DLP and U a set of atoms. U is a strong reliable set of P if and only if U ⊆ X for every SE-model (X, Y ) of P .

Proof Sketch: From the definition, if U ⊆ X for every SE-model (X, Y ) of P, then U is a strong reliable set of P. Proposition 5 proves the other direction.

From [Pearce et al., 2001], a DLP P can be translated to a propositional formula π(P), such that (X, Y ) is a SE-model of P iff X ∪ ˆ Y is a model of π(P), where ˆ Y is a set of new atoms for each atom in Y . Based on this result, the following proposition provides an approach to identify a strong reliable set of a DLP.

Proposition 13 Let P be a DLP and U a set of atoms. U is a strong reliable set of P if and only if π(P) |= ∧ U in propositional logic.

Though, it is difficult to verify whether a positive consequence U is a strong or a weak reliable set of a program P, there are some easy cases as follows.

Proposition 14 If U is a positive consequence of a positive logic program P , then U is a strong reliable set of P .

From Proposition 13, given a DLP P, we can compute a consequence L by using efficient inference rules, like unit propagation, on the CNF form of π(P). Then L+ is a strong reliable set of P and L can be used to simplify the program P .

The notions of the strong and the weak reliable sets also provide a guideline to explore classes of positive consequence that could be used to simplify the program. We provide such an example in the next section.

5 Reliable Sets Under a Consequence

Guided by the definition of strong reliable sets, we introduce a sufficient condition for a consequence to simplify a logic program. We also provide an algorithm to identify the class of consequences specified by this sufficient condition. We show that for some programs, the consequence in the class is larger than the well-founded model.

Given a DLP P and a consistent set L of literals, a set U of atoms is a reliable set of P under L, if for every nonempty subset E of U, there exists a rule r ∈ R-(E, P) such that head(r) \ L- ⊆ E and U ∪ (L \ L+) |= body(r).

Let L be a consequence of a DLP P. A reliable set of P under L is also a strong (resp. weak) reliable set of a DLP constructed from P and L.

Proposition 15 Let P be a DLP, U a set of atoms, and L a consequence of P . If U is a reliable set of P under L, then U is a strong and a weak reliable set of the program:

Proof Sketch: U is a reliable set of P under L. From the definition, for any SE-model (X, Y ) of P with L+ ⊆ Y and L- ∩ Y = ∅ and any nonempty subset E of U, if U \ E ⊆ X, then E ∩ X ̸= ∅. There is a finite number of atoms, then U ⊆ X. So there exists a rule r ∈ R-(E, P) such that head(r) ∩ X ⊆ E, body+(r) ⊆ X ∪ U and body-(r) ∩ (Y ∪ U) = ∅. U is a strong and a weak reliable set of the new program.

From Proposition 15, Theorem 1 and 2, the notion can be used to simplify a logic program.

Corollary 3 Let P be a DLP, U a set of atoms, and L a consequence of P. If U is a reliable set P under L, then

• (i) P and trp(U) ∪ {p ←| p ∈ U} have the same set of answer sets.
• (ii) P ∪ {← not p | p ∈ L} ∪ {← p | ¬p ∈ L} is strongly equivalent to

The strongly equivalent relation mentioned in the previous corollary can be further specified in the following theorem.

Theorem 4 Let P be a DLP, U a set of atoms, and L a consistent set of literals.

is strongly equivalent to

if and only if U is a reliable set of P under L.

Proof Sketch: Let P1, P2 stand for these programs respectively.

• ⇐: U is a reliable set of P under L implies U is a strong reliable set of P1 under L. The direction can be proved from Corollary 3.

⇒: Assume that U is not a reliable set of P under L, then there exists a nonempty subset E of U which prevents U to be a strong reliable set of P under L. It can be verified that (U ∪ L+) \ E satisfies P U∪L+ 1 , so ((U ∪ L+) \ E, U ∪ L+) is a SE-model of P1, which conflicts to the fact it is not a SE-model of P2.

Proposition 16 If U1 and U2 are reliable sets of a DLP P under a consistent set L of literals, then U1 ∪ U2 is also a reliable set of P under L.

Given a DLP P and a consistent set L of literals, there exists the greatest reliable set of P under L. We denote it by GRS(P,L), i.e., the union of all possible reliable sets of P under L.

Example 3 (Example 2 continued) Recall that L = {a, f} is a consequence of P1. From the definition, GRS(P1,L) = ∅. L′ = {¬e} is another consequence of P1, and GRS(P1, L′ ) = {a, b, c, d, f}.

Proposition 17 Let P be a DLP, U a set of atoms, and L a consequence of P .

• Deciding whether U is a reliable set of P under L is coNP-complete.
• Deciding whether U is equivalent to GRS(P,L) is coNP-hard.
• Deciding whether an atom p is in GRS(P,L) is coNPhard.

Proof Sketch: The first item is a coNP problem, as we can guess a corresponding set E which prevents U to be a reliable set of P under L.

In the proof of Proposition 10, the set U = Atoms(C) ∪ {t, e} is a strong reliable set of P iff U is a reliable set of P under ∅ iff U = GRS(P, ∅) iff e ∈ GRS(P, ∅).

When P is an NLP, GRS(P,L) can be computed efficiently. In the following, we provide such a polynomial time algorithm, which can also be used to compute a subset of GRS(P, L) for a DLP P .

Let P be a DLP, X a set of atoms and L a set of literals.

TP,L(X) = {p | there is a rule r ∈ P such that p ∈ head(r),

TP,L is a monotonic operator. We use T(P, L) to denote the least fixed point of TP,L.

Proposition 18 Let P be an NLP and L a consistent set of literals. GRS(P, L) = T (P, L).

Proof Sketch: (1) If U is a reliable set of P under L, then TP,L(U) is also a reliable set of P under L. So T(P,L) ⊆ GRS(P, L).

(2) If there is an atom p ∈ U, U is a reliable set of P under L, and p /∈ T(P,L), then U \ {p} ̸⊆ T(P,L). So GRS(P, L) ⊆ T (P, L).

Note that, T(P,L) can be computed in polynomial time, then GRS(P, L) can be computed efficiently for NLPs.

Proposition 19 Let P be a DLP and L a consistent set of literals. T (P, L) ⊆ GRS(P, L).

We show that GRS(P,L) also extends the well-founded operator.

Proposition 20 Let P be a DLP, L1 and L2 be consistent sets of literals with L1 ⊆ L2. The following hold:

• WFM(P )+ ⊆ GRS(P, ¬WFM(P )-).
• GRS(P,L1) ⊆ GRS(P,L2).

Example 4 Consider the NLP P2:

WFM(P2) = ∅, L = {¬a, b} is a consequence of P2, and T (P2, L) = GRS(P2, L) = {b}.

Example 5 Consider the DLP P3:

We also provide an algorithm for computing GRS(P,L), when P is a DLP. Given a DLP P, a set X of atoms, and a set L of literals, the operator RSP,L(X) is defined in Algorithm 1. Note that, RSP,L(X) is monotonic. We use RS(P, L) to denote the least fixed points of the corresponding operators.

Algorithm 1: RSP,L(X)

1 A :=X; 2 H := {head(r) \ L- | r ∈ P, head(r) ∩ body+(r) = ∅, 3 X ∩ head(r) = ∅, and X ∪ (L \ L+) |= body(r)}; 4 for each C ∈ H do 5 if |C| = 1 or 6 for each p ∈ C, C ⊆ RSP,L(X ∪ {p}) then 7 A := A ∪ C; 8 return A

Proposition 21 Let P be a DLP and L a consistent set of literals. GRS(P, L) = RS(P, L).

Proof Sketch: The proof is similar to Proposition 18. Additionally with the fact that, if C ̸⊆ RSP,L(X ∪ {p}) for some p ∈ C, then for the set E = C \ {p}, there does not exist a corresponding rule r ∈ R-(E, P), which prevents C ∪ X to be a reliable set of P under L.

Now we compare the reliable set under a consequence of a program with the results computed from the approximation of the well-founded operator. Given a logic program P, we can preprocess P by the grounding engine gringo [Gebser et al., 2007b] (or lparse) and receive the simplified program P ′ . In specific, P ′ is consisted from two parts P ∗ and R, where no atoms in WFM ∗ (P) occurring in P ∗ , R = {p ←| p ∈ WFM ∗ (P)}, and WFM ∗ (P) is an approximation of WFM(P) by gringo. We can compute a consequence of P ∗ by applying unit propagation to the set of clauses obtained from the rules in P ∗ . For example, let P ∗ = {p ∨ q ←, q ← not r, ← r}, the corresponding set of clauses is {p ∨ q, q ∨ r, ¬r}, and the consequence computed by applying unit propagation is {¬r, q}. Notice that both gringo and lparse do not compute the full well-founded model, unit propagation would produce useless consequences for programs that have no answer sets. Then we also characterize the benchmark by the number of programs that have no answer sets. Based on such consequence L, we can compute T(P ∗ ,L). From Proposition 18 and 19, it is equal to GRS(P ∗ , L) if P ∗ is an NLP; it is a subset of GRS(P ∗ , L) if P ∗ is a DLP. In the following, for the program P ′ grounded by gringo, we use GRS∗ to denote such T (P ∗ , L).

We have implemented a program to compute GRS∗ for programs grounded by gringo (version 4.4.0). Table 1 contains average sizes of consequences and GRS∗ of P ∗ for different instances from 3 classes of NLPs and 2 classes of DLPs, and average times for computing these notions 1 .

These benchmarks were frequently used to compare the performance of ASP solvers [Denecker et al., 2009; Gebser et al., 2013]. If a class's name contains "(N)" (resp. "(D)") then instances in the class are NLPs (resp. DLPs). In the table, a number under "#ins" denotes the number of instances in the corresponding class, a number under "#NAS" denotes the number of instances which have no answer sets in the corresponding class and a number under "#WFM" denotes the average number of facts in grounded programs, which is also the size of positive consequence in WFM ∗ (P ′ ).

The result shows that for some programs in benchmarks, GRS∗ is larger than the results computed from the approximation of the well-founded operator. The performance could be improved when a larger consequence is considered. We have also implemented a program for Algorithm 1 to compute GRS(P,L) for DLPs. However the program requires a long running time and returns nothing more than GRS∗ for benchmarks.

6 Conclusions

In this paper, we consider when a consequence of a logic program can be used to simplify a logic program so that the resulting program would no longer contain atoms appearing in the consequence. We introduce notions of the strong and the weak reliable set of a program. We show that a logic program is strongly equivalent to the simplified program if and only if the consequence is a strong reliable set, and they have the same answer sets if and only if the consequence is a weak reliable set. We explore computational complexity on identifying a strong or a weak reliable set and provide an approach to verify a strong reliable set. These notions can provide a guideline to explore classes of consequences that could be used to simplify a logic program. As an example, we introduce the notion of the reliable set under a consequence of a program, which extends the well-founded model and provides a sufficient condition for a consequence to simplify a logic program. We also provide an algorithm to compute the notion. We plan to extend the idea to other notions of equivalence, such as relativized, uniform equivalence, and hyperequivalence, and find out corresponding applications in future.

1 .http://ss.sysu.edu.cn/%7ewh/simplifying.html

7 Acknowledgments

We are grateful to Fangzhen Lin for many helpful and informative discussions. We would also like to thank Xiaoping Chen and his research group for their useful discussions. Jianmin Ji's research was partially supported by the National Natural Science Foundation of China under grant 61175057, the National Natural Science Foundation for the Youth of China under grant 61403359, as well as the USTC Key Direction Project and the USTC 985 Project. Hai Wan thanks Natural Science Foundation of Guangdong Province of China (No. S2012010009836), and Guangzhou Science and Technology Project (No. 2013J4100058) for the support of this research.