Computing Stable Models by Program Transformation

Jürgen Stuber

MPI–I–93–257 December 1993 Author’s Address

Jürgen Stuber, Max-Planck-Institut für Informatik, Im Stadtwald, D-66123 Saarbrücken, Ger-

many, juergen@mpi-sb.mpg.de

Acknowledgements

The research described in this report was supported by the German Ministry for Research and Technology (Bundesministerium für Forschung und Technologie) under grant ITS 9103.

Abstract

In analogy to the Davis-Putnam procedure we develop a new procedure for computing stable models of propositional normal disjunctive logic programs, using case analysis and simplification. Our procedure enumerates all stable models without repetition and without the need for a minimality check. Since it is not necessary to store the set of stable models explicitly, the procedure runs in polynomial space.

We allow clauses with empty heads, in order to represent truth or falsity of a proposition as a one-literal clause. In particular, a clause of form ∼ A → expresses that A is constrained to be true, without providing a justification for A. Adding this clause to a program restricts its stable models to those containing A, without introducing new stable models. Together with A → this provides the basis for case analysis.

We present our procedure as a set of rules which transform a program into a set of solved forms, which resembles the standard method for presenting unification algorithms. Rules are sound in the sense that they preserve the set of stable models. A subset of the rules is shown to be complete in the sense that for each stable model a solved form can be obtained. The method allows for concise presentation, flexible choice of a control strategy and simple correctness proofs.

Keywords

Stable semantics, stable models, normal disjunctive logic program, normal deductive database, default negation, negation-as-failure, Davis-Putnam.

1 Introduction

Stable models have been introduced by Gelfond and Lifschitz (1988) as a semantics for logic programs. Most methods build stable models bottom-up, using clauses in the forward direction. For clauses whose premises are satisfied in a partially built interpretation, one proposition of the head is made true, which requires a case split for disjunctive clauses. The propositions of the negative premises are recorded to be false, either by collecting them in a separate set or by adding special literals to the interpretation. An interpretation is discarded if an inconsistency is detected. Saccà and Zaniolo (1990) give a procedure which finds a single stable model of a normal non-disjunctive program. Nevertheless it can easily be modified to allow enumerating all stable models. However, because clauses with independent assumptions may be considered in any order, a stable model may be generated many times. Fernández and Minker (1992) and Inoue, Koshimura and Hasegawa (1992) compute stable models of normal disjunctive programs. To cope with disjunction they explicitly store sets of models in order to test for minimality, which may require exponential space in the worst case. Eshghi (1990) uses the Assumption-based Truth Maintenance System (ATMS) for computing stable models of non-disjunctive programs. It starts with inconsistent assumptions and relaxes them until stable models are reached. Its representation of minimal sets of inconsistent assumptions (nogoods) and minimal sets of assumptions needed to derive a certain proposition (environments) may also require exponential space in the worst case.

We present a new procedure which computes the stable models of a normal disjunctive logic program (a normal deductive database). For infinite Herbrand bases the problem is known to be infeasible in general. There may exists continuum many stable models, and the problem of deciding whether a recursively enumerable interpretation is a stable model is Π_{2}^{0}-hard (Marek and Subrahmanian 1992). Therefore we limit ourselves to the finite case, like all other currently known methods for computing stable models. This still includes the practically important case of datalog programs.

Our procedure uses case analysis with respect to the truth-value of propositions, in analogy to Davis and Putnam (1960). This enables it to enumerate the stable models for finite propositional normal disjunctive logic programs without repetitions and without the need to explicitly test for minimality. Rather than testing afterwards, we take care to preserve minimality during computation. Each model is generated only once because cases do not overlap.

Eiter and Gottlob (1993) have shown that the problem of deciding whether a stable model exists is Σ_{2}-complete in the polynomial hierarchy. Our procedure reflects this result; it uses nondeterministic polynomial time, and the disjunction rule uses co-SAT from co-NP as an oracle.

Our procedure tries to transform a normal disjunctive logic program into sets of clauses in solved form which for each proposition contain exactly one of the clauses A → or → A.^{1} This makes determining its stable model trivial. One-literal clauses play a special role in our procedure, since they are used to represent truth or falsity of a proposition, as specified by the following table.

A →  A is false
→ A  A is true and justified
∼ A → A is true but not justified

A true but unjustified proposition acts as a constraint; it does not help in the construction of a stable model, but is used to check the truth of A after the model has been constructed. Operationally, if A → is ever added to a program containing ∼ A →, an inconsistency results. A → or → A are used to simplify the program, removing all other occurrences of A. With ∼ A → we may remove clauses containing ∼ A—these are subsumed—and we may reduce positive premises A from clauses with an empty head. Other simplifications are not possible because we have to be careful not to add unwarranted justification for A. Another use of ∼ A → is to block case analysis on A, since then its truth-value is already known. The basis for case analysis is the observation that adding alternatively A → or ∼ A → to a program P splits its set of stable models exactly into the two sets of stable models of the new programs. One contains all stable models of P where A is false while the other contains those where A is true.

1Note that we allow clauses with empty heads.

Case analysis and simplification are sufficient to compute all stable models of non-disjunctive programs. For disjunctive programs only a very restricted case remains open, where the constraints specify exactly one possible stable model. It suffices to test whether the disjunctions provide justification for all propositions constrained to true. To this end it is necessary to prove the validity of certain classical implications. Any procedure for tautology checking in classical propositional logic may be employed, for instance classical Davis-Putnam.

We prove the soundness of some other rules which are not needed for completeness but which may speed up the computation, namely Tautology elimination, Factoring and Default negation. Default negation corresponds to the Purity rule of the classical Davis-Putnam procedure for the case of propositions which don’t appear positively. It is our only nonmonotonic rule.

For programs without a stable model Inoue et al. (1992) distinguish between inconsistent and incoherent programs. Incoherent programs are those which do not allow to derive an inconsistency, but which have no stable model for lack of justification. Suppose we do not use the Default negation rule. Then an incoherent program is transformed into at least one program which is reduced with respect to our rules, not solved and does not contain the empty clause. The distinction between solved forms and reduced incoherent programs will then be the only source of nonmonotonicity. If incremental computation is desired, one may store these reduced incoherent programs and resume the computation when new clauses are added.

We present our procedure as a set of rules which transform a program into a set of solved forms, which resembles the standard method for presenting unification algorithms. Rules are sound in the sense that they preserve the set of stable models. Subsets of the rules are shown to be complete for non-disjunctive and disjunctive programs, in the sense that for each stable model a solved form can be obtained. This presentation has several advantages. Soundness, termination and completeness can be proven with relative ease. It is made precise which transformations are necessary to achieve completeness, while more sound transformation may be used where appropriate. Any inference system between these boundaries is sound and complete. We also make precise which choices can be made eagerly, and where alternative cases have to be considered.

2 Preliminaries

⊎ denotes disjoint union. We assume a fixed set of propositions Prop. A (normal disjunctive) clause C is a triple ⟨Prem^{+}(C), Prem^{∼}(C), Concl(C)⟩ of sets of propositions Prem^{+}(C) = {A_{1}, …, A_{n}}, Prem^{∼}(C) = {B_{1}, …, B_{m}} and Concl(C) = {D_{1}, …, D_{k}}, which is written

A_{1}, …, A_{n}, ∼ B_{1}, …, ∼ B_{m} → D_{1}, …, D_{k}.

Given Γ = A_{1}, …, A_{n} we write ∼ ·Γ for ∼ A_{1}, …, ∼ A_{n}. A clause C is non-disjunctive if k ≤ 1 and negation-free if m = 0. A (normal disjunctive logic) program is a set of clauses. A program is non-disjunctive if all its clauses are non-disjunctive. We write Prog for the set of programs, and NProg for the set of non-disjunctive programs.

An interpretation I is a set of propositions. I satisfies a negation-free clause C, written I ⊧ C, iff Prem^{+}(C) ⊈ I or Concl(C) ∩ I ≠ ∅. I satisfies a negation-free program P, written I ⊧ P, iff it satisfies all clauses in P. In this case we also say that I is a model of P. The set of models of P is denoted by Mod(P). P′ is a logical consequence of P, written P ⊧ P′, if Mod(P) ⊆ Mod(P′). An I ∈ Mod(P) is minimal if there exists no J ∈ Mod(P) such that J is a proper subset of I. Min(P) denotes the set of minimal models of a program P. For a program P let P̃ be the program where each literal ∼ A is replaced by a new proposition Ã. Analogously define C̃ for a clause C. Let P̃rop = { Ã | A ∈ Prop }.

Gelfond and Lifschitz (1988) define a transformation on logic programs which eliminates all literals ∼ A from a program P based on an interpretation I, where ∼ A is treated as true if A is not in I. For an interpretation I, a clause C and a program P let

GL_{I}(C) = \{ \begin{matrix}\{Prem^{+}(C) → Concl(C)\} & if Prem^{∼}(C) ∩ I = ∅ \\ ∅ & otherwise \end{matrix}
GL_{I}(P) = ⋃_{C∈P} GL_{I}(C)

If GL_{I}(C) = ∅ we say GL_{I} eliminates C. GL_{I}(P) is called the Gelfond-Lifschitz transformation of P with respect to I. An interpretation I is called a stable model of P if I is a minimal model of GL_{I}(P). We write Stab(P) for the set of stable models of P. If we restrict this to the case of non-disjunctive clauses we get the original notion of stable model as defined by Gelfond and Lifschitz (1988).

3 Transformation rules

To describe our procedure we will use transformation rules on programs. They allow to take whole program into account, which is necessary to make nonmonotonic inferences. A program will be transformed into a set of solved forms, which correspond to the programs stable models.

A program P is in solved form if it consists of clauses of form A → or → A with exactly one clause for each proposition A. For a program P in solved form we define the corresponding interpretation I_{P} as { A | → A ∈ P }. On the other hand an interpretation I corresponds to the program in solved form P_{I} = { → A | A ∈ I } ∪ { A → | A ∈ Prop − I }.

Lemma 3.1 Let P be a program. If P is in solved form then Stab(P) = {I_{P} }.

A transformation relation is a subset ⊢ of Prog × Prog. We write ⊢^{∗} for its reflexivetransitive closure. A transformation rule r is a set of instances ρ = \frac{P}{P_{1}|...|P_{n}}. An instance ρ defines a transformation relation ⊢_{ρ} where P ⊢_{ρ} P′ if ρ = \frac{P}{...|P′|...}. To a rule r the associated transformation relation is ⊢_{r}= ⋃_{ρ∈r} ⊢_{ρ}. Similarly, for a set of rules R we define ⊢_{R}= ⋃_{r∈R} ⊢_{r}. We also say ρ is an instance of R.^{2} We say P is R-reduced if there exists no P′ such that P ⊢_{R} P′.

2We do this two-step construction, since we want to keep track which instances belong to the same rule, without specifying formally how to instantiate the schemas defining rules.

A strategy ⊢_{S} for R is a subrelation of ⊢_{R} such that if P is not R-reduced then (⊢_{ρ}) ⊆ (⊢_{S}) for some instance ρ of R. I.e., it is sufficient to eagerly apply some arbitrarily chosen rule. Rules with more than one conclusion encode the control information that several alternatives must be considered, either by backtracking or in parallel.

Let ⊢ be a transformation relation, R a set of transformation rules and P a class of logic programs. ⊢ is sound if P ⊢ P′ implies Stab(P) = ⋃_{P ⊢P′} Stab(P′). ⊢ is complete with respect to P if Stab(P) = { I_{P′} | P ⊢^{∗} P′ and P′ is in solved form } for all P in P. ⊢ is terminating if there exists no infinite sequence P_{0} ⊢ P_{1} ⊢ P_{2} ⊢ …. ⊢ preserves P if P ∈ P and P ⊢ P′ implies P′ ∈ P. R preserves P if ⊢_{R} preserves P. R is sound, terminating or complete if every strategy for R is sound, terminating or complete, respectively. A set of transformation rules R is independent with respect to P if there is no proper subset R′ of R such that R′ is complete with respect to P.

Lemma 3.2 Let R be a set of transformation rules.

1. If ⊢_{r} is sound for all r in R then ⊢_{R} is sound.

2. R is sound if and only if ⊢_{ρ} is sound for all instances ρ of R.

Proof: (1) If ⊢_{r} is sound for all r in R then Stab(P) = ⋃_{P ⊢_{r}P′} Stab(P′) for all r in R, and thus ⋃_{P ⊢_{R}P′} Stab(P′) = ⋃_{r∈R} ⋃_{P ⊢_{r}P′} Stab(P′) = ⋃_{r∈R} Stab(P) = Stab(P).

(2) Suppose ⊢_{r} is sound for all r in R, then ⊢_{R} is sound by (1). By definition P ⊢_{S} P′ implies P ⊢_{R} P′. Hence ⋃_{P ⊢_{S}P′} Stab(P′) ⊆ ⋃_{P ⊢_{R}P′} Stab(P′) = Stab(P). On the other hand, { P′ | P ⊢_{ρ} P′ } ⊆ { P′ | P′ ⊢_{S} P′ } for some instance ρ of R, and thus Stab(P) = ⋃_{P ⊢_{ρ}P′} Stab(P′) ⊆ ⋃_{P ⊢_{S}P′} Stab(P′).

For the converse, assume that R is sound, but ⊢_{ρ} is not sound for some instance ρ = \frac{P}{P_{1}|...|P_{n}} of R. Then Stab(P) ≠ ⋃_{1≤i≤n} Stab(P_{i}). We may choose ⊢_{S} such that P ⊢_{S} P′ iff P ⊢_{r} P′, which makes ⊢_{S} unsound. □

4 Sound program transformations

We first state the soundness of some general program transformation rules. Later we will use this to show soundness of the specific transformation rules of our procedure for computing stable models.

We call clauses of form A, Γ → A, Δ standard tautologies and clauses of form A, ∼ A, Γ → Δ constraint tautologies. Tautologies are always satisfied and do not contribute to the meaning of a program. We may remove tautologies.

Tautology elimination  \frac{\{C\} ⊎ P}{P}  if C is a tautology.

We have two different inference rules for resolution. We may resolve a negative literal either with a positive or a constraint literal. In the latter case a first approach might be the following inference rule.

Naïve constraint resolution \frac{∼ A, Γ → Δ  A, Λ → Π}{Γ, Λ → Δ, Π}

But with this rule it is possible to create new justification for the propositions in Π. The simplest example is the program P = {∼ p →; p → p}, which has no stable model. Naïve constraint resolution would add the clause → p, which leads to the stable model {p}. Therefore we will adopt the following inference rules for resolution.

Standard resolution  \frac{Γ → Δ, A  A, Λ → Π}{Γ, Λ → Δ, Π}

Constraint resolution  \frac{∼ A, Γ → Δ  A, Λ → Π}{Γ, Λ, ∼ ·Π → Δ}

The conclusion of such a resolution inference is called a resolvent of the premises. We may add resolvents.

Resolution  \frac{P}{\{C\} ∪ P}  if C is a resolvent of two clauses in P.

Subsumption is useful to remove clauses which are already implied by the program, in order to reduce the size of the program. Moreover, we will use it to explicitly remove clauses which are satisfied. Note the interaction between positive and constraint literals. In particular, → A subsumes ∼ A →. A clause C′ subsumes a clause C if Prem^{+}(C′) ⊆ Prem^{+}(C), Prem^{∼}(C′) ⊆ Prem^{∼}(C) and Concl(C′) ⊆ Concl(C) ∪ Prem^{∼}(C). We may remove subsumed clauses.

Subsumption  \frac{\{C, C′\} ⊎ P}{\{C′\} ⊎ P}  if C′ subsumes C.

A clause ∼ A, Γ → Δ is called a factor of ∼ A, Γ → A, Δ. Note that a proposition cannot appear twice in the same role in a clause, since for each clause the positive premises, the negative premises and the conclusions form sets. Hence we do not need other factoring rules.

Factoring  \frac{P}{\{C\} ∪ P}  if C is a factor of a clause in P.

We can explain the effect of a clause with negative loop like ∼ p → p by observing that it can be factored to ∼ p →. Hence it constrains p to be true. The classical Davis-Putnam procedure has a Purity-rule, which stipulates a propositions to be true if it only appears in positive positions and false if it only appears in negative positions. Since we need to preserve minimality, we can only do the latter here. In fact, if a proposition does not appear in any head of a clause it cannot be true in a stable model.

Default negation  \frac{P}{\{A →\} ∪ P}  if no head of a clause in P contains A.

In contrast to the other rules in this section, Split is not an equivalence transformation on programs, but generates two programs whose combined semantics is equivalent to the original. The two cases correspond to A being either true or false.

Split  \frac{P}{\{A →\} ⊎ P | \{∼ A →\} ⊎ P}

Unlike in the classical Davis-Putnam procedure, case analysis is not sufficient to cope with disjunctive programs in the case of stable semantics. We can remove all false disjuncts by resolution with the negative fact A →, but if in a minimal model more than one disjunct is true the constraint ∼ A → is too weak to remove the disjunction.

Disjunction  \frac{\{→ A_{1}, …, A_{n}\} ⊎ P}{\{→ A_{1}; …; → A_{n}; → A_{1}, …, A_{n}\} ∪ P}

if n ≥ 2 and P̃ ∪ {→ A_{1}, …, A_{n}} ⊧ {→ A_{1}; …; → A_{n}}.

Disjunction factors out the problem, enabling us to apply any suitable method to it. For instance, we may check if P̃ ∪ {→ A_{1}, …, A_{n}} ∪ {A_{1}, …, A_{n} →} is inconsistent by using a classical Davis-Putnam procedure.

Theorem 4.1 Tautology elimination, Resolution, Subsumption, Factoring, Default negation, Split and Disjunction are sound transformation rules.

For the proof of this theorem we refer the reader to the appendix.

5 The Davis-Putnam procedure

Factoring, Disjunction and certain Resolution transformations add clauses which subsume a clause in their premise. We may remove this clause by subsumption. In combination this yields simplification rules which decrease the size of the program. Moreover, we will also use Tautology elimination and Subsumption for simplification, and in particular subsumption with respect to one-literal clauses, as this can be implemented most efficiently.

Split, Disjunction, Default negation and Constraint propagation add one-literal clauses, thereby decreasing the number of propositions whose truth value is unknown. When proving termination, we will give this decrease precedence over the increase in size. Also, the increase in size is at most linear in the number of propositions. We call a proposition A unknown in P if it doesn’t appear in a one-literal clause in P.

Subsumption-true (SubT)  \frac{\{Γ → Δ, A; → A\} ⊎ P}{\{→ A\} ⊎ P}

Subsumption-false (SubF)  \frac{\{Γ, A → Δ; A →\} ⊎ P}{\{A →\} ⊎ P}

Subsumption-constraint (SubC) \frac{\{Γ, ∼ A → Δ; ∼ A →\} ⊎ P}{\{∼ A →\} ⊎ P}

GL-Subsumption (SubGL)  \frac{\{Γ, ∼ A → Δ; → A\} ⊎ P}{\{→ A\} ⊎ P}

Reduction-true (RedT)  \frac{\{Γ, A → Δ; → A\} ⊎ P}{\{Γ → Δ\} ∪ \{→ A\} ∪ P}

Reduction-false (RedF)  \frac{\{Γ → Δ, A; A →\} ⊎ P}{\{Γ → Δ\} ∪ \{A →\} ∪ P}

Reduction-constraint (RedC)  \frac{\{Γ, A →; ∼ A →\} ⊎ P}{\{Γ →\} ∪ \{∼ A →\} ∪ P}

GL-Reduction (RedGL)  \frac{\{Γ, ∼ A → Δ; A →\} ⊎ P}{\{Γ → Δ\} ∪ \{A →\} ∪ P}

Split (Split)  \frac{P}{\{A →\} ⊎ P | \{∼ A →\} ⊎ P}

if A is unknown in P.

Disjunction (Disj)  \frac{\{→ A_{1}, …, A_{n}\} ⊎ P}{\{→ A_{1}; …; → A_{n}\} ∪ P}

if n ≥ 2, for some 1 ≤ i ≤ n neither A_{i} → nor → A_{i} is in P and P̃∪{→ A_{1}, …, A_{n}} ⊧ {→ A_{1}; …; → A_{n}}.

Constraint propagation (CP)  \frac{\{A_{1}, …, A_{n} → B; ∼ A_{1} →; …; ∼ A_{n} →\} ⊎ P}{\{∼ B →; A_{1}, …, A_{n} → B; ∼ A_{1} →; …; ∼ A_{n} →\} ⊎ P}

if B is unknown in P.

Default negation (DN)  \frac{P}{\{A →\} ⊎ P}

if P contains no clause of form Γ → Δ, A and A → is not already in P.

Tautology elimination (TE)  \frac{\{C\} ⊎ P}{P}

if C is a tautology.

Factoring (F)  \frac{\{∼ A, Γ → A, Δ\} ⊎ P}{\{∼ A, Γ → Δ\} ∪ P}

Let Full be the set of all transformation rules defined in this section. Furthermore we define the following particular subsets of Full:

Norm = {SubF, SubGL, RedT, RedGL, Split}
Disj = Norm ∪ {RedF, Disj}

We will show that these are complete and independent for their respective classes of programs. Note that the Gelfond-Lifschitz transformation essentially uses the transformation rules GL = {SubGL, RedGL}, i.e., P ∪ P_{I} ⊢_{GL}^{∗} GL_{I}(P) ∪ P_{I}.

Theorem 5.1 Every subset of Full is sound.

Proof: It is sufficient to show Stab(P) = ⋃_{1≤i≤n} Stab(P_{i}) for every rule instance \frac{P}{P_{1}|...|P_{n}} of Full. The subsumption rules are instances of the general subsumption rule. The reduction rules can be obtained from Resolution followed by Subsumption. Disjunction and Factoring can be obtained from the general rules followed by Subsumption. Constraint propagation is an instance of Resolution. Default negation, Tautology elimination and Split are the same as the general rules. Thus soundness follows from theorem 4.1. □

Theorem 5.2 Every subset R of Full is terminating. Moreover, the length of a derivation P ⊢ … ⊢ P′ is polynomial in the size of P for any (⊢) ⊆ (⊢_{Full}).

Proof: To each program we associate a complexity measure c(P) = 2U(P)+2U′(P)+|P | where U(P) is the set of unknown propositions in P, U′(P) is the set of propositions A such that P neither contains A → nor → A and |P | is the number of literal occurrences in P. All subsumption and reduction rules, Tautology elimination and Factoring don’t increase 2U(P) + 2U′(P) and strictly decrease |P |. Disjunction, Default negation, Split and Constraint propagation strictly decrease 2U(P) + 2U′(P) by at least two, while Disjunction doesn’t increase |P | and Default negation, Split and Constraint propagation increase |P | by one. Thus every rule strictly decreases c(P) and every derivation in ⊢_{Full} starting from P can have at most length c(P). Since any strategy for a subset of Full is a subset of ⊢_{Full} we conclude that every subset of Full is terminating. □

Our transformation rules allow a great variety of strategies, but only a few will be reasonable in a practical sense. Tautology elimination and Factoring need to be used only at the beginning, since no rule introduces a tautology or a factorable clause. The simplification rules, Constraint propagation and Default negation should be used exhausively before applying Split. For the selection of the literal to use for splitting, heuristics known from classical Davis-Putnam procedures, like selecting propositions from short clauses, should be useful. We conjecture that in practice Disjunction will be applicable rarely. Since it is expensive to test its condition, it is reasonable to try it only if no other rule is applicable. In this case for a disjunction → A_{1}, …, A_{n} there exist clauses ∼ A_{1} →; …; ∼ A_{n} → and a stable model can only be reached if all A_{i} become true. We may abort a branch of our computation once the empty clause signals an inconsistency. For instance, to determine the stable models of P = {→ p, q; ∼ p → p; p, ∼ q → r} the following would be a typical computation.

F {→ p, q; ∼ p → p; p, ∼ q → r}

Split {→ p, q; ∼ p →; p, ∼ q → r} RedF \{q →; → p, q; ∼ p →; p, ∼ q → r\} SubGL \{q →; → p; ∼ p →; p, ∼ q → r\} RedGL \{q →; → p; p, ∼ q → r\} RedT \{q →; → p; p → r\} ; {\{q →; → p; → r\} \atop solved, I_{P} = \{p, r\}} | \{∼ q →; → p, q; ∼ p →; p, ∼ q → r\} \{∼ q →; → p, q; ∼ p →\} \{r →; ∼ q →; → p, q; ∼ p →\} incoherent, no model DNSubC

We get the result Stab(P) = {{p, r}}.

The other procedures for computing stable models of disjunctive programs do a case analysis with respect to which proposition of the conclusion becomes true. As a consequence some implied proposition may also become true, and the resulting model need not be minimal. Hence they need an explicit minimality check. We do case analysis whether an atom is false or constrained to true. With a false proposition we can reduce a disjunction while preserving minimality. However, we cannot reduce a disjunction with respect to a clause ∼ A →, hence we get a residual case where all atoms in the disjunction are constrained to be true. The Disjunction rule is then used to handle this special situation. The following derivations illustrates what happens for two critical example programs. First consider P = {→ p, q; p → q}.

Split {→ p, q; p → q} RedF \{p →; → p, q; p → q\} SubF \{p →; → q; p → q\} ; {\{p →; → q\} \atop solved, I_{P} = \{p\}} | \{∼ p →; → p, q; p → q\} \{∼ q →; ∼ p →; → p, q; p → q\} incoherent, no model CP

In the right branch Disjunction is not applicable, since p is not a consequence of P. By adding the clause q → p we get an example where Disjunction is needed. Note that this computation is an extension of the previous one, which illustrates the possibility of incremental computation.

Split {→ p, q; p → q; q → p} RedF \{p →; → p, q; p → q; q → p\} RedT \{p →; → q; p → q; q → p\} RedT \{p →; → q; p → q; → p\} \{□; → q; p → q; → p\} inconsistent, no model | \{∼ p →; → p, q; p → q; q → p\} \{∼ q →; ∼ p →; → p, q; p → q; q → p\} ; \{∼ q →; ∼ p →; → p; → q; p → q; q → p\} ; ⋮ ; {\{→ p; → q\} \atop solved, I_{P} = \{p, q\}} Disj CP

5.1 Completeness

Lemma 5.3 Full preserves NProg.

Proof: Observe that no transformation rule introduces new literals into the conclusion. □

Theorem 5.4 Norm is complete and independent for NProg.

Proof: To prove completeness it suffices to show that a Norm-reduced program which is not in solved form has no stable models. Then we will eventually obtain the solved forms for all stable models since every strategy has to apply some rule for non-reduced programs, and since Norm is terminating and sound.

Suppose P is Norm-reduced. Then Split assures that for every proposition A either A →, → A or ∼ A → is in P. Assume that for each proposition there exists one clause of form A → or → A, but that P is not in solved form because P contains some additional clause C. If C = □ then Stab(P) = ∅ and we are done. P doesn’t contain both A → and → A since Reduction-true is not applicable. Hence the premise of C cannot be empty, and we can apply some rule according to the following table, contradicting that P is reduced.

A →  → A
A, Γ → Δ Subsumption-false Reduction-true
∼ A, Γ → Δ GL-Reduction GL-Subsumption

Hence we may now assume that the set of all propositions A such that P contains neither A → nor → A is nonempty. Let us call this set U. From the table above we also know that the premises of clauses in P which are not of form A → or → A contain only propositions from U, since otherwise some transformation is possible. Since the Split rule is not applicable, P contains a clause ∼ A → for each A in U. Hence P has the form

\begin{aligned}L_{11}, …, L_{1k_{1}} → Δ_{1} & ∼ B_{1} → & → B′_{1} & B′′_{1} → \\ ⋮ & ⋮ & ⋮ & ⋮ \\ \underbrace{L_{n1}, …, L_{nk_{n}} → Δ_{n}}_{P′} & \underbrace{∼ B_{m} →}_{P_{U}} & \underbrace{→ B′_{m′}}_{P_{T}} & \underbrace{B′′_{m′′} →}_{P_{F}} \end{aligned}

where n, m′, m′′ ≥ 0, m ≥ 1, |Δ_{i}| ≤ 1, k_{i} + |Δ_{i}| ≥ 2, U = {B_{1}, …, B_{m}}, T = {B′_{1}, …, B′_{m′}} and F = {B′′_{1}, …, B′′_{m′′}} are pairwise disjoint, and all L_{ij} are of form B or ∼ B for B in U. Then P has at most the stable model I = T ∪ U. P_{1} = GL_{I}(P) eliminates all clauses with negative literals. We will show that J = T is a model of P_{1}. It satisfies GL_{I}(P_{T}) = P_{T}, GL_{I}(P_{F}) = P_{F} and GL_{I}(P_{U}) = ∅. To see that J satisfies GL_{I}(P′), observe that any clause in GL_{I}(P′) has at least one positive premise from U. We conclude that I is not minimal and Stab(P) = ∅.

To prove independence we exhibit for each rule r in Norm a program in NProg which is (Norm − {r})-reduced, not in solved form and has a stable model.

Rule  Program  Stable models
Reduction-true (RedT)  {p → q; → p; → q}  {p, q}
GL-Reduction (RedGL)  {∼ p → q; p →; → q}  {q}
Subsumption-false (SubF) {p, q →; p →; q →}  ∅
GL-Subsumption (SubGL)  {∼ p →; → p}  {p}
Split  {∼ p → q; ∼ q → p}  {p}, {q}
□

Theorem 5.5 Disj is complete and independent for Prog.

Proof: As in the completeness proof for Norm we will show that a Disj -reduced program which is not in solved form has no stable model. Suppose P is a Disj -reduced program. Then it is also Norm-reduced, and has the following form.

\begin{aligned}L_{11}, …, L_{1k_{1}} → Δ_{1} & ∼ B_{1} → & → B′_{1} & B′′_{1} → \\ ⋮ & ⋮ & ⋮ & ⋮ \\ \underbrace{L_{n1}, …, L_{nk_{n}} → Δ_{n}}_{P′} & \underbrace{∼ B_{m} →}_{P_{U}} & \underbrace{→ B′_{m′}}_{P_{T}} & \underbrace{B′′_{m′′} →}_{P_{F}} \end{aligned}

where n, m′, m′′ ≥ 0, m ≥ 1, k_{i} + |Δ_{i}| ≥ 2, U = {B_{1}, …, B_{m}}, T = {B′_{1}, …, B′_{m′}} and F = {B′′_{1}, …, B′′_{m′′}} are pairwise disjoint, and all L_{ij} are of form B or ∼ B for B in U. Moreover, RedF ensures that Δ_{i} ⊆ T ∪ U. Then P has at most the stable model I = T ∪ U and GL_{I}(P) = GL_{I}(P′) ∪ P_{T} ∪ P_{F}, where GL_{I}(P′) contains exactly the negation-free clauses of P′.

Now suppose Disjunction is not applicable. If k_{i} > 0 for all i then J = T is a model of GL_{I}(P), hence I is not minimal.

If there exists a clause with k_{i} = 0, but P̃ ∪ {→ A_{1}, …, A_{l}} |̸= {→ A_{1}; …; → A_{l}} then there exists an interpretations M of P̃∪{→ A_{1}, …, A_{l}} such that A_{j} ∉ M for some 1 ≤ j ≤ l. Because of P_{U} all propositions B̃ for B in U are false in M. Let J = M ∩ Prop, then J ⊧ GL_{I}(P), J ⊆ (T ∪ U) \ {A_{j}} ⊂ T ∪ U = I and I is not minimal. We conclude Stab(P) = ∅.

For independence we augment the proof for the non-disjunctive case by programs which are (Disj − {r})-reduced for r ∈ {RedF, Disj}. All the programs of the previous proof are reduced with respect to these rules, hence they carry over to this proof.

Rule  Program  Stable models
Reduction-false (RedF)  {→ p, q; p →; → q}  {q}
Disjunction (Dis)  {→ p, q; p → q; q → p; ∼ p →; ∼ q →}  {p, q}
□

6 Further work

Datalog. For the case of Datalog programs it would be desirable to avoid explicitly representing all false propositions and all instances of rules. This requires a more general notion of solved form and some modifications of the procedure since the original clauses will not be subsumed by their instances arising during computation. Moreover, Split and Disjunction may only be used on ground atoms, otherwise they are not sound. For the case of range-restricted programs, where all variables of a clause appear in its positive premises, this can be guaranteed.

Querying. Normally the interest is not so much in computing models but in query answering. It is possible to use a refutational approach for stable semantics. Consider a query Q = A_{1} ∧ … ∧ A_{n} ∧ ¬B_{1} ∧ … ∧ ¬B_{m} and let neg(Q) = A_{1}, …, A_{n}, ∼ B_{1}, …, ∼ B_{m} →. Then for any program P

P ⊧_{Stab} Q iff Stab(P ∪ {neg(Q)}) = ∅

It remains to develop a procedure which is specifically tailored to query answering. For that purpose it is not necessary to actually compute the stable models, but it suffices to test for satisfiability.

7 Conclusion

We have presented a new procedure for computing stable models of normal disjunctive logic programs. In analogy to the well-known Davis-Putnam procedure for classical propositional logic we used case analysis on the truth value of a proposition. It was crucial to allow clauses with empty heads. Then ∼ A → could represent that A is constrained to be true, without justifying A. Together with A → this allowed case analysis. We have shown the soundness of several transformation rules on programs, which allow to transform a program into an equivalent one. These may be interesting in their own right, either to develop different procedures for reasoning with stable models, or because they provide more insight into the nature of stable semantics. For instance, Factoring allowed to notice that ∼ p → p is equivalent to ∼ p →, hence its only effect is to constrain p to be true. From sets of sound rules we built our procedures and showed them to be complete, in the sense that they enumerate all stable models and terminate. We showed that for completeness only a subset of the rules was needed, while the others could be useful to improve performance. An actual implementation is free to choose which of these additional rules it uses.

We presented our procedure as a set of transformation rules, which resembled the standard method for presenting unification algorithms. Rules were sound in the sense that they preserved the set of stable models. The method allowed for concise presentation, flexible choice of a control strategy and simple correctness proofs.

Acknowledgements I would like to thank Harald Ganzinger for his helpful remarks on an earlier version of this report and Ullrich Hustadt and Yannis Dimopoulos for many discussions and for their general support.

References

Davis, M. and Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM 7: 201–215.

Eiter, T. and Gottlob, G. (1993). Complexity results for disjunctive logic programming and applications to nonmonotonic logics. Proc. Int. Logic Programming Symp., pp. 266–278.

Eshghi, K. (1990). Computing stable models by using the ATMS. Proc. AAAI-90, Boston, pp. 272–277.

Fernández, J. A. and Minker, J. (1992). Disjunctive deductive databases. Int. Conf. on Logic Programming and Automated Reasoning, Springer LNCS 624, St. Petersburg, pp. 332–356.

Gelfond, M. and Lifschitz, V. (1988). The stable model semantics for logic programming. Proc. Logic Programming Conf., Seattle.

Inoue, K., Koshimura, M. and Hasegawa, R. (1992). Embedding negation as failure into a model generation theorem prover. In D. Kapur (ed.), 11th International Conference on Automated Deduction, Springer LNAI 607, Saratoga Springs, NY, pp. 400–415.

Marek, W. and Subrahmanian, V. S. (1992). The relationship between stable, supported, default and autoepistemic semantics for general logic programs. Theoretical Computer Science 103: 365–386.

Saccà, D. and Zaniolo, C. (1990). Stable models and non-determinism in logic programs with negation. Proc. 9th ACM Symp. on Principles of Database Systems, Nashville, TN, pp. 205–229.

A Consequence relations

For the sake of the soundness proofs we introduce a consequence relation |∼ between programs. For other purposes |∼ is of little use, since it is not closed with respect to (cautious) cut. Define |∼ by P_{1} |∼ P_{2} if and only if for all interpretations I and J such that I ⊧ GL_{I}(P_{1}), J ⊆ I, and J ∈ Min(GL_{I}(P_{1})) we have J ⊧ GL_{I}(P_{2}).

Lemma A.1 Let P_{1} and P_{2} be programs. If P_{1} |∼ P_{2} and P_{2} |∼ P_{1} then Stab(P_{1}) = Stab(P_{2}).

Proof: Let P_{1} and P_{2} be programs and let I be an interpretation. We have to show that I is a minimal model of P′_{1} = GL_{I}(P_{1}) if and only if I is a minimal model of P′_{2} = GL_{I}(P_{2}).

For the only-if direction suppose I is a minimal model of P′_{1}. Then by P_{1} |∼ P_{2} with J = I we get I ⊧ P′_{2}. Suppose I is not a minimal model of P′_{2}, then there exists a minimal model J of P′_{2} with J ⊂ I. By P_{2} |∼ P_{1} we get J ⊧ P′_{1}, in contradiction to our assumption that I is a minimal model of P′_{1}. We conclude that I is a minimal model of P′_{2}. The argument for the other direction is exactly symmetric. □

Let CTaut = { A, Ã → | A ∈ Prop }.

Lemma A.2 Let P_{1} and P_{2} be programs. Then P̃_{1} ∪ CTaut ⊧ P̃_{2} implies P_{1} |∼ P_{2}.

Proof: Assume that I and J are interpretations such that J ⊆ I and J ⊧ GL_{I}(P_{1}), and combine them into an interpretation M = J ∪ { Ã | A ∉ I } suitable for P̃_{1}. We first show that M ⊧ P̃_{1} ∪ CTaut. Suppose C = A, Ã →∈ CTaut. By J ⊆ I A ∈ J implies A ∈ I, hence A ∈ M implies Ã ∉ M and C is true in M. Now suppose that C is a clause in P_{1}. If GL_{I} eliminates C then A ∈ I for some literal ∼ A in C. Thus Ã ∉ M and C̃ is true in M. If on the other hand GL_{I}(C) = {C′}, we have J ⊧ C′. Since C′ is negation-free this implies M ⊧ C′, and since C′ is a subclause of C we get M ⊧ C̃. Thus by assumption M ⊧ P̃_{2}.

Now let C be any clause in P_{2}. If GL_{I}C = ∅ we are done, so assume GL_{I}C = {C′}. In this case A ∉ I for all ∼ A in C. Then Ã ∈ M for all Ã in C̃, which implies M ⊧ C̃′. Since C′ is negation-free J ⊧ C′ follows and we are done. □

Lemma A.3 Let P_{1}, P_{2} and P_{3} be programs.

1. P_{1} |∼ P_{1}.

2. P_{1} |∼ P_{2} and P_{1} |∼ P_{3} imply P_{1} |∼ P_{2} ∪ P_{3}.

3. P_{1} |∼ P_{2} and P_{3} ⊆ P_{2} imply P_{1} |∼ P_{3}.

4. P_{2} ⊆ P_{1} implies P_{1} |∼ P_{2}.

5. P_{1} |∼ P_{2} if and only if P_{1} |∼ P_{1} ∪ P_{2}.

Proof: (1), (2) and (3) are trivial from the definition of |∼. (4) is a consequence of lemma A.2. The if part of (5) follows from (1) and (3), while the only-if part follows from (1) and (2). □

B Soundness proofs

Lemma B.1 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by Tautology elimination then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: This is an immediate consequence of lemma A.2. □

Lemma B.2 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by Resolution then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: Let P_{1} and P_{2} be programs such that P_{1} ⊢ P_{2} by Resolution. Then P_{1} = {C_{1}, C_{2}} ⊎ P and P_{2} = {C_{1}, C_{2}, C_{3}} ⊎ P for some program P and clauses C_{1}, C_{2} and C_{3} where C_{3} is a resolvent of C_{1} and C_{2}. Since P_{1} ⊆ P_{2} we have P_{2} |∼ P_{1}. For P_{1} |∼ P_{2} it suffices by lemma A.3 to show P_{1} |∼ C_{3}. For Standard resolution this is a consequence of lemma A.2.

For Constraint resolution we show that for all interpretations I and J with I ⊧ GL_{I}(P_{1}) and J ⊆ I such that J ⊧ GL_{I}(P_{1}) we have J ⊧ GL_{I}({C_{3}}). If GL_{I} eliminates C_{3} we are done. Suppose this is not the case.

For Constraint resolution C_{1} = ∼ A, Γ → Δ, C_{2} = A, Λ → Π and C_{3} = Γ, Λ, ∼ ·Π → Δ. Since GL_{I} doesn’t eliminate C_{3} we have Π ∩ I = ∅. Then GL_{I} eliminates neither Γ → Δ nor Λ → Π. Let GL_{I}(Γ → Δ) = Γ′ → Δ and GL_{I}(Λ → Π) = Λ′ → Π. Then GL_{I}(C_{3}) = Γ′, Λ′ → Δ. If A ∈ I then, because I is a model of GL_{I}({C_{1}, C_{2}}) and Π ∩ I = ∅, we have Λ′ ⊈ I. Via J ⊆ I we get Λ′ ⊈ J. We conclude J ⊧ GL_{I}(C_{3}). If on the other hand A ∉ I then A ∉ J and J ⊧ GL_{I}(Γ → Δ), which implies J ⊧ GL_{I}(C_{3}). □

Lemma B.3 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by subsumption then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: Let P_{1} and P_{2} be programs such that P_{1} ⊢ P_{2} by subsumption. Then P_{1} = {C_{1}, C_{2}} ⊎ P and P_{2} = {C_{1}} ⊎ P for some program P and clauses C_{1} and C_{2} where C_{1} subsumes C_{2}. Since P_{2} ⊆ P_{1} we trivially have P_{1} |∼ P_{2}. For P_{2} |∼ P_{1} it suffices by lemma A.3 to show P_{2} |∼ C_{2}, and in turn by lemma A.2 to show C̃_{1} ∪ CTaut ⊧ C̃_{2}. The clauses have the form C̃_{1} = Γ, Ã_{1}, …, Ã_{n} → B_{1}, …, B_{m}, Δ and C̃_{2} = Γ′, Ã_{1}, …, Ã_{n}, B̃_{1}, …, B̃_{m} → Δ′ with Γ ⊆ Γ′ and Δ ⊆ Δ′. By a series of classical resolutions of C̃_{1} with {B_{1}, B̃_{1} →; …; B_{m}, B̃_{m} →} we get Γ, Ã_{1}, …, Ã_{n}, B̃_{1}, …, B̃_{m} → Δ which implies C̃_{2}. □

Lemma B.4 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by Factoring then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: Let P_{1} and P_{2} be programs such that P_{1} ⊢ P_{2} by Factoring. Then P_{1} = {C_{1}} ⊎ P and P_{2} = {C_{1}, C_{2}} ⊎ P for some program P and clauses C_{1} = ∼ A, Γ → A, Δ and C_{2} = ∼ A, Γ → Δ. Since P_{1} ⊆ P_{2} we trivially have P_{2} |∼ P_{1}. For P_{1} |∼ P_{2} it suffices by lemma A.3 to show P_{1} |∼ C_{2}, which by lemma A.2 is a consequence of C̃_{1} ∪ CTaut ⊧ C̃_{2}. This is can be demonstrated by classical resolution and factoring. □

Lemma B.5 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by Default negation then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: Let P_{1} and P_{2} be programs such that P_{1} ⊢ P_{2} by Default negation. Then P_{2} = {C} ⊎ P_{1} for a clause C = A →. Since P_{1} ⊆ P_{2} we have P_{2} |∼ P_{1}. For P_{1} |∼ P_{2} it suffices by lemma A.3 to show P_{1} |∼ C. We show that for all interpretations I and J where J ∈ Min(GL_{I}(P_{1})) we have J ⊧ GL_{I}({C}).

Suppose A ∈ J and let J′ = J − {A}. Clauses in P_{1} which don’t contain A are satisfied by J′, since J is a model of P_{1}. Any clause in P_{2} which contains A has the form C = Γ, A → Δ, since GL_{I} deletes all literals ∼ A and by assumption A does not appear in the conclusion. But since A ∉ J′ we have J′ ⊧ C. Hence J is not minimal, in contradiction to the assumption. We conclude A ∉ J and J ⊧ P_{1}. □

Lemma B.6 Let P be a program and A a proposition. Then

Stab(P ∪ {A →}) = { I | I ∈ Stab(P) and A ∉ I }  and
Stab(P ∪ {∼ A →}) = { I | I ∈ Stab(P) and A ∈ I }.

Proof: Let P be a program, I an interpretation and A a proposition. Consider the case where A ∈ I. We have to show that I is a minimal model of GL_{I}(P) iff it is a minimal model of GL_{I}(P ∪ {∼ A →}). But from the definition of GL_{I} we get GL_{I}(P ∪ {∼ A →}) = GL_{I}(P).

Now suppose A ∉ I. It is easy to see that I ∈ Min(GL_{I}(P)) iff I ∈ Min(GL_{I}(P) ∪ {A →}) from the fact that I satisfies A →. □

Lemma B.7 Let P_{1} and P_{2} be programs. If P_{1} ⊢ P_{2} by Disjunction then P_{1} |∼ P_{2} and P_{2} |∼ P_{1}.

Proof: The proof is immediate from the condition on the rule and lemmas A.3 and A.2.

Theorem 4.1 is a consequence of these lemmas and lemma A.1.