Discovering Classes of Strongly Equivalent Logic Programs

1 Introduction

This paper makes two contributions. First, it reports on a successful experiment of computer-aided theorem discovery in logic programming with answer set semantics. Second, it contributes to the theory and practice of logic programming in that the discovered theorems that capture certain classes of strongly equivalent logic programs are new, non-trivial, and lead to new program simplification rules that preserve strong equivalence.

Theorem discovery is a highly creative human process. Generally speaking, we can divide it into two steps: (i) conjecture formulation, and (ii) conjecture verification, and computers can help in both of these two steps. For instance, machine learning tools can be used in the first step, i.e. in coming up with reasonable conjectures, and automated deduction tools can be used in the second step, i.e. in verifying the correctness of these conjectures.

While theorem discovery may make use of learning, these two tasks are fundamentally different. Theorem discovery starts with a theory, and aims at finding interesting consequences of the theory, while learning is mostly about induction, i.e. it starts with examples/consequences, and aims at finding a theory that would explain the given examples/consequences.

∗Our thanks to Yan Zhang for his comments on an earlier version of this paper. This work was supported in part by HK RGC CERG HKUST6170/04E.

Yin Chen

Software Institute Sun Yat-Sen University Guangzhou, China

Using computers to discover theorems is an old aspiration. There have been many success stories. For instance, AM [Lenat, 1979] was reported to be able to come up with some interesting concepts and theorems in number theory, and the remarkable system described in [Petkovsek et al., 1996] automates the discovery and proofs of identities, especially hypergeometric identities involving sums of binomial coefficients that are important for the analyses of algorithms. Yet another example where "interesting" theorems can be discovered almost fully automatically is a recent work by Lin [2004] on discovering state invariants in planning domains. Lin showed that there are ways to classify potentially interesting constraints according to their syntactic properties, and these constraints can be easily enumerated for most domains. Furthermore, for many of these constraints whether they are invariants can be checked automatically. As a result, the system described in [Lin, 2004] could discover many common invariants in planning domains, and for the logistics domain, it could even discover a set of "complete" state invariants.

In this paper, we consider the problem of discovering theorems about strongly equivalent logic programs under answer set semantics.

The notion of strongly equivalent logic programs is interesting for a variety of reasons. For instance, as Lifschitz et al. [2001] noted, if two sets of rules are strongly equivalent, then one can be replaced by the other in any logic program regardless of the context. Thus identifying strongly equivalent sets of rules is a useful exercise that may have applications in program simplification, and the purpose of this paper is to discover conditions under which a set of rules is strongly equivalent to another. It is important that these conditions need to be computationally effective as in general checking if two sets of rules are strongly equivalent is coNP-complete (c.f.[Lin, 2002]).

To discover these conditions, we follow the methodology of [Lin, 2004] by looking at domains of small sizes first. For instance, to discover for what kinds of rules r1 and r2 we have that {r1} is strongly equivalent to {r2}, we consider a language with, say three atoms, and enumerate all possible pairs of rules in this language that are strongly equivalent. We then conjecture a condition that would capture exactly this set of pairs of rules, and then try to verify if this conjecture is true in the general case. In [Lin, 2004], a general theorem is proved to automate the verification part. We try to do the same here by proving some general theorems that will make the verification part easier, almost semi-automatic.

This paper is organized as follows. In the next section, we briefly review the basic concepts of logic programming under answer set semantics. Then in section 3 we state in more precise terms the type of theorems that we want to discover. In section 4 we prove some general theorems that will help us prove these theorems, and in section 5, we describe some of the theorems that we discovered. We then discuss an application to logic program simplification in section 6, and finally we conclude this paper in section 7.

2 Logic programming with answer set semantics

Let L be a propositional language, i.e. a set of atoms. In this paper we shall consider logic programs with rules of the following form:

h1; · · · ; hk ← p1, · · · , pm, not pm+1, · · · , not pn (1) where hi's and pi's are atoms in L. So a logic program here can have default negation (not ), constraints (when k = 0), and disjunctions in the head of its rules. In the following, if r is a rule of the above form, we write Hdr to denote the set {h1, ..., hk}, Psr the set {p1, ..., pm}, and Ngr the set {pm+1, ..., pn}. Thus a rule r can also be written as Hdr ← Psr, notNgr. The semantics of these programs are given by answer sets as defined in [Gelfond and Lifschitz, 1991]. To save space, we do not give the definition here.

Two such logic programs P1 and P2 are said to be equivalent if they have the same answer sets, and strongly equivalent [Lifschitz et al., 2001] (under the language L) if for any logic program P in L, P ∪ P1 and P ∪ P2 are equivalent. For example, {a ← b} and {a ← c} are equivalent, but not strongly equivalent. It can be shown that {a ← not a} and {← not a} are strongly equivalent.

Lifschitz et al. [2001] showed that checking for strong equivalence between two logic programs can be done in the logic of here-and-there, a three-valued non-classical logic somewhere between classical logic and intuitionistic logic. Lin [2002] provided a mapping from logic programs to propositional theories and showed that two logic programs are strongly equivalent iff their corresponding theories in propositional logic are equivalent. This result will be used here both for generating example pairs of strongly equivalent logic programs, and for verifying a conjecture. We repeat it here.

Let P1 and P2 be two finite logic programs, and L the set of atoms in them.

Theorem 1 [Lin, 2002] P1 and P2 are strongly equivalent iff in propositional logic, the following sentence is valid:

where for each p ∈ L, p′ is a new atom, and for each rule r of the form (1), δ(r) is the conjunction of the following two sentences:

Notice that if m = n = 0, then the left sides of the implications in (3) and (4) are considered to be true, and if k = 0, then the right sides of the implications in (3) and (4) are considered to be false.

3 The problem

As we mentioned above, one possible use of the notion of strongly equivalent logic programs is in program simplification. For instance, given a logic program, for each rule r in it, we may ask whether it can be deleted without knowing what other rules are in P, i.e. whether {r} is strongly equivalent to the empty set. Or we may ask whether a rule r in P can be deleted if one knows that another rule r′ is already in P, i.e. whether {r, r′ } is strongly equivalent to {r′ }. In general, we may ask the following k-m-n question: Is {r1, ..., rk, u1, ..., um} strongly equivalent to {r1, ..., rk, v1, ..., vn}? Thus our theorem discovery task is to come up, for a given k-m-n problem, a computationally effective condition that holds if and only if the answer to the k-m-n question is positive.

Now suppose we have such a condition C, and suppose that when {r1, ..., rk, u1, ..., um} is strongly equivalent to {r1, ..., rk, v1, ..., vn}, it is better to replace {u1, ..., um} by {v1, ..., vn} in the presence of r1, ..., rk for the purpose of, say computing the answer sets of a program. One way to use this result to simplify a given program P is to first choose k rules in P, and for any other m rules in it, try to find n rules so that the condition C holds, and then replace the m rules in P by the simpler n rules.

However, even if checking whether C holds would take a negligible constant time, using the above procedure to simplify a given logic program will be practical only when k,m, n are all very small or when k is almost the same as the number of the rules in the given program, and m and n are very small. Thus it seems to us that it is worthwhile to solve the k-m-n problem only when k,m, n are small. In particular, in this paper, we shall concentrate on the 0-1-0 problem (whether a rule can always be deleted), the 0-1-1 problem (whether a rule can always be replaced by another one), the 1-1-0 problem (in the presence of a rule, whether another rule can be deleted), the 2-1-0 problem (in the presence of two rules, whether a rule can always be deleted), and the 0-2-1 problem (if a pair of rules can be replaced by a single rule).

An example of theorems that we want to discover about these problems is as follows:

4 Some General Theorems

In this section, we prove some general theorems that will help us verify whether an assertion like (∗) above is true.

Let L be a propositional language, i.e. a set of atoms. From L, construct a first-order language FL with equality, two unary predicates H1 and H2, three unary predicates Hdr, Psr, and Ngr for each logic program rule r in L (we assume that each rule in L has a unique name), and three unary predicates Xi, Yi, and Zi for each positive number i.

Notice that we have used Hdr, Psr, and Ngr to denote sets of atoms previously, but now we overload them as unary predicates. Naturally, the intended interpretations of these unary predicates are their respective sets.

Definition 1 Given a set L of atoms, an intended model of FL is one whose domain is L, and for each rule r in L, the unary predicates Psr, Hdr, and Ngr are interpreted by their corresponding sets of atoms, Psr, Hdr, and Ngr, respectively.

Conditions on rules in L, such as Psr ∩Ngr ̸= ∅, will be expressed by special sentences called properties in FL.

Definition 2 A sentence of FL is a property about n rules if it is constructed from equality and predicates Xi, Yi, and Zi, 1 ≤ i ≤ n. A property Φ about n rules is true (holds) on a sequence P = [r1, ..., rn] of n rules if Φ[P] is true in an intended model of FL, where Φ[P] is obtained from Φ by replacing each Xi by Hdri , Yi by Psri , and Zi by Ngri .

Notice that since Φ[P] does not mention predicates Xi, Yi, Zi, H1, and H2, if it is true in one intended model, then it is true in all intended models.

As we have mentioned above, we are interested in capturing the strong equivalence between two programs by a computationally effective condition. More specifically, for some small k, m, and n, we are interested in finding a property Φ about k+m+n rules such that for any sequence of k+m+n

are strongly equivalent if and only if Φ is true on P. (5)

We shall now prove some general theorems that can help us verify the above assertion for a class of formulas Φ.

First of all, Theorem 1 can be reformulated in FL as follows by reading H1(p) as "p holds", and H2(p) as "p′ holds":

Theorem 2 P1 and P2 are strongly equivalent in L iff the following sentence

is true in all intended models of FL, where γ(r) is the conjunction of the following two sentences:

In first order logic, if a prenex formula of the form ∃⃗x∀⃗yB is satisfiable, then it is satisfiable in a structure with n elements, where n is the length of ⃗x if it is non-empty, and 1 when ⃗x is empty. We can prove a similar result for our firstorder languages and their intended models here.

From this and Theorem 2, we can show the following theorem which will enable us to automate the verification of the "if" part of (5) when the property Φ is in the prenex format.

Theorem 3 Without loss of generality, suppose m ≥ n. If Φ is a property about k+m+n rules of the form ∃⃗x∀⃗yQ, where ⃗x is a tuple of w variables, and Q a formula that does not have any quantifiers, then the following two assertions are equivalent:

• (a) For any sequence of k+m+n rules, P = [r1, ..., rk, u1, ..., um, v1, ..., vn], if Φ is true on P, then {r1, ..., rk, u1, ..., um} is strongly equivalent to {r1, ..., rk, v1, ..., vn}.
• (b) (b.1) If n > 0, then for any sequence P = [r1, ..., rk, u1, ..., um, v1, ..., vn] of rules with at most w + 2(k + m) atoms, if Φ is true on P, then {r1, ..., rk, u1, ..., um} is strongly equivalent to {r1, ..., rk, v1, ..., vn}.
• (b.2) If n = 0, then for any sequence P = [r1, ..., rk, u1, ..., um] of rules with at most K atoms, if Φ is true on P, then {r1, ..., rk, u1, ..., um} is strongly equivalent to {r1, ..., rk}, where K is w+2k if w+2k > 0, and K = 1 otherwise.

The "only if" part of (5) can often be proved with the help of the following theorem.

Theorem 4 Let L1 and L2 be two languages, and f a function from L1 to L2. If P1 and P2 are two programs in L1 that are strongly equivalent, then f(P1) and f(P2) are two programs in L2 that are also strongly equivalent. Here f(P) is obtained from P by replacing each atom p in it by f(p).

Proof: By Theorem 1 and the fact that in propositional logic, if ϕ is a tautology, and f a function from L1 to L2, then f(ϕ) is also a tautology, where f(ϕ) is the formula obtained from ϕ by replacing each atom p in it by f(p).

For an example of using the theorems in this section for proving assertions of the form (5), see Section 5.1.

5 Computer aided theorem discovery

Given a k-m-n problem, our strategy for discovering theorems about it is as follows:

1. Choose a small language L;
2. Generate all possible triples

of sets of rules in L such that {r1, ..., rk, u1, ..., um} is strongly equivalent to {r1, ..., rk, v1, ..., vn} in L;

1. Formulate a conjecture on the k-m-n problem that holds in the language L, i.e. a condition that is true for a triple of the form (9) iff it is generated in Step 2;
2. Verify the correctness of this conjecture in the general case.

This process may have to be iterated. For instance, a conjecture came up at Step 3 may fail to generalize in Step 4, so the whole process has to be repeated. Or we may start with a language L with, say three atoms but have to increase it to five or six atoms later on.

Ideally, we would like this process to be automatic. However, it is difficult to automate Steps 3 and 4 - the number of possible patterns that we need to examine in order to come up with a good conjecture in Step 3 is huge, and we do not have a general theorem that enables us to automate the verification part in Step 4: while Theorem 3 enables us to automate the proof of the sufficient part of the assertion (5) for a class of formulas Φ, we do not have a similar result for the necessary part. Theorem 4 helps, but it is not fully automatic yet. Nonetheless, computers play a crucial role in all steps, and in the following we report some of the theorems discovered using the above procedure.

5.1 The 0-1-0 problem

This problem asks if a given rule is strongly equivalent to the empty set, thus can always be deleted from any program. We have the following experimental result:

Lemma 1 If a rule r mentions at most three distinct atoms, then {r} is strongly equivalent to ∅ iff (Hdr∪Ngr)∩Psr ̸= ∅. Using Theorem 4, we can show the following result:

Lemma 2 If there is a rule r of the form (1) such that {r} is strongly equivalent to ∅ and (Hdr ∪ Ngr) ∩ Psr ̸= ∅ is not true, then there is such a rule that mentions at most three atoms.

Proof: Suppose {r} is strongly equivalent to ∅, Hdr ∩Psr = ∅, and Psr ∩ Ngr = ∅. Suppose L is the set of atoms in r, and a, b, c are three new atoms. Let

By Theorem 4, {f(r)} is also strongly equivalent to ∅. By the construction of f , we also have Hdf(r) ∩ Psf(r) = ∅, and Psf(r) ∩ Ngf(r) = ∅, and that f(r) mentions at most three distinct atoms.

Theorem 5 (The 0-1-0 problem) Lemma 1 holds in the general case, i.e. without any restriction on the number of atoms in r.

Proof: We notice that the condition in Lemma 1, (Hdr ∪ Ngr) ∩ Psr ̸= ∅, is equivalent to the following property

being true on [r]. Thus the "if" part follows from Theorem 3 and Lemma 1. The "only if" part follows from Lemma 1 and Lemma 2.

The "if" part of the theorem is already well-known, first proved by Osorio et. al. [2001]. To the best of our knowledge, the "only if" part is new.

We notice here that there is no need to consider the 0-n-0 problem for n > 1, because for any n, {r1, ..., rn} is strongly equivalent to ∅ iff for each 1 ≤ i ≤ n, {ri} is strongly equivalent to ∅.

5.2 The 1-1-0 and the 0-1-1 problems

The 1-1-0 problem asks if a rule can always be deleted in the presence of another rule, and the 0-1-1 problem asks if a rule can always be replaced by another one. We first solve the 1-1-0 problem, and the solution to the 0-1-1 problem will come as a corollary.

We have the following experimental result for the 1-1-0 problem:

Lemma 3 For any two rules r1 and r2 that mentions at most three atoms, {r1, r2} and {r1} are strongly equivalent iff one of the following two conditions is true:

1. {r2} is strongly equivalent to ∅.

Lemma 4 If there are two rules r1 and r2 such that {r1, r2} and {r2} are strongly equivalent, but none of the two conditions in Lemma 3 hold, then there are two such rules that mention at most three atoms.

Theorem 6 (The 1-1-0 problem) Lemma 3 holds in the general case, without any restriction on the number of atoms in r1 and r2.

Proof: The condition in Lemma 3 is equivalent to the following property

being true on [r1, r2]. Thus the "if" part follows from Theorem 3 and Lemma 3, by noticing that the above property can be written as ∃x∀⃗y.Q as required by Theorem 3. The "only if" part follows from Lemma 3 and Lemma 4.

Thus if a rule r2 cannot be deleted on its own but can be deleted in the presence of another rule r1, then it must be the case that r2 is redundant given r1: if the body of r2 is satisfied, then the body of r1 is satisfied as well; furthermore, r2 can entail no more than what can be entailed by r1 (Hdr1 ⊆ Hdr2 ∪Ngr2 ).

Osorio et al. [2001] proved that {r1, r2} and {r1} are strongly equivalent if either Psr1 ∪ Ngr1 = ∅ and Hdr1 ⊆ Ngr2 or Psr1 ⊆ Psr2 , Ngr1 ⊆ Ngr2 , and Hdr1 ⊆ Hdr2 . More recently, Eiter et al. [2004] showed that {r1, r2} and {r1} are strongly equivalent if r1 s-implies r2 [Wang and Zhou, 2005], i.e. if there exists a set A ⊆ Ngr2 such that Hdr1 ⊆ Hdr2 ∪ A, Ngr1 ⊆ Ngr2 \ A, and Psr1 ⊆ Psr2 .

As one can see, these are all special cases of the "if" part of Theorem 6. Our result is actually more general. For instance, these special cases do not apply to {(c ← b, not c), (← b, not c)} and {c ← b, not c}, but one can easily show that these two sets are strongly equivalent using our theorem.

From our solution to the 1-1-0 problem, we can derive a solution to the 0-1-1 problem.

Theorem 7 (The 0-1-1 problem) For any two rules r1 and r2, {r1} and {r2} are strongly equivalent iff one of the following two conditions is true:

1. {r1} and {r2} are both strongly equivalent to ∅.

Proof: By Theorem 1, it is easy to see that {r1} and {r2} are strongly equivalent iff {r1, r2} and {r1} are strongly equivalent and {r1, r2} and {r2} are strongly equivalent.

Thus two rules r1 and r2 can always be interchanged if either both of them can be deleted (strongly equivalent to the empty set) or they have the same body, and the same consequences when the body is true. For instance, {a ← B, not a} and {← B, not a} are strongly equivalent no matter what B is, because the two rules have the same body, and when the body is true, the same consequence - a contradiction. As another example, {a; b ← not a} and {b ← not a} are strongly equivalent because the two rules have the same body, and, when the body is true, the same consequence, b.

5.3 The 2-1-0, 0-2-1, and 0-2-2 problems

The 2-1-0 problem asks if a rule can be deleted in the presence of another two rules, the 0-2-1 problem asks if two rules can be replaced by a single rule, and the 0-2-2 problem asks if two rules can be replaced by another two rules. Similar to the previous subsection, the solution to the 0-2-1 and 0-2-2 problems will follow from a solution to the 2-1-0 problem.

We have the following experimental result for the 2-1-0 problem:

Lemma 5 For any three rules r1, r2 and r3 that mentions at most six atoms, {r1, r2, r3} and {r1, r2} are strongly equivalent iff one of the following four conditions is true:

1. {r3} is strongly equivalent to ∅.
2. {r1, r3} is strongly equivalent to {r1}.
3. {r2, r3} is strongly equivalent to {r2}.
4. There is an atom p such that:
5. p ∈ (Psr1 ∪Psr2 )∩(Hdr1 ∪Hdr2 ∪Ngr1 ∪Ngr2 )
6. Hdri \ {p} ⊆ Hdr3 ∪Ngr3 and Psri \ {p} ⊆ Psr3 and Ngri \ {p} ⊆ Ngr3 , where i = 1, 2
7. If p ∈ Psr1 ∩Ngr2 , then Hdr1 ∩Hdr3 = ∅
8. If p ∈ Psr2 ∩Ngr1 , then Hdr2 ∩Hdr3 = ∅

Notice that in principle, given a language L, every subset of L can be the Hd, Ps, or Ng of a rule. Thus when the size of L is six, there are in principle (26 )3 - 1 = 262, 143 possible rules, and 262, 1433 triples of them. Thus at first glance, it seems that verifying Lemma 5 experimentally using the currently available computers would be impossible. However, we can cut the numbers down significantly with the results that we already have proved. First, we only have to consider rules that do not have common elements in Hd, Ps, and Ng: if either Hd and Ps or Ps and Ng have a common element, then by Theorem 5, this rule can be deleted; if Hd and Ng have common elements, then according to Theorem 7, we obtain a strongly equivalent rule by deleting the common elements in Hd. Second, we do not have to consider isomorphic rules: if there is a one-to-one onto function from L to L that maps {r1, r2, r3} to {r′1 , r′2 , r′3 }, then these two sets of rules are essentially the same except for the names of atoms in them. By using a certain normal form for triples of rules that avoids these redundant cases, we ended up with roughly 120 million triples of rules to consider for testing Lemma 5, which took about 10 hours on a Solaris server consisting of 8 Sun Ultra-SPARC III 900Mhz CPUs with 8GB RAM.

The following lemma is the reason why we need to consider a language with six atoms for this problem.

Lemma 6 If there are three rules r1,r2 and r3 such that {r1, r2, r3} and {r1, r2} are strongly equivalent, but none of the four conditions in Lemma 5 hold, then there are three such rules that mention at most six atoms.

Theorem 8 (The 2-1-0 problem) Lemma 5 holds in the general case, without any restriction on the number of atoms in r1, r2, r3.

The conditions in Lemma 5 (Theorem 8) are rather complex, and the reason why it is difficult to automate Step 3 of the procedure at the beginning of the section. These conditions capture all possible cases when r3 is "subsumed" by r1 and r2, and are difficult to describe concisely by words. We give some examples.

Consider the following three rules: r1: (a2 ← a1), r2: (a3 ← not a1), and r3: (a3 ← not a2). We have that {r1, r2, r3} and {r1, r2} are strongly equivalent because the condition (4) in Lemma 5 holds.

However, if we change r3 into r′3 : a2 ← not a3, then P1 = {r1, r2, r′3 } and P2 = {r1, r2} are not strongly equivalent: one could check that condition (4.3) in Lemma 5 does not hold, and indeed, while P2 ∪ {a1 ← a2} has a unique answer set {a3}, P1 ∪ {a1 ← a2} has two answer sets {a3} and {a1, a2}.

It is also easy to show by Theorem 8 that a3 ← not a2 is "subsumed" by {(a1; a2; a3 ←), (a2; a3 ← a1)}, and a2; a3 ← is "subsumed" by {(a2 ← a1), (a3 ← not a1)}.

With the results that we have, the following theorem will yield a solution to the 0-2-1 problem.

Theorem 9 (the 0-2-1 problem) For any three rules r1, r2 and r3, {r1, r2} and {r3} are strongly equivalent iff the following three conditions are true:

1. {r1, r2, r3} and {r1, r2} are strongly equivalent.
2. {r1, r3} and {r3} are strongly equivalent.
3. {r2, r3} and {r3} are strongly equivalent.

For example, {(a2 ← a1, not a3), (a1; a2 ← not a3)} is strongly equivalent to {a2 ← not a3}. While {(← a2, a3), (← a3, not a2)} is strongly equivalent to {← a3}, {(a1 ← a2, a3), (a1 ← a3, not a2)} is not strongly equivalent to {a1 ← a3}. Similarly, we have the following theorem

Theorem 10 (the 0-2-2 problem) For any four rules r1, r2, r3, r4, {r1, r2} and {r3, r4} are strongly equivalent iff the following four conditions are true:

1. {r1, r2, r3} and {r1, r2} are strongly equivalent.
2. {r1, r2, r4} and {r1, r2} are strongly equivalent.
3. {r3, r4, r1} and {r3, r4} are strongly equivalent.
4. {r3, r4, r2} and {r3, r4} are strongly equivalent.

6 Program simplification

We have mentioned that one possible use of the notion of strongly equivalent logic programs is in simplifying logic programs: if P and Q are strongly equivalent, and that Q is "simpler" than P, we can then replace P in any program that contains it by Q.

Most answer set programming systems perform some program simplifications. However, only Smodels [Niemel¨ a et al., 2000] has a stand-alone front-end called lparse that can be used to ground and simplify a given logic program. It seems that lparse simplifies a grounded logic program by computing first its well-founded model. It does not, however, perform any program simplification using the notion of strong equivalence. For instance, lparse-1.0.13, the current version of lparse, did nothing to the following set of rules: {(a ← not b), (b ← not a), (a ← a)}. Nor does it replace the first rule in the following program {(a ← not a), (a ← not b), (b ← not a)} by the constraint ← not a.

It is unlikely that anyone would be intentionally writing rules like a ← a or b ← a, not a. But these type of rules can arise as a result of grounding some rules with variables. For instance, the following is a typical recursive rule used in logic programming encoding of the Hamiltonian Circuit problem [Niemel¨ a, 1999; Marek and Truszczynski, 1999]:

When instantiated on a graph with cyclic arcs like arc(a, a), this rule generates cyclic rules of the form reached(X) ← hc(X,X), reached(X). Unless deleted explicitly, these rules will slow down many systems, especially those based on SAT.

It is thus useful to consider using the results that we have here for program simplification. Indeed, transformation rules such as deleting those that contain common elements in their heads and positive bodies have been proposed [Brass and Dix, 1999], and studied from the perspective of strong equivalence [Osorio et al., 2001; Eiter et al., 2004]. Our results add new such transformation rules. For instance, by Theorem 7, we can delete those elements in the head of a rule that also appear in the negation-as-failure part of the rule. Theorems 6, 8, and 9 can also be used to define some new transformation rules.

7 Concluding remarks and future work

Donald Knuth, in his Forward to [Petkovsek et al., 1996], said

"Science is what we understand well enough to explain to a computer. Art is everything else we do. ...Science advances whenever an Art becomes a Science. And the state of the Art advances too, because people always leap into new territory once they have understood more about the old."

We hope that with this work, we are one step closer to making discovering classes of strongly equivalent logic programs a Science.

We have mentioned that the methodology used in this paper is similar to that in [Lin, 2004]. In both cases, plausible conjectures are generated by testing them in domains of small sizes, and general theorems are proved to aid the verification of these conjectures in the general case. However, while plausible conjectures are generated automatically in [Lin, 2004], they are done manually here. While the verifications of most conjectures in [Lin, 2004] are done automatically as well, they are done only semi-automatically here. Overcoming these two weaknesses is the focus of our future work. Specifically, we would like to make Step 3 of the procedure in Section 5 automatic, and prove a theorem similar to Theorem 3 to automate the proofs of the "only if" parts of theorems like Theorems 5 - 8, in the same way that Theorem 3 makes the proofs of the "if" parts of these theorems automatic. This way, we would be able to discover more interesting theorems in this area, and more easily!