TOPOLOGICAL CHARACTERIZATIONS FOR

LOGIC PROGRAMMING SEMANTICS

by

Audrey Piltch Ferry

A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Mathematics) in The University of Michigan 1994

Doctoral Committee: Professor Andreas Blass, Chair Professor Morton Brown Associate Professor Kevin Compton Professor Peter Hinman Professor Arthur G. Wasserman

ACKNOWLEDGEMENTS

I have been fortunate in the course of this work to have the advice of three fine mathematicians: Andreas Blass, Wiktor Marek, and Steve Ferry. In addition to their enthusiasm, I particularly admire their ability to bring to light the reality behind formalisms. I hope their example finds reflection in my work.

Though I would hope that my family realizes how much I appreciate all they have done, I would like here to express my gratitude publicly to my parents, Abe and Helen Piltch; my parents–in–law, Arthur and Virginia Ferry; my sister, Nancy; my children, Ken and Vivian; and again and especially to my husband Steve, whose support throughout every aspect of this project has been indispensable.

PREFACE

Mathematical reasoning, formalized in classical logical systems as the production of a set of theorems from a set of axioms, is of course monotonic with respect to inclusion. Since what may be deduced is what holds in every model of the axioms, enlarging the set of assumptions restricts the set of acceptable models and thus increases the set of deducible consequences. In the real world, however, reasoning may follow a different paradigm. Often it is appropriate to admit only typical situations which fit some given initial information, without taking every remote possibility into account. Under this paradigm, reasoning is not generally monotonic. For with the addition of new information, different cases may qualify as typical, with some characteristics changed from those accepted before. Operationally, applications based on this approach, such as deductive databases or some aspects of robotics, might incorporate a mechanism for making revisions. More fundamentally, any system involving this type of reasoning must have some satisfactory basis beyond classical logic for deriving conclusions.

Since the late 1970’s, a number of formalisms for nonmonotonic reasoning have been proposed, based on different intuitions and formulated in diverse ways. They differ in applicability, and on examples where they can be compared they may not agree. For various systems, individually and jointly, researchers have examined syntax and semantics, the complexity of calculations, what concepts are expressible, and how well the formal answers accord with intuition. Such analysis has led to improvements and refinements, and, more significantly, to some understanding of general principles.

In this regard, particular progress has come about through comparing different systems on the basis of their intended models. Important examples of intended models are the minimal, stable, and supported models associated with different semantics for logic programming, and, by translation, with the semantics for various other systems. Though much has been learned about their structure, no full description of these classes of models has previously been given.

The main contribution of this paper is to characterize among the sets of appropriate interpretations for the language those which are the minimal, stable, and supported model classes of programs. This is accomplished by viewing the interpretations as points in a topological space; the subsets of the space corresponding to classes of a given sort are then found to be distinguished by particular topological properties. The study involves both the Cantor topology familiar from descriptive set theory and the less well–known inverse–Scott topology, defined originally in domain theory in connection with representing information about computations. We view the topological approach as a supplement to and extension of the usual recursion–theoretic analysis, whose use is appropriate in this situation as a setting for distinguishing the roles of negative and positive information in determining these classes. Furthermore the properties which characterize these classes are in fact found to depend on such topological concepts as closure and compactness.

The basic characterization results are stated in Theorem 2.2 for minimal model classes, Theorems 3.1, 3.2, and 3.3 for stable model classes (in different forms), and Theorem 5.1 for supported model classes. Closely related to the topological characterizations are results of two other sorts: descriptions of the classes in terms of formulas extracted from the programs, and normal forms for programs representing given classes. Results of the first sort have previously been given for supported models ([10]) and for stable models ([36]); we obtain in Theorem 2.5 a similar description for minimal models. We make explicit a normal form representation for stable model classes (Proposition 3.1) due to [36], and provide such forms also for minimal model classes (Theorem 2.4) and for supported model classes (Corollary 5.1). We include algorithms for calculating minimal models from programs and vice versa; in other cases the theorems themselves provide procedures for calculations. As an application of compactness, we obtain characterization results for the stable and supported model classes of programs with certain finiteness properties (Theorems 4.1 and 6.1). Finally we describe how the classes of intended models can be broadened via a natural transformation h introduced in [34, 35] for studying Turing complexity (Theorems 7.1–7.5). Examples are included at every stage to mark distinctions among conditions.

The presentation is as follows: In Chapter 1 we review the introduction of various forms of nonmonotonic reasoning and the subsequent development of a more comprehensive point of view. We also discuss the application of topological ideas to logical questions and introduce the Cantor and inverse–Scott topologies. We conclude the introductory section by setting our main question in the context of previous results. Chapter 2 contains the results on minimal model classes, which are basic to the further development. Chapter 3 relates stable models to minimal models to obtain characterizations for stable model classes, and Chapter 4 treats the special case of stable model classes of finite proof support programs. Chapters 5 and 6 obtain analogous results for supported model classes, first of general programs and then of programs with the finite completion property. Finally Chapter 7 establishes characterization results involving the transformation h.

TABLE OF CONTENTS

ACKNOWLEDGEMENTS . . . . . . . . . . . . . . . . . . . . . . . . . . ii PREFACE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii CHAPTER

1. INTRODUCTION . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1 Logic programming background . . . . . . . . . . . . . . . . . . . 1 1.2 Nonmonotonic reasoning background . . . . . . . . . . . . . . . . 11 1.3 Topological background . . . . . . . . . . . . . . . . . . . . . . . . 22 1.4 The characterization problem . . . . . . . . . . . . . . . . . . . . . 27

2. MINIMAL MODEL CLASSES . . . . . . . . . . . . . . . . . . . . . . 35 3. STABLE MODEL CLASSES . . . . . . . . . . . . . . . . . . . . . . . 64 4. FINITE PROOF SUPPORT PROPERTY . . . . . . . . . . . . . . . 79 5. SUPPORTED MODEL CLASSES . . . . . . . . . . . . . . . . . . . . 90 6. FINITE COMPLETION PROPERTY . . . . . . . . . . . . . . . . . 102 7. THE TRANSFORMATION h . . . . . . . . . . . . . . . . . . . . . . 107 BIBLIOGRAPHY . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123

CHAPTER 1

INTRODUCTION

In this chapter we present background material from three areas: logic programming, the setting for our investigation; non–monotonic reasoning, the subject of our study; and topology, our means for analysis. In the last section we will discuss specifically the characterization problem and the form of our solution.

1.1 Logic programming background

In this section we present basic terminology concerning programs, models, and partial orderings. While our notation in this and later sections is for the most part standard, we find it convenient in representing clauses and finite sets of conditions to make use of a vector notation. In the first place, we permit the use of conjunction or disjunction symbols outside the setting of a formal system as abbreviations for saying that all or some of an indicated collection of conditions hold, including in particular the convention that ⋀_{a∈∅} φ_{a} = true and ⋁_{a∈∅} φ_{a} = false. Now, given a finite set A ⊆ U, the symbol A⃗ appearing within an expression abbreviates the individual use of each element of A. When negation is involved, it applies separately to each element. Thus the assertion

A⃗ ∈ S

for S ⊆ U stands for the conjunction of the assertions

a ∈ S for a ∈ A, generally written as

⋀_{a∈A}(a ∈ S),

which has the same meaning as

A ⊆ S.

The expression

B⃗ ∉ S

involving a negated relation symbol stands for the conjunction of the assertions

b ∉ S

for b ∈ B; that is, for

⋀_{b∈B}(b ∉ S),

or, equivalently,

B ∩ S = ∅.

Similarly, when the expression A⃗ appears in a clause body, it should be interpreted to mean that each element a of A appears there; and likewise when the symbol ¬B⃗ occurs, it stands for the appearance of ¬b for each b ∈ B. To avoid confusion, no such notation will be used to represent disjunctions.

We consider first the syntax of logic programming, beginning with the literals which are the building blocks of clauses. A positive literal in the case of propositional logic programming is an element of a given set U of atoms, or in the predicate case is an atomic formula, with or without free variables, in a given language L. A negative literal in either case is the negation of a positive literal. In predicate logic programming, a literal with no free variables is called a ground literal.

A clause (or, for emphasis, general clause) is an expression of the form

c ← a_{1}, …, a_{n}, ¬b_{1}, …, ¬b_{m},

c ← a_{1}, …, a_{n},

c ← ¬b_{1}, …, ¬b_{m},

or

c ←

where a_{1}, …, a_{n}, b_{1}, …, b_{m}, and c are all positive literals. As mentioned above, we sometimes write a general clause in the form

c ← A⃗, ¬B⃗

where A and B are finite sets of positive literals, either or both of which may be empty. The element c is called the head of the clause, and the set A ∪ {¬b : b ∈ B} of the remaining positive and negative literals is called the body of the clause. The positive literals in the body are called prerequisites. If the set of prerequisites is empty, then the clause is said to be prerequisite–free. On the other hand, if there are no negative literals in the body, the clause is called a Horn clause. Thus

c ← ¬b_{1}, …, ¬b_{m}

is prerequisite–free,

c ← a_{1}, …, a_{n}

is Horn, and

c ←

has both properties. Since Horn clauses were studied before the more general clauses defined here, in older works the term “clause” by itself is used as a synonym for “Horn clause,” and when negative literals are permitted in the body, the term “general clause” is always used. In this paper, however, the terms “clause” and “general clause” are used interchangeably.

A logic program, or simply program, is a finite or countably infinite set of clauses. A program is called prerequisite–free if it consists entirely of prerequisite–free clauses, and similarly is called a Horn program if it contains only Horn clauses.

Next we consider the semantic aspects of logic programming. Given a logic program P, we associate with it a theory Θ(P) of propositional or predicate logic, whichever is appropriate, by replacing each clause

c ← A⃗, ¬B⃗

of P by the formula

( ⋀_{a∈A} a ∧ ⋀_{b∈B} ¬b) → c

if P is a propositional logic program, or by the formula

∀v_{1} … ∀v_{k}[( ⋀_{a∈A} a ∧ ⋀_{b∈B} ¬b) → c],

where v_{1}, …, v_{k} are the free variables of the clause, if P is a predicate logic program. By an interpretation for P, we mean then an interpretation for Θ(P) in the sense of the appropriate logic. Thus an interpretation for a propositional logic program over U is a subset of U, and an interpretation for a predicate logic program in a language L is a set A together with elements from A and relations and functions over A corresponding to the constant, relation, and function symbols of L. Similarly an interpretation I for program P is a model of P (written I ⊧ P) if I is a model in the logical sense for Θ(P). A sentence σ of propositional or predicate logic is a logical consequence of P (written P ⊧ σ) if σ holds on every model of P. Different notions of consequence, connected with special sorts of models, will be introduced in Section 1.2.

For a predicate logic program P, models whose domains correspond exactly to the closed terms of the language of P are of particular interest. (By the language of P we mean the set of relation, function, and constant symbols which actually appear in P.) If L is the language of P, the set of closed terms of L is called the Herbrand universe of P. An interpretation for P is called a Herbrand interpretation if its domain is the Herbrand universe, each constant symbol of L is assigned to itself, and each function symbol of L is assigned to the function which maps an n– tuple of closed terms in the domain to the closed term formed by application of the function symbol to the n–tuple. Different Herbrand interpretations are distinguished by different interpretations for the relation symbols of L—that is, by different sets of ground atomic facts. A Herbrand interpretation for P which is a model of P is called a Herbrand model of P.

For a predicate logic program P, the set of closed atomic formulas in the language of P is called the Herbrand base of P, usually denoted B_{P} . The Herbrand interpretations of P are in one–to–one correspondence with the subsets of B_{P} , where each Herbrand interpretation is associated with its set of ground atomic facts. Furthermore, suppose that program P′ is obtained from P by replacing each clause of P by all its ground instances. P′ may be considered as a propositional logic program over the universe U = B_{P} . Then the set of ground atomic facts of a Herbrand interpretation of P constitutes an interpretation in the propositional sense of the program P′. Thus results about interpretations of propositional programs apply also to Herbrand interpretations of predicate logic programs.

Finally we review some notions about partial orderings, in connection with certain orderings of interpretations. Interpretations of propositional programs, which are just sets of atoms from a given universe, are naturally ordered by set inclusion. For interpretations of predicate logic programs, we say that I_{1} ≤_{t} I_{2} if I_{1} and I_{2} have the same domains and the same interpretations for constant and function symbols of L and, for each relation symbol R of L and tuple a⃗ of elements from the domain, if I_{1} ⊧ R[a⃗] then I_{2} ⊧ R[a⃗]. It is easily checked that the ordering ≤_{t} is reflexive, antisymmetric, and transitive. (The notation “≤_{t}” was introduced by Fitting ([16]), to distinguish an ordering of partial interpretations based on “truth” from a different ordering based on “knowledge.”)

For any ordering ≤ on a set S, we use min S (called the minimal elements of S) to stand for the set of elements of S for which no other element of S is lower in the ordering ≤; that is,

min S = {S ∈ S : (∀S′ ∈ S)[S′ ≤ S ⇒ S′ = S]}.

In particular, S is said to be a minimal model of a given program P if S is a model of P and no other model of P is below S in the appropriate ordering ⊆ or ≤_{t} . An element S of S is said to be the least element of S relative to ≤ if S ≤ S′ for every S′ ∈ S. By antisymmetry of ≤, a set has at most one least element. If S is the least element of S, then also S ∈ min S. Of course an arbitrary set S of interpretations may not have a least element or even any minimal elements. For some programs, however, a least model of a particular sort is guaranteed.

For S ⊆ 2^{U}, we denote the upper closure of S with respect to the ordering ⊆ by S^{⊇}; that is

S^{⊇} = {S′ ∈ 2^{U} : S′ ⊇ S for some S ∈ S}.

We will not need to use the corresponding notion of lower closure for propositional interpretations, nor will we need similar notions for interpretations of predicate logic programs.

Much of logic programming semantics is described in terms of operators defined on the collection of subsets of a universe U. A set S is said to be a fixpoint of an operator T if T (S) = S, a prefixpoint of T if T (S) ⊆ S, and a postfixpoint of T if T (S) ⊇ S. In general nothing can be said about the existence of fixpoints of such an operator. However, if the operator T : 2^{U} → 2^{U} is monotone with respect to the ordering ⊆ on 2^{U}—that is, if S_{1} ⊆ S_{2} implies that T (S_{1}) ⊆ T (S_{2})—then by a theorem of Knaster and Tarski ([60]) T has both a least fixpoint lfp(T) and a greatest fixpoint gfp(T). The least fixpoint of T is the intersection of all the fixpoints, or equivalently all the prefixpoints, of T, and the greatest fixpoint is the union of all the fixpoints, or equivalently all the postfixpoints, of T.

When T has a further property, more can be said about the structure of the least fixpoint (or, for an analogous property, about the structure of the greatest fixpoint). An operator T (not necessarily monotone) is said to be finitizable (we prefer to say positive–finitizable) if

T ( ⋃_{n∈ω} S_{n}) ⊆ ⋃_{n∈ω} T (S_{n})

whenever S_{0} ⊆ S_{1} ⊆ …. The terminology is appropriate because, for determining the presence of an element y in T (X) for X ⊆ U, if X is expressed as the union of an increasing sequence of finite sets S_{i}, the information about X which is used is confined to some set S_{n}, for which there is an infinite amount of negative information but only finitely much \underline{positive} information. Note that if T is monotone, then the reverse inclusion

⋃_{n∈ω} T (S_{n}) ⊆ T ( ⋃_{n∈ω} S_{n})

holds, so that, if T is both monotone and finitizable,

T ( ⋃_{n∈ω} S_{n}) = ⋃_{n∈ω} T (S_{n}).  (1.1)

If T is monotone, the upward ordinal powers of T applied to S ∈ 2^{U} are defined as follows:

T ↑ 0(S) = S
T ↑ α(S) = T (T ↑ (α − 1)(S)) if α is a successor ordinal
T ↑ α(S) = ⋃{T ↑ β(S) : β < α} if α is a limit ordinal.

Consider the sequence of upward ordinal powers of T obtained by starting at S = ∅. Since

∅ =^{def} T ↑0(∅) ⊆ T ↑1(∅),

using monotonicity it follows by induction that

T ↑0(∅) ⊆ T ↑1(∅) ⊆ … ⊆ T ↑n(∅) ⊆ T ↑(n + 1)(∅) ⊆ ….

Now if in addition T is positive–finitizable, then

T (T ↑ω(∅)) =^{def} T ( ⋃_{n∈ω} T ↑n(∅))
= ⋃_{n∈ω} T (T ↑n(∅)) by (1.1)
= ⋃_{n∈(ω−{0})} T ↑n(∅)
= ⋃_{n∈ω} T ↑n(∅)
=^{def} T ↑ω(∅),

so T ↑ ω(∅) is a fixed point of T. In fact T ↑ ω(∅) is the least fixpoint lfp(T) given in the Knaster–Tarski theorem. For if S is an arbitrary fixpoint of T, then from the base case

∅ =^{def} T ↑0(∅) ⊆ S,

we can show by induction, using monotonicity and the fact that S is a fixpoint, that

T ↑n(∅) ⊆ S

for all n ∈ ω, and therefore

T ↑ω(∅) =^{def} ⋃_{n∈ω} T ↑n(∅) ⊆ S.

The positive–finitizability property gives no information about the structure of the greatest fixpoint of a monotone operator. If T has a certain dual property, however, the point gfp(T) can be specified instead of lfp(T). An operator T : 2^{U} → 2^{U} (not necessarily monotone) may be said to be negative–finitizable if

T ( ⋂_{n∈ω} S_{n}) ⊇ ⋂_{n∈ω} T (S_{n})

whenever S_{0} ⊇ S_{1} ⊇ …. In this case, if X ⊆ U is expressed as the intersection of a descending sequence of cofinite sets S_{i}, then the absence of a point y from T (X) is determined by the information about some set S_{n}, hence by possibly infinitely much positive information but at most finitely much negative information. If T is monotone, then the downward ordinal powers of T applied to S ∈ 2^{U} are defined as follows:

T ↓ 0(S) = S
T ↓ α(S) = T (T ↓ (α − 1)(S)) if α is a successor ordinal
T ↓ α(S) = ⋂{T ↓ β(S) : β < α} if α is a limit ordinal.

In this case the sequence of downward ordinal powers starting at S = U is a decreasing sequence. If T is both monotone and negative–finitizable, then we can show as above that T ↓ω(U) is the greatest fixpoint of T.

In Section 1.2, the well–known immediate consequence operator T_{P} : 2^{U} → 2^{U} for a program P will be introduced. We will define it here as well in order to establish properties which are generally considered common knowledge. We may assume that P is a propositional logic program (possibly obtained, as discussed earlier, by replacing the clauses of a predicate logic program by all their ground instances). For S ∈ 2^{U}, we define

T_{P} (S) = {c ∈ U : c ← A⃗, ¬B⃗ is a clause of P and S ⊧ ( ⋀_{a∈A} a ∧ ⋀_{b∈B} ¬b)}.

Notice that if P is a Horn program, then T_{P} is monotone. For suppose that S_{1} ⊆ S_{2}, and that c ∈ T_{P} (S_{1}). Then there is a clause

c ← A⃗

of P such that S_{1} ⊧ ⋀_{a∈A} a, which means that A ⊆ S_{1}. Since S_{1} ⊆ S_{2}, it follows that S_{2} ⊧ ⋀_{a∈A} a, and hence c ∈ T_{P} (S_{2}). Furthermore, for any program P (Horn or otherwise), T_{P} is positive–finitizable. For suppose that S_{0} ⊆ S_{1} ⊆ …. We need to show that

T_{P} ( ⋃_{n∈ω} S_{n}) ⊆ ⋃_{n∈ω} T_{P} (S_{n}).

Let c ∈ T_{P} (⋃_{n∈ω} S_{n}). Then there is a clause

c ← A⃗, ¬B⃗

of P such that A ⊆ ⋃_{n∈ω} S_{n} and B ∩ ⋃_{n∈ω} S_{n} = ∅. Since A is finite, A ⊆ S_{k} for some k ∈ ω, and it is also the case that B ∩ S_{k} = ∅. Therefore

c ∈ T_{P} (S_{k}) ⊆ ⋃_{n∈ω} T_{P} (S_{n}),

as desired. On the other hand, it is not the case that T_{P} is negative–finitizable, even if P is Horn. For instance, if P is the program

c ← a_{0}
c ← a_{1}
c ← a_{2}
⋮

and S_{n} = {a_{i} : i ≥ n}, then T_{P} (S_{n}) = {c} for every n ∈ ω, but T_{P} (⋂_{n∈ω} S_{n}) = T_{P} (∅) = ∅. Thus it is not the case that

T_{P} ( ⋂_{n∈ω} S_{n}) ⊇ ⋂_{n∈ω} T_{P} (S_{n})

for this sequence S_{0} ⊇ S_{1} ⊇ …. We note then the following properties of T_{P} when P is a Horn clause program: Since T_{P} is monotone, it has both a least and a greatest fixpoint. Since T_{P} is positive–finitizable, the least fixpoint can be found by calculating T_{P} ↑ ω(∅). On the other hand, T_{P} ↓ ω(U) may be strictly greater than every fixpoint of T_{P} in the ordering ⊆ .

The important notions of supported and stable models of programs will be introduced in the next section (Section 1.2) of this chapter, where the reasons for studying intended models of various sorts will be discussed. Working definitions for model, minimal model, stable model, and supported model will be restated briefly at the beginning of Section 1.4. For definitions of the topological spaces (2^{U}, Cantor) and (2^{U}, Scott^{−1}), see Section 1.3.

1.2 Nonmonotonic reasoning background

In this section we survey the introduction and development of systems for nonmonotonic reasoning. As history this account is far from complete. Its purpose is rather to provide the background for understanding a common outlook based on intended models which has gradually emerged.

In the following description, the treatment of negation will be a prominent issue. The problem for any system of nonmonotonic reasoning is how to make plausible deductions from information which is not sufficient to justify any conclusion in the classical sense. With the conclusions of implications or of inference rules limited by convention to positive elements, the problem centers on how to handle negation: how to derive negative conclusions, and how to reason in the presence of negative information. Different solutions amount to different non–classical interpretations of negation. Furthermore, the interpretation must reflect some intuition about deriving only properties which are generic or typical for the given data. On examples like Horn clause programs in logic programming, intuitions for the most part agree and different systems of reasoning produce similar answers. But when negative premises are permitted, different interpretations no longer coincide.

One of the first formalizations for nonmonotonic reasoning was given by Reiter for deductive databases ([53]). Recognizing as nonmonotonic the reasoning in relational database systems under which ¬A is asserted if the ground atomic fact A is not present in the database, he generalized this principle to deductive databases as the Closed World Assumption (CWA): that for a ground atom A, ¬A is entailed by the database whenever A is not derivable.^{1} Then he defined the nonmonotonic consequences of database D to be the logical consequences of the extended database D′ obtained by adding to D the negated atoms obtained by the Closed World Assumption along with axioms for Herbrandness. Reiter showed that if D consists entirely of Horn clauses, then D′ has a unique model M, which may be interpreted as the “intended” model of D. Note for later comparison that M is the least Herbrand model of D, and also that every positive fact of M is “supported” by a derivation from data. In many instances the Closed World Assumption provides a convincing realization for nonmonotonic reasoning. However this approach does not deal in any satisfactory way with information which involves the disjunction of more than one positive ground literal. For instance, if the database consists of the single non–Horn clause

p ← ¬q,

or of the logically equivalent formula

p ∨ q,

then the extended database, containing

{p ∨ q, ¬p, ¬q},

is inconsistent.

To accommodate so–called “indefinite” information of this sort, some approaches recognize multiple situations as typical. Two such approaches based on “minimal” as the interpretation of “typical” are the Generalized Closed World Assumption (GCWA) for disjunctive databases due to Minker [45] and circumscription, invented

1 Reiter states explicitly ([55]) that in this definition a database D may be any first–order theory. Later authors have confined their consideration of the CWA to the case where D is a universal first–order theory or even consists only of clauses. In that case, the condition that ground atom A is not derivable from D, which appears in the definition, is equivalent to the existence of a Herbrand model of D ∪ {¬A}.

by McCarthy [42] and developed particularly by Lifschitz [30]. Under the GCWA, the sentences which are inferred are the logical consequences of the database augmented by the negative ground literals which hold in all minimal Herbrand models of the database. When the database is a universal theory (for which by Zorn’s Lemma every Herbrand model contains a minimal Herbrand model), notice that the CWA in contrast asserts all negative ground literals that hold on \underline{some} minimal Herbrand model of the database. Minker also gave an equivalent procedural description, as in the CWA, for inferring negated ground atoms, based on nonderivability of certain formulas involving the associated atom. Subsequently Yahya and Henschen ([63]) defined and also provided a procedural description for the Extended Generalized Closed World Assumption (EGCWA), under which the database is augmented by formulas ¬K which hold on all minimal Herbrand models of the database, where K is a finite conjunction of positive ground literals. It can be shown by induction that the EGCWA permits the inference of all quantifier–free sentences which hold on every minimal Herbrand model of the database. Circumscription on the other hand permits the inference of those sentences of first–order logic which hold on \underline{all} minimal models of a given theory, obtained in this case as the logical consequences of the theory together with second–order circumscription axioms declaring the extents of predicates to be minimal. In general, it is not possible to replace the second–order axioms by an equivalent set of first–order sentences. Desired consequences can often be derived in practice, however, by instantiating the universally quantified predicate variables in the axioms to properly chosen values. Typical but possibly conflicting expectations for multiple predicates can be represented using a generalization of the ordering ≤_{t} proposed by McCarthy ([43]), which orders models in accordance with a priority assigned to predicates to allow some to be minimized at the expense of others. For Herbrand models, the Extended Closed World Assumption of [21] relates this generalized notion of minimality to inference of negated atoms based on nonderivability.

Study of a different sort of nonmonotonic reasoning was motivated by the development of Prolog at approximately the same time as the ideas above were being explored. Prolog is based on the idea that a clause

c ← ℓ_{1}, …, ℓ_{n}

may be interpreted as the definition of a procedure for computing c (that is, for computing the truth value of c in the propositional case, or for computing substitutions for variables that result in true statements in the predicate case), based on subprocedures for computing the literals ℓ_{1}, …, ℓ_{n}. In “standard” Prolog, which applies only to Horn clause programs, a positive literal c as above may be inferred by a process called Selection Linear Definite (or SLD) resolution introduced by Kowalski ([25]). Nonmonotonicity arises from the “negation as failure” interpretation, under which a negative ground literal is inferred if the attempt to derive the associated positive literal by SLD–resolution fails within finitely many steps. In [10] Clark combined “negation as failure” with SLD–resolution into a comprehensive SLDNF procedure applicable to general clauses. For programs where the SLDNF procedure terminates, it is easier to derive negative literals by SLDNF than by logical consequence; accordingly easier to derive positive literals depending on negative subgoals by SLDNF than by logical consequence; and therefore more difficult to derive negative literals by SLDNF than by CWA. For example, given the program

p ← ¬q,

no literals are inferred by logical consequence, ¬q and p are inferred by SLDNF , and both ¬q and ¬p are inferred under the CWA. For the program

p ← ¬p,

however, neither p nor ¬p is inferred by SLDNF , although p is a logical consequence of the program.

To clarify negation as failure in this special sense, Clark proposed that a program should be viewed in terms of a related theory called its “completion.” The completion comp(P) of a program P consists of equivalences formed using combinations of clauses from P to express the additional requirement that a clause head may hold only if one of its clause bodies is satisfied. Clark suggested that the models of comp(P) were to be considered as the “typical” or intended models of P. He then showed that SLDNF is sound with respect to the completion in the sense that every goal which can be inferred by SLDNF from P (using a “safe” computation rule, which prohibits the selection of non–ground negative literals) is a logical consequence of comp(P). Later it was shown ([23]) that, when P is a Horn clause program, positive goals which are logical consequences of comp(P) can be inferred by SLDNF from P. In general, however, SLDNF is not complete with respect to comp(P).

Though the notion of completion was originally introduced to support negation as failure, it has come to be considered the more basic concept. Under the completion semantics, a goal is inferred from program P if it holds on every model of comp(P). The SLDNF proof procedure may then be viewed as supporting this “declarative” semantics for logic programming in certain cases.

A useful method introduced in connection with the completion involves the immediate consequence operator T_{P} for a program P, defined for Horn clause programs in [61] and for general programs apparently in [32]. Given as input a set of ground atoms, T_{P} produces as output the set of conclusions of ground instantiations of clauses from P whose bodies are satisfied on the input set. In [61] and [5], the Herbrand models of a Horn clause program P and of its completion were studied as the prefixpoints and fixpoints, respectively, of T_{P} . If P is Horn, then T_{P} is monotone and its least fixpoint T_{P} ↑ ω(∅) is the least Herbrand model both of P and of comp(P). Under the least fixpoint semantics ([61]), the goals inferrable from the program are considered to be the ones which hold on this single model, in agreement with the CWA. A different semantics for Horn clause programs, based on [5], permits the inference of those goals which hold on all fixpoints of T_{P} —that is, on all Herbrand models of comp(P). It uses in particular what Lloyd ([32]) calls the Herbrand rule to infer negative ground literals. For a ground literal a (that is, for a ∈ B_{P}), ¬a can be inferred under the least fixpoint semantics if and only if a ∉ lfp(T_{P}) = T_{P} ↑ω(∅), but under the Herbrand rule semantics if and only if a ∉ gfp(T_{P}). In comparison, by results of [5] and [29], ¬a can be inferred under SLDNF (or equivalently in this case by the completion semantics) if and only if a ∉ T_{P} ↓ ω(B_{P}). When P is a general rather than Horn program, the operator T_{P} is not monotone, and fixpoints are not guaranteed. Whatever fixpoints there might be are called the supported models ([3]) of P. As a generalization of the Horn program semantics given by the Herbrand rule, the supported model semantics for a general program P permits the inference of those goals which hold on all supported models of P —that is, on all Herbrand models of comp(P). Notice that with the shift of attention to intended models, the interpretation of negation has shifted from failure of a proof procedure to absence from appropriate models.

Another formalization for nonmonotonic reasoning, introduced only slightly later than the formulations based on minimality or on negation as failure which we have considered so far, is the default logic proposed by Reiter [54]. In this system, along with an initial set W of sentences is given a set D of default inference rules. A default rule specifies what is to be inferred when certain information is lacking; if that information is present, however, the default inference is blocked. It is crucial that the criterion about presence of information refers not to W but to a candidate set extending the first–order consequences of W. If a set E is closed under the inference rules of first–order logic and all default rules which are applicable in E, and contains only elements derivable by these rules, then E is called an extension of (W, D). The extensions are considered to represent “typical” situations in this reasoning system. It is possible then to define the consequences of (W, D) to be the sentences which belong to every extension of (W, D). Formally the extensions of (W, D) are obtained as the fixpoints of an operator F_{(W,D)} on sets of sentences; because its output depends on the absence of information from its input, F_{(W,D)} is non– (in fact, anti–) monotonic. A different nonmonotone operator F′_{(W,D)}, involving presence as well as absence of information, gives rise to a different set of intended models called weak extensions.

In [19] Gelfond and Lifschitz proposed a new semantics for logic programming, called the stable model semantics, which is closely related to default reasoning. In their interpretation, negations of ground atoms in a clause body are understood in the default sense as testing the absence of those atoms from a candidate set, with the effect of permitting or blocking inferences described by the remainder of the clause. This is accomplished by way of a two–stage operation F_{P} on such candidate sets. The program P is assumed to have no free variables, any program not originally of this form having been replaced by the ground instantiations of its clauses. For a given set S of ground atoms, first the program P is transformed to a new program GL(S, P) by dropping those clauses whose bodies contain negations of atoms which are present in S and omitting all negative literals from the remaining clauses. Since the resulting program is Horn, it has a least Herbrand model, which can then be found as T_{GL(S,P)} ↑ ω(∅). This is the value assigned by F_{P} to S. The elements of F_{P} (S) are said to be S–provable. If S is a fixpoint of the operator F_{P} —that is, if S = F_{P} (S) = T_{GL(S,P)} ↑ω(∅)—then S is called a stable model of P.

Given a logic program P, suppose that a set D(P) of default inference rules is obtained by translating each clause

c ← a_{1}, …, a_{n}, ¬b_{1}, …, ¬b_{m}

of P into a rule with c as conclusion, a_{1}, …, a_{n} as prerequisites, and b_{1}, …, b_{m} as the information whose absence is required to activate the rule. Then the stable models of P are the same as the atomic parts of the extensions of (∅, D(P)) [8, 39]. Furthermore, under this same translation, the supported models of P correspond to the weak extensions of (∅, D(P)). This clarifies the effect of the completion as specifying fixed points under a type of deduction that allows both positive and negative introspection.

To this point we have considered three independent strains in the development of nonmonotonic reasoning, based respectively on minimality, negation as failure, and default reasoning. The associated intended models provide the material which we will study in this thesis. The remaining topics which we will survey—stratification, autoepistemic logic, and modal nonmonotonic logic—can now be understood as involving specializations or generalizations of these basic reasoning patterns. We mention them both because they are essential parts of the subject and because the current point of view based on intended models developed from and encompasses all these topics.

Somewhat prior to the introduction of the stable model semantics for logic programming, Apt, Blair, and Walker ([3]) described a syntactic class of logic programs called stratified logic programs, properly including the class of Horn clause programs, for which a unique intended model can be constructed in a natural way. Przymusinski ([49]) generalized their notion to locally stratified logic programs, for which a similar construction works, by adapting their ideas about predicates to ground literals. A logic program P is locally stratified if there is a partition (S_{α})_{α<γ} of its Herbrand base such that for every ground instance of a clause in P the ordinal level of the literal in the head is at least as great as the levels of the positive literals and strictly greater than the levels of the negative literals in the body. The intended model M is constructed by a transfinite induction on the levels of the stratification. M is both supported and minimal, but need not be the only model with these two properties. For stratified programs, Lifschitz ([31]) showed that M could be specified declaratively using prioritized circumscription. Again by adapting a notion about predicates to individual values, Przymusinski defined the notion of perfect model based on such priorities, and showed that M is the unique \underline{Herbrand} perfect model for a locally stratified program. Subsequently Gelfond and Lifschitz showed that M is the unique stable model of such a program as well ([19]). This relation has prompted further examination of how the nature of recursion through negation in a program is reflected in its stable model structure [64, 48].

Yet another scheme for performing nonmonotonic reasoning makes use of modal formulas to identify conditions which are in some way “less than definite.” In the modal nonmonotonic logics of McDermott and Doyle [44], the modal operator is viewed as expressing consistency as distinguished from logical consequence; in Moore’s autoepistemic logic [46], it represents belief as distinct from knowledge. McDermott and Doyle proposed that a theory T (consisting of modal formulas) should be considered as an appropriate set of inferences from a given initial theory I (also consisting of modal formulas) if T is a fixed point of the operator

F : S ↦ Cn(I ∪ {Mφ : ¬φ ∉ S})

where Cn(A) stands for the collection of sentences derivable from A by the inference rules of first–order logic; that is, if T satisfies the equation

T = Cn(I ∪ {Mφ : ¬φ ∉ T }).

This can be restated in terms of the dual operator, which in later developments became standard, as

T = Cn(I ∪ {¬Lφ : φ ∉ T }).

Such theories T should be considered to describe “typical” situations arising from I; as usual, the nonmonotonic consequences of I can then be defined as the intersection of all such fixed points. Moore’s proposal, based on the reasoning of an agent capable of positive as well as negative introspection, selected a different set of theories as intended models, namely the solutions of the equation

T = Cn(I ∪ {Kφ : φ ∈ T } ∪ {¬Kφ : φ ∉ T }), which he called the autoepistemic expansions of I. It was later discovered that a spectrum of nonmonotonic logics, including autoepistemic logic, can be obtained by the McDermott–Doyle approach if first–order consequence is replaced by consequence in the sense of different modal logics, using modus ponens and necessitation as inference rules and various modal axiom schemas for simplification. An S–expansion, then, is any solution T of the equation

T = Cn_{S}(I ∪ {¬Lφ : φ ∉ T }),

where S is a specified set of modal axiom schemas which are permitted in derivations. Autoepistemic expansions, for instance, are S–expansions in the McDermott–Doyle sense, when S is any subset of {k, d, 4, 5} which includes the axiom 5 [59, 39]. Furthermore, under an appropriate translation of logic programming clauses into modal formulas, supported models correspond to this same type of S–expansion and stable models to S–expansions for which S is any subset of the axioms {k, t, 4, f} [38, 41]. (The axiom schemas named here can be found in standard texts on modal logic or in [41].)

Throughout the decade and a half since nonmonotonic reasoning systems were first introduced, there have been constant efforts to relate the proposals one to another. In [34, 36], Marek, Nerode, and Remmel abstracted common features of several proposals to form a theory of nonmonotonic rule systems. This framework emphasized the principles of context–directed reasoning and intended models. As intended, results obtained in this general setting could be applied to systems of different sorts after appropriate translation. In fact the translation between nonmonotonic rule systems and propositional logic programs is so direct that logic programming itself may be considered as an appropriate setting for general investigations into nonmonotonic reasoning. Propositional general logic programs provide perhaps the most basic structure in which deduction involving negation can be represented. Programs with more complicated syntax—programs with classical negation, disjunctive logic programs, clausal logic programs, programs with infinite sets of negative conditions, and of course predicate logic programs—have been and continue to be studied as vehicles for more complex types of nonmonotonic reasoning.

In summary, the systems surveyed above, though motivated by a variety of intuitions and expressed in an assortment of formalisms, appear at this point to be realizations of three basic modes of nonmonotonic reasoning, identified in the setting of logic programming with minimal, supported, and stable models. Each gives meaning to a particular notion of “typical” or “generic” by restricting attention to models with some sort of “local” or “context–dependent” closed–world property: that is, to models in which no positive atomic fact holds unless it follows in an appropriate sense from information about the model itself. Thus a minimal model of program P, defined above as a set S ⊆ U which is a model of P and for which no proper subset is a model of P, has the property that every positive atomic fact which holds in S follows in the logical sense from the clauses of P together with the negative atomic facts that hold in S. (For if a ∈ S is not a logical consequence of P ∪ {¬b : b ∈ U and S ⊧ ¬b}, then S−{a} contains a model of P.) Stable and supported models are defined using not the full logical inference involved in minimal models, but only what we may call “clausal inferences” in which the head of a clause is deduced from the conjuncts in the body. A stable model of P, defined formally as a set S for which S = T_{GL(S,P)} ↑ ω(∅), has the property that each positive atomic fact that holds in S follows by clausal inferences (in finitely many steps) from the negative atomic facts that hold in S. Such use of local negative information is sometimes called “negative introspection.” A supported model of P, defined above as a set S for which S = T_{P} (S), has the property that each positive atomic fact true in S follows by a clausal inference from the negative \underline{and} the positive atomic facts that hold in S—that is, using both negative and positive introspection. In this case, using a single inference is no more restrictive than allowing derivations of greater length, since any atom occurring in the body of a clause that can be obtained by an intermediate derivation is already available by positive introspection.

As understood now, the inferences produced from an initial theory or program by a given nonmonotonic reasoning system are based on its intended models. Under the so–called “skeptical” approach followed in most systems, the inferences are taken to be the sentences true in all intended models. Sometimes individual intended models are considered to define alternate sets of inferences. In certain systems the scope of application is restricted to specified theories which admit a unique canonical model used to determine the inferences. Though for some systems the set of inferences is computationally complex, in others an efficient proof procedure is provided.

In this thesis we will give mathematical characterizations of the sets of minimal, stable, and supported models determined by programs. (We will review the definitions for these models in Section 1.4 when we discuss the characterization problem specifically.) By characterizing these sets we determine what certain logic programming semantics are capable of reasoning about. By appropriate translation, the results apply also to other nonmonotonic reasoning systems besides logic programming.

An important development not previously mentioned is the use of three–valued or partial models for logic programs. As in the two–valued case, different sorts of intended models have been proposed in accordance with different intuitions. These include generalizations of supported, perfect, and stable models. While the present paper applies only to classes of two–valued models, it would be interesting to compare these results with a similar analysis for classes of three–valued models.

1.3 Topological background

Though of only recent application in logic programming, ideas from topology have often appeared in logical investigations of other sorts. Topology is relevant to logic because convergence of some sort underlies many constructions. As in the present paper, this usually involves a space consisting of interpretations for formulas, with a topology determined by the structure of the logic. For first–order logic, the Cantor topology (defined later in this section) on a collection of sets is the appropriate structure. Some of the most basic existence results for first–order logic (the completeness theorem, the downward Lowenheim–Skolem theorem, the omitting types theorem) can be obtained by the Baire category theorem in a space of this type ([52]). Morley’s theory about rank of 1-types is based on isolated points of such a space (see [57]). On the other hand, the arithmetic and analytical hierarchies of recursion theory provide a logical analogue of the Borel and projective hierarchies for spaces of this sort ([1]).

Topology has been applied outside the scope of classical first–order logic as well. For intuitionistic logic and for a type of modal logic, suitable algebraic structures can be produced from sets in a given topological space (see [28]). A similar approach occurs in the Boolean–valued models method for proving independence results in set theory (see [56]).

A topological approach to logic programming was introduced by Batarekh ([7]), who studied the immediate consequence operator T_{P} for a general logic program P as a continuous function on a topological space. As part of this investigation, she examined and compared several possible topologies on the space of interpretations of logic programs, including the Scott and inverse–Scott topologies borrowed from domain theory. The main results, however, which concern the existence of fixed points or of unique fixed points of T_{P} , are based on the application of contraction theorems to the space of interpretations under the Cantor topology ([7], [6]). Fitting ([18]) showed how these results can be applied modularly to gain information about portions of programs not covered by the basic results. Recently Khamsi, Kreinovich, and Misane ([24]) extended this approach to disjunctive logic programs by proving a generalization of the Banach contraction principle appropriate to this case.

The complexity of various sets connected with logic programming has been considered in a number of studies, both in terms of the polynomial hierarchy for finite programs (for example [12], [22], [40], [58]) and of the arithmetic or analytical hierarchies for arbitrary programs (for example [2], [4], [9], [37], [35]). In particular it was shown in [36] that, for a given program P, the class of models of P is Π_{1}^{0} in P, and the classes of minimal, stable, and supported models of P are all Π_{2}^{0} in P —that is, given P as a parameter, its class of models is an effective closed subset and its classes of minimal, stable, and supported models are effective G_{δ} subsets of the space of interpretations with the Cantor topology. Furthermore, every closed set in this space was shown to be a model class for some program. In [14], the present author showed similar results for a generalization of logic programming permitting clauses with infinitely many negative literals, with respect to a topology on 2^{U} introduced several years earlier by Ellentuck [13]. As with the results of [36] for the classical case, only the classes of models of programs are fully characterized by these results. In the present paper, returning to classical logic programs, the author uses the inverse–Scott topology in addition to the Cantor topology on 2^{U} to find exact characterizations for minimal, stable, and supported model classes as well.

In the remainder of this section we define and discuss the properties of the Cantor and inverse–Scott topologies on a set 2^{U}, which in the next section will be specified as the set of interpretations of propositional logic programs over U. We will refer back to this section as needed later on in proofs or examples.

Let U be a nonempty finite or countably infinite set. The Cantor topology on 2^{U}, denoted by (2^{U}, Cantor), is generated by a basis consisting of all sets of the form

{S ∈ 2^{U} : A⃗ ∈ S ∧ B⃗ ∉ S}

for A and B finite, possibly empty, subsets of U. This is of course homeomorphic to the product topology on the set of functions from U to {0, 1} with the discrete topology on each factor {0, 1}. As a product of spaces which are Hausdorff and compact, the space (2^{U}, Cantor) has these properties as well. Note that each basis element specified above is both open and closed. For U = ω, the Borel and projective hierarchies of (2^{ω}, Cantor) are familiar from descriptive set theory, and furthermore were shown in [1] to be related to the arithmetic and analytical hierarchies of recursion theory as follows:

Open  ≡ Σ_{1}^{0}[2^{ω}]
Closed  ≡ Π_{1}^{0}[2^{ω}]
G_{δ}  ≡ Π_{2}^{0}[2^{ω}]
F_{σ}  ≡ Σ_{2}^{0}[2^{ω}]
etc.
Analytic  ≡ Σ_{1}^{1}[2^{ω}]
Co − analytic ≡ Π_{1}^{1}[2^{ω}]
etc.

The inverse–Scott topology on 2^{U}, denoted by (2^{U}, Scott^{−1}), is generated by a basis consisting of all sets of the form

{S ∈ 2^{U} : B⃗ ∉ S}

for B a finite, again possibly empty, subset of U. A basic \underline{closed} set, then, has the form

{S ∈ 2^{U} : ⋁_{a∈A} a ∈ S}

for A a finite (possibly empty) subset of U. Note that every set which is open according to this definition is open in the Cantor sense as well—that is, the Cantor topology is a refinement of the inverse–Scott topology. The inverse–Scott topology also can be obtained as the product of factors {0, 1}, in this case with {∅, {0}, {0, 1}} as the topology on each factor. An essential feature of this topology is that, with respect to the partial order ⊆ on elements of the space, open sets are “lower closed” (that is, if G is open, S ∈ G, and S′ ⊆ S, then S′ ∈ G) and closed sets are “upper closed” (if F is closed, S ∈ F, and S′ ⊇ S, then S′ ∈ F). We note that the only open set to which U belongs is {S : ⋀_{b∈∅} b ∉ S} = 2^{U}; equivalently, U belongs to every closed set except ∅. Similarly the empty subset of U is an element of every open set except ∅; the only closed set to which it belongs is 2^{U} itself. It is also important to note that, if U is infinite, then there are sets which are lower closed which are not open. For instance, if U = ω, the set consisting of all subsets of even numbers is lower closed but is not an open set. We note for later use in Example 2.1 that likewise the set {∅} consisting of the empty subset of U is lower closed but not open, and its complement 2^{U} − {∅} is upper closed but not closed, whenever U is infinite.

In contrast to the Cantor space, much about the inverse–Scott space runs counter to intuition. For one thing, its Borel hierarchy is not analogous to the arithmetic hierarchy; a closed set, for instance, generally is not G_{δ}. The situation is much worse, however. The space is not Hausdorff (that is, T_{2})—in fact does not even satisfy the weaker (that is, T_{1}) requirement that singleton sets be closed—so convergence does not work as expected. Indeed, if a sequence converges to a point S, then it converges also to every point S′ ⊇ S. Surprising as this may seem at first, it makes sense in the context of information, where S is regarded as a refinement of every S′ ⊇ S. In fact, certain properties of operators important in logic programming concerning continuity in the lattice–theoretic sense appear to be features which are well–known from study of this topology in domain theory.

For S ⊆ 2^{U}, we will denote the closure of S in (2^{U}, Cantor) by S̄ and the closure of S in (2^{U}, Scott^{−1}) by S̃.

1.4 The characterization problem

Having introduced the subject of intended models of logic programs and presented a topological setting where it can be studied, we can now describe in mathematical terms the topic of our investigation. We will show what aspects of the problem were known previously and mention other contributions that were helpful to its solution. In particular at this point we state some theorems from other sources to be used in later chapters.

In this paper we will be concerned with propositional general logic programs over a finite or countably infinite set U of atoms, by which we mean programs consisting of a possibly infinite set of clauses of the form

c ← A⃗, ¬B⃗,

where c is an element of U and A and B are finite subsets of U. This includes the case in which the propositional program consists of all ground instances of a previously given \underline{predicate} logic program, with U in this case the Herbrand base of the original program.

By an interpretation for a propositional program P over a set U of atoms, we mean any subset of U. We distinguish the following special sorts of interpretations, connected with different kinds of nonmonotonic reasoning and different semantics for logic programming, as described in Section 1.2: A set S ⊆ U is a model of P if S is closed under application of the immediate consequence operator T_{P}; that is, if T_{P} (S) ⊆ S. S is a minimal model of P if S is a model of P and no proper subset of S is a model of P. S is a supported model of P if S is a fixpoint of T_{P}; that is, if S = T_{P} (S). And S is a stable model of P if S is the least fixpoint of the immediate consequence operator for GL(S, P), the program obtained from P by the Gelfond– Lifschitz transformation with respect to S; that is, if S = T_{GL(S,P)} ↑ ω(∅).

For a given program P, we let Mod(P), Min(P), Supp(P), and Stab(P) denote the sets of models, minimal models, supported models, and stable models, respectively, of P. We refer to S ⊆ 2^{U} as a model class if there is a program P for which S = Mod(P), and similarly for minimal, supported, and stable model classes. For each type of semantics, the collection of the appropriate intended model classes of all possible programs over U constitutes a concrete realization of what the semantics can express. The main topic of this paper is to determine the extent of these collections for minimal, supported, and stable model semantics—that is, to characterize which sets S ⊆ 2^{U} occur as minimal model classes, as supported model classes, and as stable model classes.

Given a set U of atoms, consider a space consisting of the subsets of U. Then for a propositional program P over U, the interpretations of P are the points of the space, and Mod(P), Min(P), Supp(P), and Stab(P) are particular subsets. In [36] it was observed that, as a subset of 2^{U}, Mod(P) is Π_{1}^{0} in P, so that as a subset of (2^{U}, Cantor), Mod(P) is closed. It was further noted that, regardless of P, the set U belongs to Mod(P). These two properties were then shown to characterize the subsets of 2^{U} which are model classes:

Theorem ([36]) (Characterization of model classes) A set S ⊆ 2^{U} is the model class of some program over U if and only if U ∈ S and S is a closed subset of (2^{U}, Cantor). Proof (summary): The set of models of the disjunction

⋁_{a∈A} ¬a ∨ ⋁_{b∈B} b

agrees with the basic closed subset

{S : ⋁_{a∈A} a ∉ S ∨ ⋁_{b∈B} b ∈ S}

of (2^{U}, Cantor). The condition B ≠ ∅ then corresponds both to the existence of a clause logically equivalent to the disjunction and to membership of U in the basic closed set. □

As mentioned in Section 1.3, it was also shown in [36] that the subsets Min(P), Supp(P), and Stab(P) of 2^{U} are each Π_{2}^{0} in P, and thus are G_{δ} subsets of (2^{U}, Cantor). Additionally, Min(P) is clearly an antichain—that is, no element is a subset of any other—and, as shown later in this section, the same is true for Stab(P). However, these properties are not sufficient to characterize any of these classes, as we will show by examples later in the paper.

The key to finding a full characterization was to retain the topological point of view that was ancillary to the recursion–theoretic complexity estimate, but to replace the Cantor by the inverse–Scott topology. This approach was suggested by the importance of negative information in determining minimality and stability. In particular, since the deduction related to stable models is based on absence of information (as discussed in Section 1.2), if convergence to a point is to occur by repeated deduction, then neighborhoods of interpretations should be determined by degree of agreement on absence of information. We are able to give a complete description of minimal and stable model classes in terms of the inverse–Scott topology, clarifying in the process the difference between the two. In keeping with this point of view, we find that the Cantor topology, which is appropriate for describing deduction based on both presence and absence of information, permits a similar characterization for supported model classes.

In each characterization theorem, one direction of the proof rests on a specification of the intended models of a given sort in terms of formulas derived from the program. The first example of such a description was Clark’s use of the completion of a program P to specify the intended models of P (which, as seen in Section 1.2, preceded and led to the fixpoint definition of supported models). For a propositional program P over U, the completion of P consists of the formulas

u ↔ ⋁_{(A,B)∈Σ_{u}}( ⋀_{a∈A} a ∧ ⋀_{b∈B} ¬b)  (1.2)

for u ∈ U, where Σ_{u} is the set of pairs (A, B) of finite subsets of U such that

u ← A⃗, ¬B⃗

is a clause of P. (Note that Σ_{u} is countable but not necessarily finite.) The supported models of P then are those sets S which satisfy the set Cmp_{P} of conditions

u ∈ S ↔ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)  (1.3)

for u ∈ U. In accordance with the later terminology of [36], these equivalences (1.3) may be called a set of defining equations for the supported models of P, since the corresponding formulas (1.2) may be considered as Boolean equations which are satisfied by those valuations which correspond to supported models. Alternately these conditions may be formulated as a sentence

⋀_{u∈U}[R(\underline{u}) ↔ ⋁_{(A,B)∈Σ_{u}}( ⋀_{a∈A} R(\underline{a}) ∧ ⋀_{b∈B} ¬R(\underline{b})],

denoted by cmp_{P} , of L_{ω_{1},ω}^{U} (in the language L^{U} consisting of a unary predicate symbol R and a constant symbol \underline{u} for each u ∈ U), with the property that (U, S, u⃗_{u∈U}) ⊧ cmp_{P} if and only if S is a supported model of P. In [36], this description of the supported models of P was used to show that the class Supp(P) is Π_{2}^{0} in P.

For stable models, a similar description in terms of formulas (rather than fixpoints) was given by Marek, Nerode, and Remmel in [36] and independently by Dung and Kanchanasut in [11]. As described in [36], a proof scheme from P for element u ∈ U consists of: (1) a finite sequence of clauses from P, with u as the head of the last clause, such that every positive literal in the body of a clause occurs as the head of some previous clause, and (2) a cumulative list of the negative literals occurring in these clauses, called the support of the proof scheme. For any set S ⊆ U, an element u ∈ U belongs to T_{GL(S,P)} ↑ ω(∅) (that is, u is S–provable) just in case S omits all the atoms in the support of some proof scheme for u. Then S is a stable model of P if and only if S satisfies the system of equivalences

u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S

for u ∈ U, where the sets A ∈ Ψ_{u} are the supports, or, better, the minimal supports, of proof schemes for U. (Again the disjunction may be countably infinite.) In [36] these equivalences were called defining equations for the stable models of P, because of the interpretation of

u ↔ ⋁_{A∈Ψ_{u}} ¬A⃗

for u ∈ U as Boolean equations. As before, these conditions may be formulated as a single sentence

⋀_{u∈U}[R(\underline{u}) ↔ ⋁_{A∈Ψ_{u}} ⋀_{a∈A} ¬R(\underline{a})],

denoted by σ_{P} , of L_{ω_{1},ω}^{U}, with the property that (U, S, u⃗_{u∈U}) ⊧ σ_{P} if and only if S is a stable model of P. This description of the stable models of P was used in [36] to show that the class Stab(P) is Π_{2}^{0} in P. We will use it to classify Stab(P) in (2^{U}, Scott^{−1}).

In this paper, we give a similar description of minimal models in terms of defining equations, which was not previously known. Indeed, our intent in characterizing minimal and stable model classes was to understand how negative information is involved in determining minimal models as compared with stable models. In the Extended Closed World Assumption of [21] (which was discussed in Section 1.2), the first–order sentences which hold on all minimal Herbrand models of a theory T were described in terms of a property called free for negation; in general, however, these sentences do not axiomatize the minimal Herbrand models of a program P if P is infinite. In [26], Kueker obtained an axiomatization for the minimal models of a theory T using infinitary formulas. In the setting of propositional logic programs, it is possible to understand the construction of these formulas in terms of program clauses (though generally not of the program as originally given). Reformulated as defining equations for minimal models, they provide a clear description of minimal models in terms of negative information, making possible a comparison then of minimal and stable model classes through the inverse–Scott topology.

We will make use throughout the paper of the relationships

Stab(P) ⊆ Supp(P)

and

Stab(P) ⊆ Min(P),

shown first by Marek and Subrahmanian ([38]) and Gelfond and Lifschitz ([19]), respectively. Here we give a brief proof of each, based on three lemmas which are direct consequences of the definitions:

Lemma For each program P and set S ⊆ U, T_{P} (S) = T_{GL(S,P)}(S).

Proof. u ∈ T_{P} (S)

⟺ there is a clause u ← A⃗, ¬B⃗ of P such that A⃗ ∈ S and B⃗ ∉ S

⟺ there is a clause u ← A⃗ of GL(S, P) such that A⃗ ∈ S

⟺ u ∈ T_{GL(S,P)}(S). □

Lemma If S ∈ Mod(P), then T_{GL(S,P)} ↑ ω(∅) ⊆ S.

Proof. By the first lemma and the hypothesis,

T_{GL(S,P)}(S) = T_{P} (S) ⊆ S.

The conclusion follows by the Knaster–Tarski Theorem. □

Lemma (Antimonotonicity) If S_{1} ⊆ S_{2}, then T_{GL(S_{2},P)} ↑ ω(∅) ⊆ T_{GL(S_{1},P)} ↑ ω(∅).

Proof. Since every clause of GL(S_{2}, P) also belongs to GL(S_{1}, P),

T_{GL(S_{2},P)}(S) ⊆ T_{GL(S_{1},P)}(S)

for any set S ⊆ U. In particular,

T_{GL(S_{2},P)}(T_{GL(S_{1},P)} ↑ ω(∅)) ⊆ T_{GL(S_{1},P)}(T_{GL(S_{1},P)} ↑ ω(∅)) = T_{GL(S_{1},P)} ↑ ω(∅),

so T_{GL(S_{1},P)} ↑ ω(∅) is a prefixpoint of T_{GL(S_{2},P)}. Since T_{GL(S_{2},P)} ↑ ω(∅) is the least fixpoint of T_{GL(S_{2},P)}, the conclusion follows by the Knaster–Tarski Theorem. □

We can now establish the two relationships:

Theorem ([38]) For each program P, Stab(P) ⊆ Supp(P).

Proof. Let S be a stable model of P. Then S is a fixpoint of the operator T_{GL(S,P)}. By the first lemma,

S = T_{GL(S,P)}(S) = T_{P} (S). □

Theorem ([19]) For each program P, Stab(P) ⊆ Min(P).

Proof. Let S be a stable model of P. As shown in the preceding theorem, S = T_{P} (S), so in particular S is a model of P. To show that S is minimal, let S′ be a model of P such that S′ ⊆ S. Then

S =^{def} T_{GL(S,P)} ↑ ω(∅)
⊆ T_{GL(S′,P)} ↑ ω(∅)
⊆ S′

by the last two lemmas, as desired. □

As mentioned earlier, this shows the following property for Stab(P) : Corollary For each program P, Stab(P) is an antichain. Proof. By the previous theorem. □

In the final chapter we extend the characterization theorems found earlier to a wider class of logic programs, those formed using classical negation in addition to default or other nonmonotonically determined negation. That is, we consider sets S ⊆ 2^{U} for which the related set h(S) is representable in the sense of the earlier theorems by programs over U ∪ U̇, where U̇ = {u̇ : u ∈ U} is a distinguished copy of U and h : 2^{U} → 2^{U∪U̇} is defined by

h : S ↦ S ∪ {u̇ : u ∉ S}.

Since h transforms any set S ⊂ 2^{U} to an antichain as a subset of U ∪ U̇, representability using minimal or stable models is extended to sets which are not antichains. This technique first appeared in [34], where the set of prime ideals of a commutative ring with unit was shown to be representable as a stable model class in this sense. In [36] the same transformation appeared in a proof that the Turing degrees of elements of closed subsets of (2^{U}, Cantor) match the degrees of stable models of programs with the finite proof support property (considered in Chapter 4), thus allowing results about the degree structure of Π_{1}^{0} sets to be transferred to these stable model classes. In this paper we separate the study of the finite proof support property from that of the transformation h, in order to understand how each contributes to the complexity result above. Though it turns out that, among antichains, the sets S ⊆ 2^{U} which are representable as the stable models of a finite proof support program are the same as those for which h(S) is so representable, our caution is perhaps justified by the failure of similar statements for minimal, stable, and supported models.

MINIMAL MODEL CLASSES

As discussed in Section 1.4, in this chapter we will show that minimal model classes of programs over U can be characterized in terms of the inverse–Scott topology on 2^{U}. The result will be based on a relation between model classes and certain subsets of (2^{U}, Scott^{−1}). Recall from Section 1.4 that, by a theorem of [36], model classes of programs over U are characterized as the closed subsets of (2^{U}, Cantor) to which U belongs. The subsets of 2^{U} which are closed in the coarser inverse–Scott topology have a similar significance with respect to a special subclass of programs:

Theorem 2.1 A set S ⊆ 2^{U} is the model class of some prerequisite–free program if and only if S is nonempty and closed in the inverse–Scott topology.

Proof: ⇒ Let P be a prerequisite–free program such that S = Mod(P). Then

S = {S : for every clause ρ in P, S ⊧ ρ}
= ⋂_{ρ∈P}{S : S ⊧ ρ}.

So it suffices to show that, for any clause ρ, U ⊧ ρ and {S : S ⊧ ρ} is closed in the inverse–Scott sense. Suppose that ρ has the form

c ← ¬B⃗ for B a finite, possibly empty, subset of U. Then

{S : S ⊧ ρ} = {S : S ⊧ ( ⋀_{b∈B} ¬b) → c}
= {S : S ⊧ c ∨ ⋁_{b∈B} b}
= {S : c ∈ S ∨ ⋁_{b∈B} b ∈ S},

which is a basic closed set in the inverse–Scott topology. Since c ∈ U, U ⊧ ρ. ⇐ Suppose that S is nonempty and that S = ⋂_{i∈I} S_{i}, where each S_{i} is a basic closed set in the inverse–Scott topology. We will show that for each i there is a prerequisite–free clause ρ_{i} such that S_{i} = {S : S ⊧ ρ_{i}}. Let ≤ be an ordering on U of type ω. Suppose that the basic closed set S_{i} has the form

{S : ⋁_{b∈B} b ∈ S}

for B a finite subset of U. Since S_{i} is nonempty, B must be nonempty as well. Let c be the greatest element of B with respect to the ordering ≤ . Then

S_{i} = {S : c ∈ S ∨ ⋁_{b∈B−{c}} b ∈ S}
= {S : S ⊧ c ∨ ⋁_{b∈B−{c}} b}
= {S : S ⊧ ( ⋀_{b∈B−{c}} ¬b) → c}
= {S : S ⊧ ρ_{i}},

where ρ_{i} is the clause c ← ¬\overline{(B − \{c\})}. Finally let P be the prerequisite–free program consisting of {ρ_{i} : i ∈ I}. Then S = Mod(P). □

Next we consider some general facts about closed subsets of (2^{U}, Cantor) and (2^{U}, Scott^{−1}) and their minimal elements: Proposition 2.1 For nonempty S ⊆ 2^{U} :

(a) min S = min S^{⊇}. In fact, min S = min X for any X with S ⊆ X ⊆ S^{⊇}.

(b) S = min S if and only if S is an antichain.

Proof: Straightforward.

Proposition 2.2 If F ⊆ 2^{U} is closed in the Cantor topology, then F^{⊇} is closed in the inverse–Scott topology.

Proof: Suppose that R ∉ F^{⊇}. We will find a neighborhood B of R in (2^{U}, Scott^{−1}) such that B ∩ F^{⊇} = ∅.

For each u ∈ U, let

B_{u} = {S : u ∉ S}.

Then S ∈ ⋂_{u∉R} B_{u} if and only if S ⊆ R. For each S ∈ F, therefore, S ∉ ⋂_{u∉R} B_{u}; that is,

F ∩ ⋂_{u∉R} B_{u} = ∅.

Now in (2^{U}, Cantor), each B_{u}, as well as F, is closed. So by compactness there is some finite Q ⊆ (U − R) such that

F ∩ ⋂_{u∈Q} B_{u} = ∅.

In (2^{U}, Scott^{−1}), ⋂_{u∈Q} B_{u} is an open set, and clearly R ∈ ⋂_{u∈Q} B_{u}. Because ⋂_{u∈Q} B_{u} is lower closed, no element of F^{⊇} can belong to ⋂_{u∈Q} B_{u}; that is,

F^{⊇} ∩ ⋂_{u∈Q} B_{u} = ∅.

So we may take B = ⋂_{u∈Q} B_{u}. □

Proposition 2.3 For S ⊆ 2^{U}, \overline{(S^{⊇})} = (S̄)^{⊇} = S̃.

Proof: We will show that \overline{(S^{⊇})} ⊆ (S̄)^{⊇} ⊆ S̃ ⊆ \overline{(S^{⊇})}. [To show \overline{(S^{⊇})} ⊆ (S̄)^{⊇}] Because S ⊆ S̄, S^{⊇} ⊆ (S̄)^{⊇}. Since S̄ is closed in (2^{U}, Cantor), by Proposition 2.2 (S̄)^{⊇} is closed in the inverse–Scott sense, and hence also in the Cantor sense. Therefore \overline{(S^{⊇})} ⊆ (S̄)^{⊇}.

[To show (S̄)^{⊇} ⊆ S̃] We have S̄ ⊆ S̃ because S̃ is closed in the Cantor sense. Since S̃ is closed under taking supersets, (S̄)^{⊇} ⊆ S̃. [To show S̃ ⊆ \overline{(S^{⊇})}] Let Y ∈ S̃. We wish to show that Y ∈ \overline{(S^{⊇})}. So let

O = {S : A⃗ ∈ S ∧ B⃗ ∉ S}

be a basic open subset of (2^{U}, Cantor) such that Y ∈ O. We will show that O∩S^{⊇} ≠ ∅.

Let O′ be the set {S : B⃗ ∉ S}. Since Y ∈ S̃, and O′ is a basic open subset of (2^{U}, Scott^{−1}) to which Y belongs,, there is a set Z ∈ O′ such that Z ∈ S. Then the set Z ∪ A is an element of both O and S^{⊇}, as desired. □

Lemma 2.1 If F ⊆ 2^{U} is closed in the Cantor topology, then for all X ∈ F there exists X′ ⊆ X such that X′ is a minimal element of F.

Proof: Let X ∈ F. We apply Zorn’s Lemma to the set P_{X} = {X′ ∈ F : X′ ⊆ X} with order relation < given by {⊃ \atop ≠} .

Let X_{1} {⊃ \atop ≠} X_{2} {⊃ \atop ≠} … be a chain in P_{X}. Let Y = ⋂ X_{i}. Clearly Y {⊂ \atop ≠} X_{i} for each i, and Y ⊆ X. Since F is closed, we also have that Y ∈ F. So Y is an upper bound (in the sense of <) for the given chain. By Zorn’s Lemma, P_{X} has a <-maximal element X′.

X′ is then ⊆-minimal with respect to P_{X}. But if S ⊆ X′ for any S ∈ F, then S ∈ P_{X}, so X′ is a minimal element of F. □

Theorem 2.2 (Characterization of minimal model classes) For nonempty S ⊆ 2^{U}, the following are equivalent:

(i) S is a minimal model class. (ii) S is an antichain and S^{⊇} is inverse–Scott closed. (iii) S = min S̃.

(iv) S = min S̄. Proof:

(i) ⇒ (ii) It is clear that S is an antichain. To see that S^{⊇} is closed, let P be a program such that S = Min(P) = min Mod(P), and let F = Mod(P). By the model class characterization result of [36], F is closed in the Cantor topology. By Proposition 2.2, F^{⊇} then is closed in the inverse–Scott topology. We show that S^{⊇} = F^{⊇} : Since S ⊆ F, S^{⊇} ⊆ F^{⊇}. For the other inclusion, the preceding lemma says that F ⊆ S^{⊇}, which then implies F^{⊇} ⊆ S^{⊇}. Therefore S^{⊇} is an inverse–Scott closed set.

(ii) ⇒ (iii) Since S^{⊇} is closed, S̃ = S^{⊇} by Proposition 2.3. Then min S̃ = min S^{⊇} = min S = S by Proposition 2.1(a) and (b).

(iii) ⇒ (iv) By Proposition 2.3, S̃ = (S̄)^{⊇}. So S = min S̃ = min (S̄)^{⊇} = min S̄, by Proposition 2.1(a).

(iv) ⇒ (i) By the model class characterization theorem of [36], S̄ ∪ {U} is the collection of models of some program P. Since S is nonempty, S = min S̄ = min(S̄ ∪ {U}) = min Mod(P) = Min(P). □

By way of this theorem, we can now present an example to show that the G_{δ} and antichain properties mentioned in the introduction are too broad to characterize minimal model classes: Example 2.1 Let S = {{u_{0}}, {u_{1}}, {u_{2}}, …}, where U = {u_{0}, u_{1}, u_{2}, …}. We note that S is both an antichain and a G_{δ} subset in (2^{U}, Cantor). But condition (iv) of the theorem, namely S = min S̄, fails because ∅ ∈ S̄, and therefore S is not a minimal model class. Alternately, we can check, as in condition (ii), that

S^{⊇} = {S : u_{0} ∈ S ∨ u_{1} ∈ S ∨ u_{2} ∈ S ∨ …} = 2^{U} − {∅},

which, as observed in Section 1.3, is not closed in (2^{U}, Scott^{−1}). □

By the same approach, we can also recognize whether a given set can be even a subset of some minimal model class:

Theorem 2.3 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a subset of a minimal model class. (ii) S ⊆ min S̃. (iii) S ⊆ min S̄.

Proof:

(i) ⇒ (ii) Let P be a program such that S ⊆ Min(P), as in (i), and let F = (Mod(P))^{⊇}. Then

S = S ∩ Min(P)
= S ∩ min F
⊆ S̃ ∩ min F
⊆ min S̃,

where the last inclusion follows because S̃ ⊆ F. (ii) ⇒ (iii) We are given that S ⊆ min S̃. Then

S = S ∩ min S̃
⊆ S̄ ∩ min S̃
⊆ min S̄,

where the last inclusion follows because S̄ ⊆ S̃. (iii) ⇒ (i) We are given that S ⊆ min S̄. Even when S = ∅, min S̄ ⊆ min(S̄ ∪ {U}). By the model class characterization theorem of [36], S̄ ∪ {U} is the class of models of some program. □

Example 2.2 Let S = {{u_{0}}, {u_{1}}, {u_{2}}, …} be the set of the previous example. As observed before, min S̄ = {∅}, so S ⊈ min S̄. Therefore not only is S itself not a minimal model class, but by condition (i) no set containing S can be a minimal model class either. □

In addition to the characterization theorem, the propositions above also produce a useful representation result for minimal model classes:

Theorem 2.4 (Prerequisite–free representation) For any program P there is a prerequisite–free program P′ which has the same minimal models as P.

Proof: By the model class theorem of [36], Mod(P) is a nonempty closed subset F of (2^{U}, Cantor). By Proposition 2.2, F^{⊇} is closed in (2^{U}, Scott^{−1}). By Theorem 2.1 then F^{⊇} = Mod(P′) for some prerequisite–free P′. Proposition 2.1(a) says that F and F^{⊇} have the same minimal elements. Thus Min(P) = min Mod(P) = min F = min F^{⊇} = min Mod(P′) = Min(P′). □

Remark 2.1 Later in the chapter we will give procedures (Algorithms 2.2 and 2.3) for finding a canonical prerequisite–free program representing a given minimal model class.

To study minimal model classes, then, it is enough to study the minimal models of programs which are prerequisite–free, or, equivalently, the minimal elements of sets which are inverse–Scott closed. We show next how to describe these minimal elements of closed sets in terms of the closed–set structure:

Proposition 2.4 Let F = ⋂_{C∈C}C be a nonempty closed subset of 2^{U} in the inverse– Scott topology, where each C ∈ C is a basic closed set of the form C = {S : ⋁_{y∈P_{C}} y ∈ S} for P_{C} a finite, nonempty subset of U. (We permit C = ∅ in order to include F = 2^{U} as a possibility.) Let

M = {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{u∈P_{C}^{C∈C,}} ⋀_{y≠u^{y∈P_{C} ,}} y ∉ S]}.

Then M is the set of minimal elements of F.

Proof: [To show: M ⊆ min F] Let S′ ∈ M. To show that S′ ∈ min F, we will show that (a) S′ ∈ F, and (b) no proper subset of S′ belongs to F.

(a) Let

C′ = {S : ⋁_{y∈P_{C′}} y ∈ S}

be an element of C, and let u′ ∈ P_{C′} (since P_{C′} is nonempty). Because S′ ∈ M,

( ⋀_{y≠u′^{y∈P_{C′} ,}} y ∉ S′) → u′ ∈ S′,

or equivalently

⋁_{y∈P_{C′}} y ∈ S′.

Therefore S′ ∈ C′, as desired.

(b) Let A ∈ F, with A ⊆ S′. To show that S′ ⊆ A, let a ∈ S′. Because

a ∈ S′ → ⋁_{a∈P_{C}^{C∈C,}} ⋀_{y≠a^{y∈P_{C} ,}} y ∉ S′,

(since S′ ∈ M), there is some C ∈ C with a ∈ P_{C} such that S′ ∩ (P_{C} − {a}) = ∅. Then A ∩ (P_{C} − {a}) = ∅ as well. But A ∩ P_{C} ≠ ∅ since A ∈ F, and therefore a ∈ A, as desired.

[To show: min F ⊆ M] Let S′ ∈ min F, and let u′ ∈ U. To show that S′ ∈ M, it will suffice to show that

u′ ∈ S′ ↔ ⋁_{u′∈P_{C}^{C∈C,}} ⋀_{y≠u′^{y∈P_{C} ,}} y ∉ S′.

(←) Since S′ ∈ F,

⋀_{C∈C} ⋁_{y∈P_{C}} y ∈ S′

and in particular

⋀_{u′∈P_{C}^{C∈C,}}(u′ ∈ S′ ∨ ⋁_{y≠u′^{y∈P_{C} ,}} y ∈ S′).

Therefore

u′ ∈ S′ ∨ ⋀_{u′∈P_{C}^{C∈C,}} ⋁_{y≠u′^{y∈P_{C} ,}} y ∈ S′,

which is equivalent to

( ⋁_{u′∈P_{C}^{C∈C,}} ⋀_{y≠u′^{y∈P_{C} ,}} y ∉ S′) → u′ ∈ S′.

(→) Suppose that

⋀_{u′∈P_{C}^{C∈C,}} ⋁_{y≠u′^{y∈P_{C} ,}} y ∈ S′.

Since S′ ∈ F,

S′ ∩ P_{C} ≠ ∅

for each C ∈ C. For sets C such that u′ ∉ P_{C}, then,

(S′ − {u′}) ∩ P_{C} = S′ ∩ P_{C} ≠ ∅.

For sets C on the other hand such that u′ ∈ P_{C}, by the assumption above

S′ ∩ (P_{C} − {u′}) ≠ ∅,

and hence for this case as well

(S′ − {u′}) ∩ P_{C} ≠ ∅.

This shows that (S′ − {u′}) ∈ F. Since S′ is a minimal element of F,

S′ ⊆ (S′ − {u′}).

Therefore u′ ∉ S′, as desired. □

We can now apply this result to get a useful description of the minimal models of a logic program in terms of a system of “defining equations:”

Theorem 2.5 (Defining equations for minimal models) Let P be a general logic program over U. For each u ∈ U, there is a countable (possibly empty) collection Φ_{u} of finite (possibly empty) sequences A from U, such that

Min(P) = {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Φ_{u}} ⋀_{a∈A} a ∉ S]}.

Proof: Let P′ be a prerequisite–free program with the same minimal models as P. Fix an expression for Mod(P′) as an intersection of basic closed sets in (2^{U}, Scott^{−1}) corresponding to the clauses of P′. Then the system of equivalences formed as in the preceding proposition characterizes the minimal elements of Mod(P′). Following the notation of the preceding proposition, for each u ∈ U, let Φ_{u} consist of those sets P_{C} − {u} for which u ∈ P_{C}. Then

Min(P) = Min(P′) = min Mod(P′)

= {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Φ_{u}} ⋀_{a∈A} a ∉ S]}.

□

Just as for the sentence σ in the case of stable models, we may formulate the defining equations for the minimal models of P as a sentence μ =

⋀_{u∈U}[R(\underline{u}) ↔ ⋁_{A∈Φ_{u}} ⋀_{a∈A} ¬R(\underline{a})]

of L_{ω_{1},ω}^{U} (in the language L^{U} consisting of a unary predicate symbol R and a constant symbol \underline{u} for each u ∈ U), with the property that (U, S, u⃗_{u∈U}) ⊧ μ if and only if S is a minimal model of P. For convenience, we shall often use the symbol μ to refer to the conditions on a set S entailed by having (U, S, u⃗_{u∈U}) ⊧ μ. As with stable models, the role of negative information in specifying minimal models is made particularly apparent by the defining equations. By analogy with the stable model case, where the elements of Ψ_{u} are the supports of proof schemes in P for u, we refer to the elements of Φ_{u} as “supports” of u in the clauses of the associated program P′.

We illustrate the notion of supports and the formation of the sentence μ using a prerequisite–free program of the simplest sort as an example:

Example 2.3 Let U = {a, b, c, d, e} and let P be the program

a ← ¬b
b ← ¬c
c ← ¬d
d ← ¬e.

As in Theorem 2.1, we express Mod(P) as an intersection of sets determined by the clauses of P, and recall, because P is prerequisite–free, that each is basic closed in (2^{U}, Scott^{−1}) :

Mod(P) = F_{1} ∩ F_{2} ∩ F_{3} ∩ F_{4}, where
F_{1} = {S : a ∈ S ∨ b ∈ S}
F_{2} = {S : b ∈ S ∨ c ∈ S}
F_{3} = {S : c ∈ S ∨ d ∈ S}
F_{4} = {S : d ∈ S ∨ e ∈ S}.

For the element a ∈ U, which occurs only in the first clause, the support of a in F_{1} is {b}, so the defining equation for a is

a ∈ S ↔ b ∉ S.

For b ∈ U, the support of b in F_{1} is {a} and the support of b in F_{2} is {c}, so the defining equation for b is

b ∈ S ↔ a ∉ S ∨ c ∉ S.

The defining equations for c, d, and e are formed similarly, so the condition determining minimal models S is

(a ∈ S ↔ b ∉ S)
∧ (b ∈ S ↔ a ∉ S ∨ c ∉ S)
∧ (c ∈ S ↔ b ∉ S ∨ d ∉ S)
∧ (d ∈ S ↔ c ∉ S ∨ e ∉ S)
∧ (e ∈ S ↔ d ∉ S).

Formally the sentence μ in the language L^{U} has the form

[R(\underline{a}) ↔ ¬R(\underline{b})]

∧ [R(\underline{b}) ↔ ¬R(\underline{a}) ∨ ¬R(\underline{c})]
∧ [R(\underline{c}) ↔ ¬R(\underline{b}) ∨ ¬R(\underline{d})]
∧ [R(\underline{d}) ↔ ¬R(\underline{c}) ∨ ¬R(\underline{e})]
∧ [R(\underline{e}) ↔ ¬R(\underline{d})],

but we will generally bypass the formal statement and display as μ the preceding conjunction of equivalences. Thus the minimal models of P are

M = {{a, c, d}, {a, c, e}, {b, c, e}, {b, d}}. □

Next we will examine more specifically how programs, their minimal models, and their associated prerequisite–free programs are related. We develop from this a procedure which in many cases will allow us to find the sentence μ and the minimal models for more complicated programs. This will also give us the means to find a prerequisite–free program with the same minimal models as a given program, or indeed with some specified set M as its minimal models, provided M satisfies the conditions of a minimal class established in Theorem 2.2.

First we will present a series of lemmas to guide and then justify the procedures. The first lemma suggests a course by which minimal models can be recognized:

Lemma 2.2 Let F ⊆ 2^{U}. Suppose that F^{⊇} = X^{⊇}, where X ⊆ 2^{U} is an antichain. Then

min F = X .

Proof: By Proposition 2.1, min F = min F^{⊇} = min X^{⊇} = min X = X . □

The next lemma contains a prescription for a prerequisite–free program. We use the notation Fin(U) to stand for the collection of finite subsets of U.

Lemma 2.3 Let S ⊆ 2^{U}. Let

Δ = {B ∈ Fin(U) : for all S ∈ S, B ∩ S ≠ ∅}.

Then

S̃ = ⋂_{B∈Δ}{S : B ∩ S ≠ ∅}.

Proof: Let C_{B} denote the basic closed subset {S : B ∩ S ≠ ∅} of (2^{U}, Scott^{−1}). Then

S̃ = ⋂{C_{B} : B ∈ F in(U) and S ⊆ C_{B}}
= ⋂{C_{B} : B ∈ F in(U) and for all S ∈ S, B ∩ S ≠ ∅}
= ⋂{C_{B} : B ∈ Δ}
= ⋂_{B∈Δ}{S : B ∩ S ≠ ∅}.

□

The last of the lemmas will be used to pick a simplest representative among suitable prerequisite–free programs:

Lemma 2.4 If Z ⊆ F in(U), then

⋂_{B∈Z}{S : B ∩ S ≠ ∅} = ⋂_{B∈min Z}{S : B ∩ S ≠ ∅}.

Proof: (⊆) Immediate. (⊇) Let S ∈ ⋂_{B∈min Z}{S : B ∩ S ≠ ∅}, and let B ∈ Z. It will suffice to show that B ∩ S ≠ ∅. Since B is finite, there is some B′ ⊆ B such that B′ ∈ min Z. Then B ∩ S ⊇ B′ ∩ S ≠ ∅. □

Before presenting the procedures, we will establish a uniqueness result of a sort for prerequisite–free programs representing a given minimal model class. We will say that a disjunction φ of literals subsumes another such disjunction ψ if every literal of φ appears in ψ. We say that φ subsumes a clause ρ if φ subsumes the disjunction which is logically equivalent to ρ. The following proposition will show that, for each minimal model class S ⊆ 2^{U}, there is a theory Π_{S} consisting of finite disjunctions of positive atoms, with S as its minimal models, such that every prerequisite–free program P with Min(P) = S contains clauses logically equivalent to each member of Π_{S} and furthermore every clause of such a program P is subsumed by some element of Π_{S}.

To simplify the statement of the proposition, let At(ρ) be the set of atoms which occur in the clause ρ, and let the set Core(P), where P is a prerequisite–free program, consist of the minimal elements of {At(ρ) : ρ ∈ P }.

Proposition 2.5 Given a minimal class S, let

Δ = {B ∈ Fin(U) : for all S ∈ S, B ∩ S ≠ ∅}

and

Θ = min Δ.

Then for every prerequisite–free program P, Min(P) = S if and only if Core(P) = Θ.

Proof: (⇐) Suppose that P is a prerequisite–free program such that Core(P) = Θ. By Lemmas 2.4 and 2.3,

Mod(P) = ⋂_{ρ∈P}{S : S ⊧ ρ}
= ⋂_{ρ∈P}{S : At(ρ) ∩ S ≠ ∅}
= ⋂_{B∈Core(P)}{S : B ∩ S ≠ ∅}
= ⋂_{B∈Θ}{S : B ∩ S ≠ ∅}
= ⋂_{B∈Δ}{S : B ∩ S ≠ ∅}
= S̃.

Therefore Min(P) = min S̃ = S, using Theorem 2.2 for the second equality. (⇒) Let P be a prerequisite–free program such that Min(P) = S. Observe first that, for every ρ ∈ P, At(ρ) ∈ Δ. So every element of Core(P) contains an element of Θ.

Suppose for contradiction that Core(P) ≠ Θ. Then either Core(P) − Θ ≠ ∅ or Θ − Core(P) ≠ ∅. But if B ∈ (Core(P) − Θ), then, by minimality of Core(P), the set B′ ⊆ B such that B′ ∈ Θ is not an element of Core(P). So it suffices to consider the second possibility.

Let C then be an element of (Θ − Core(P)). For each element B of Core(P), by minimality of Θ it is not the case that B ⊂ C, so there is some atom a_{B} ∈ (B − C). Let A = {a_{B} : B ∈ Core(P)}.

For every ρ ∈ P, A ∩ At(ρ) ≠ ∅, and therefore A ∈ Mod(P). Let A′ ⊆ A be a minimal model of P. By the hypothesis A′ ∈ S, and therefore C ∩A′ ≠ ∅ since C ∈ Δ. But then C ∩ A ⊇ C ∩ A′ ≠ ∅, which contradicts the construction of A.

Hence the contradiction assumption was incorrect, and so Core(P) = Θ, as desired. □

In the first procedure, given F ⊆ 2^{U} as an intersection of basic closed sets in (2^{U}, Cantor) we compute an expression for F^{⊇} in a form from which the minimal elements are easily recognized.

Algorithm 2.1 (for obtaining Min(P) from P) Let P be a program, not necessarily prerequisite–free. Fix an expression for the closed set F = Mod(P) in (2^{U}, Cantor) as an intersection of basic closed sets determined by the clauses of P. F appears then as an intersection of sets defined by finite disjunctions of atomic and negated atomic expressions.

(1) If P consists of a single clause, express F as a union of sets of the form {S : u ∈ S} or {S : u ∉ S} corresponding to the disjuncts of the clause. If every clause in P has an empty body, then express F as a single set defined by a conjunction (possibly infinite) of the expressions “u ∈ S” for clauses u ← in P. Otherwise, use the distributive property to express F as a union of sets defined by conjunctions (possibly infinite) of atomic and negated atomic expressions.

(2) Simplify by omitting any summand which is empty.

(3) Since ⊇ commutes with ∪, form F^{⊇} by applying ⊇ to each summand.

(4) For each summand, evaluate the application of ⊇ by omitting the negative conjuncts.

(5) Simplify by omitting summands defined by expressions which are not minimal. That is, if S′ and S′′ are summands, and the conjunction defining S′ is a proper subexpression of the conjunction defining S′′, omit S′′. (To see that the reduced expression still represents the same set F^{⊇}, note that every element X of F^{⊇} belongs to the summand {S : X′ ⊆ S} of the reduced expression, where X′ ⊆ X is a minimal element of F^{⊇} whose existence is guaranteed by Lemma 2.1.) Then F^{⊇} is expressed as a union of sets of the form {S : X ⊆ S}, where the sets X determining each summand form an antichain X; that is, F^{⊇} = X^{⊇} with X an antichain. By Lemma 2.2, the sets X themselves are the minimal models of P. □

The second procedure produces a prerequisite–free program with prescribed minimal models:

Algorithm 2.2 (for obtaining from minimal class M a canonical prerequisite–free program P′ such that Min(P′) = M) Let M ⊆ 2^{U} be a minimal class. According to Proposition 2.5, M is the collection of minimal models of the theory T consisting of disjunctions ⋁_{b∈B} b for each B ∈ Θ, where Θ, as defined in the proposition, consists of the minimal elements of

Δ = {B ∈ Fin(U) : for all S ∈ M, B ∩ S ≠ ∅}.

If M is finite, it may be more convenient to obtain this theory as follows: First express M^{⊇} in the form ⋃_{X∈M}{S : X ⊆ S}, which is a finite union of sets each defined by a countable conjunction. Then apply the distributive property to obtain an expression for M^{⊇} as a countable intersection of sets each defined by a finite disjunction. By Proposition 2.5, the minimal sets of atoms which compose disjunctions in this collection are exactly the sets B which belong to Θ, and it suffices to retain only the disjunctions formed over these minimal sets.

Now let ≤ be an ordering of type ω on U (or of type n if |U| = n for n < ω). As in Theorem 2.1, form a program P′ by replacing each disjunction

⋁_{b∈B} b

of T by the prerequisite–free clause

c ← ⋀_{b∈B,b≠c} ¬b,

where c is the greatest element of B in the ordering ≤ . Since P′ has the same models as T, Min(P′) = M, as desired. □

Remark 2.2 If S is known to be a \underline{subset} of a minimal class (as in Theorem 2.3), then Algorithm 2.2 can be used to produce a prerequisite–free program whose minimal model class \underline{contains} S (that is, with min S̃ as its minimal model class).

We now present a range of examples to illustrate the ideas of this section:

Example 2.4 Let P be the program

q ← ¬p
r ← q

which is not prerequisite–free. The collection F of models of P is F_{1} ∩ F_{2}, where

F_{1} = {S : p ∈ S ∨ q ∈ S}
F_{2} = {S : q ∉ S ∨ r ∈ S}.

The key element of our method is to find an expression for F^{⊇}. We proceed as in Algorithm 2.1:

(1) By the distributive property,

F = F_{1} ∩ F_{2}
= {S : (p ∈ S ∨ q ∈ S) ∧ (q ∉ S ∨ r ∈ S)}
= {S : p ∈ S ∧ q ∉ S} ∪ {S : q ∈ S ∧ q ∉ S}
∪ {S : p ∈ S ∧ r ∈ S} ∪ {S : q ∈ S ∧ r ∈ S}

(2) Since the second summand is empty, we omit it:

F = {S : p ∈ S ∧ q ∉ S} ∪ {S : p ∈ S ∧ r ∈ S} ∪ {S : q ∈ S ∧ r ∈ S} (3) We form F^{⊇} by applying ⊇ to each summand:

F^{⊇} = {S : p ∈ S ∧ q ∉ S}^{⊇} ∪ {S : p ∈ S ∧ r ∈ S}^{⊇} ∪ {S : q ∈ S ∧ r ∈ S}^{⊇} (4) We evaluate the application of ⊇ to each summand by omitting the negative conjuncts:

F^{⊇} = {S : p ∈ S} ∪ {S : p ∈ S ∧ r ∈ S} ∪ {S : q ∈ S ∧ r ∈ S}

(5) Since the second summand is a subset of the first, it can be omitted, leaving only maximal summands:

F^{⊇} = {S : p ∈ S} ∪ {S : q ∈ S ∧ r ∈ S}

According to Algorithm 2.1, we can read off the minimal models of P directly from this expression as

M = {{p}, {q, r}}.

As in Algorithm 2.2, we can proceed further to find an expression for F^{⊇} as an intersection of basic closed sets:

(6) Since the union in Step (5) is finite, we can apply the distributive property to get the desired form:

F^{⊇} = {S : p ∈ S ∨ q ∈ S} ∩ {S : p ∈ S ∨ r ∈ S}

Then the clauses

p ← ¬q
p ← ¬r

constitute a prerequisite–free program P′ for which Mod(P′) = F^{⊇} and hence Min(P′) = M = Min(P).^{1}

Finally, from the expression in Step (6) we can construct, as in Theorem 2.5, the sentence μ =

(p ∈ S ↔ q ∉ S ∨ r ∉ S)
∧ (q ∈ S ↔ p ∉ S)
∧ (r ∈ S ↔ p ∉ S)

defining the minimal models of P. □

Example 2.5 (More than one entry in body of clause) Let P be the program

u_{1} ← ¬u_{0}
u_{4} ← ¬u_{1}, ¬u_{2}, ¬u_{3}.

1 Algorithm 2.3 to be presented later in the chapter provides a more direct way to obtain the prerequisite–free program P′ from the given program P.

Since P is itself prerequisite–free, the set Mod(P) =

{S : u_{0} ∈ S ∨ u_{1} ∈ S} ∩ {S : u_{1} ∈ S ∨ u_{2} ∈ S ∨ u_{3} ∈ S ∨ u_{4} ∈ S}

is closed in (2^{U}, Scott^{−1}). By Theorem 2.5, its minimal elements are defined by the sentence μ =

[u_{0} ∈ S ↔ u_{1} ∉ S]
∧ [u_{1} ∈ S ↔ u_{0} ∉ S ∨ (u_{2} ∉ S ∧ u_{3} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{2} ∈ S ↔ (u_{1} ∉ S ∧ u_{3} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{3} ∈ S ↔ (u_{1} ∉ S ∧ u_{2} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{4} ∈ S ↔ (u_{1} ∉ S ∧ u_{2} ∉ S ∧ u_{3} ∉ S)].

To find its minimal models explicitly, we use Algorithm 2.1:

(1) By the distributive property, Mod(P) =

{S : u_{0} ∈ S ∧ u_{1} ∈ S} ∪ {S : u_{0} ∈ S ∧ u_{2} ∈ S}
∪ {S : u_{0} ∈ S ∧ u_{3} ∈ S} ∪ {S : u_{0} ∈ S ∧ u_{4} ∈ S}
∪ {S : u_{1} ∈ S ∧ u_{1} ∈ S} ∪ {S : u_{1} ∈ S ∧ u_{2} ∈ S}
∪ {S : u_{1} ∈ S ∧ u_{3} ∈ S} ∪ {S : u_{1} ∈ S ∧ u_{4} ∈ S}

Steps (2), (3), and (4) for evaluating (Mod(P))^{⊇} leave this expression unchanged (since P is prerequisite–free).

(5) Omitting unnecessary terms, we get (Mod(P))^{⊇} =

\begin{matrix}\{S : u_{1} ∈ S\} ∪ \{S : u_{0} ∈ S ∧ u_{2} ∈ S\} ∪ \\ \{S : u_{0} ∈ S ∧ u_{3} ∈ S\} ∪ \{S : u_{0} ∈ S ∧ u_{4} ∈ S\}. \end{matrix}

Thus Min(P) = {{u_{1}}, {u_{0}, u_{2}}, {u_{0}, u_{3}}, {u_{0}, u_{4}}}. □

Example 2.6 (Special case where Min(P) = {∅}) Let P consist of the single clause

q ← p.

Since the set

Mod(P) = {S : p ∉ S ∨ q ∈ S}

is not closed in (2^{U}, Scott^{−1}), we pass to

(Mod(P))^{⊇} = {S : p ∉ S}^{⊇} ∪ {S : q ∈ S}^{⊇} = 2^{U}.

Now 2^{U} is the intersection of an empty collection of basic closed sets (or, in logic programming terms, is the set of models of the empty program P′). So according to Theorem 2.5, the minimal elements are defined by the sentence

μ = ⋀_{u∈U}(u ∈ S ↔ false)
= ⋀_{u∈U} u ∉ S.

Thus the only minimal model of P is the empty subset of U. □

Example 2.7 (Special case where Min(P) = {U}) Let P be the program consisting of all clauses of the form

u ←

for u ∈ U. The set of its models is naturally expressed as a set closed in (2^{U}, Scott^{−1}) by

Mod(P) = ⋂_{u∈U}{S : u ∈ S}.

According to Theorem 2.5, its minimal elements are defined by the sentence

μ = ⋀_{u∈U}(u ∈ S ↔ true)
= ⋀_{u∈U} u ∈ S.

Thus U itself, the only subset of U which satisfies μ, is the only minimal model of P. □

Example 2.8 Let P be the infinite program

u_{1} ← ¬u_{0}
u_{3} ← ¬u_{2}
⋮
u_{2i+1} ← ¬u_{2i}
⋮
u_{2} ← u_{0}

where U = {u_{0}, u_{1}, u_{2}, …}. Since P is not prerequisite–free, we pass to (Mod(P))^{⊇}, which we can compute according to Algorithm 2.1. To simplify the notation, let

Ψ = {ψ ∈ ω^{ω} : ∀i(ψ(i) = 2i or ψ(i) = 2i + 1)}.

Then [Mod(P)]^{⊇}

= [{S : u_{0} ∉ S ∨ u_{2} ∈ S} ∩ ⋂_{i∈ω}{S : u_{2i} ∈ S ∨ u_{2i+1} ∈ S}]^{⊇}
= [{S : u_{0} ∉ S ∨ u_{2} ∈ S} ∩ ⋃_{ψ∈Ψ}{S : ⋀_{i∈ω} u_{ψ(i)} ∈ S}]^{⊇}
= ⋃_{ψ∈Ψ}{S : u_{0} ∉ S ∧ ⋀_{i∈ω} u_{ψ(i)} ∈ S}^{⊇} ∪ ⋃_{ψ∈Ψ}{S : u_{2} ∈ S ∧ ⋀_{i∈ω} u_{ψ(i)} ∈ S}^{⊇}
= ⋃_{ψ∈Ψ}{S : u_{1} ∈ S ∧ u_{2} ∈ S ∧ ⋀_{i≥2} u_{ψ(i)} ∈ S} ∪

⋃_{ψ∈Ψ}{S : u_{1} ∈ S ∧ u_{3} ∈ S ∧ ⋀_{i≥2} u_{ψ(i)} ∈ S} ∪

⋃_{ψ∈Ψ}{S : u_{0} ∈ S ∧ u_{2} ∈ S ∧ ⋀_{i≥2} u_{ψ(i)} ∈ S}.

Then we can read off from this expression that the minimal elements of Mod(P) are those sets which consist of u_{0} and u_{2} and one element from each pair {u_{4}, u_{5}}, {u_{6}, u_{7}}, …, together with those sets which consist of u_{1} and either u_{2} or u_{3} and one element from each pair {u_{4}, u_{5}}, {u_{6}, u_{7}}, ….

As a matter of interest, we may proceed further using Algorithm 2.2 to find a prerequisite–free program P′ with the same minimal models. In this case, however, the distributive property applied to the preceding expression for (Mod(P))^{⊇} doesn’t produce the proper form, nor is it evident how to factor this expression as a product of finite factors. Instead, as in Algorithm 2.2, we look for those finite sets B ⊆ U such that every minimal model of P contains some element of B. There are no singleton sets with this property. Among the sets with two elements, every pair {u_{2i}, u_{2i+1}} is of this sort; that is, for all X ∈ Min(P), u_{2i} ∈ X or u_{2i+1} ∈ X. Beyond these, only the pair {u_{1}, u_{2}} has this property. Conditions involving sets B of three or more elements turn out in this instance to be redundant. As in Algorithm 2.2, then,

M^{⊇} = {S : u_{1} ∈ S ∨ u_{2} ∈ S} ∩ ⋂_{i≥0}{S : u_{2i} ∈ S ∨ u_{2i+1} ∈ S},

where M is the set of minimal models of P described above. Translating the basic closed sets into clauses, we obtain finally the following prerequisite–free program P′ with Min(P′) = M :

u_{2} ← ¬u_{1}
u_{1} ← ¬u_{0}
u_{3} ← ¬u_{2}
⋮
u_{2i+1} ← ¬u_{2i}
⋮

Again, a more efficient method for obtaining P′ from P will be presented in Algorithm 2.3. □

Example 2.9 Predicate logic programs can be handled similarly, upon replacement of each clause by its set of ground instances. Consider the following predicate logic program P, based on the preceding example:

even(0)

even(σ^{2}(X)) ← even(X)
u(σ(X)) ← even(X), ¬u(X)
u(σ^{2}(0)) ← u(0),

with ground(P) then consisting of

even(0)
even(σ^{2}(0)) ← even(0)
even(σ^{3}(0)) ← even(σ(0))
even(σ^{4}(0)) ← even(σ^{2}(0))
⋮
u(σ(0)) ← even(0), ¬u(0)
u(σ^{2}(0)) ← even(σ(0)), ¬u(σ(0))
u(σ^{3}(0)) ← even(σ^{2}(0)), ¬u(σ^{2}(0))
⋮
u(σ^{2}(0)) ← u(0).

By the method above, we find that the minimal models are those subsets of the Herbrand base which consist of

even(0), even(σ^{2}(0)), even(σ^{4}(0)), …

and either u(0) and u(σ^{2}(0)) and one element from each pair

{u(σ^{4}(0)), u(σ^{5}(0))}, {u(σ^{6}(0)), u(σ^{7}(0))}, …,

or u(σ(0)) and u(σ^{2}(0)) or u(σ^{3}(0)) and one element from each pair

{u(σ^{4}(0)), u(σ^{5}(0))}, {u(σ^{6}(0)), u(σ^{7}(0))}, ….

The calculation is similar to that of the last example, though somewhat messier. □

As in Examples 2.4 and 2.8, Algorithms 2.1 and 2.2 together provide a procedure for obtaining from a given program P a canonical prerequisite–free program P′ with the same minimal models. Since there are at most countably many propositional clauses over a given countable universe U, both the initial program P and the desired program P′ are countable. However, the use of the distributive property in Step (1) of Algorithm 2.1 may produce an intermediate expression with uncountably many terms.

Here we present a different method for constructing P′ from P which terminates in at most ω steps and involves only countable sets. From Lemma 2.3 we see that a suitable prerequisite–free program with the same minimal models as P consists of all the prerequisite–free clauses that are logical consequences of P. These clauses could be generated in the form of disjunctions of positive literals by iterating the process of performing all possible resolutions, starting with the disjunctions obtained from the clauses of P. Here we present a more efficient “hyperresolution” procedure for generating positive disjunctions, based on the “unfolding” process of Dung and Kanchanasut ([11]) for finding a prerequisite–free program P † with the same stable models as a given initial program P.

Algorithm 2.3 (for obtaining from program P a canonical prerequisite– free program P′ such that Min(P′) = Min(P)) Let P be a propositional general logic program. For clarity, replace each clause

p ← ¬p_{1}, …, ¬p_{n}, q_{1}, …, q_{m}

of P (with n, m ≥ 0) by the expression

p ∨ p_{1} ∨ … ∨ p_{n} ← q_{1}, …, q_{m},

denoting by P_{d} the resulting disjunctive logic program.

We define an operator O_{P} on sets of positive disjunctions as follows: Let I be a set of positive disjunctions. If

p ∨ p_{1} ∨ … ∨ p_{n} ← q_{1}, …, q_{m}

belongs to P_{d} and each of the disjunctions

q_{1} ∨ r_{1,1} ∨ … ∨ r_{1,k_{1}}
⋮
q_{m} ∨ r_{m,1} ∨ … ∨ r_{m,k_{m}}

(with k_{1}, …, k_{m} ≥ 0) belongs to I, then the disjunction

p ∨ p_{1} ∨ … ∨ p_{n} ∨ r_{1,1} ∨ … ∨ r_{1,k_{1}} ∨ … ∨ r_{m,1} ∨ … ∨ r_{m,k_{m}}

belongs to O_{P} (I). In particular (when m = 0), if

p ∨ p_{1} ∨ … ∨ p_{n} ←

belongs to P_{d}, then the disjunction

p ∨ p_{1} ∨ … ∨ p_{n}

belongs to O_{P} (I). Since O_{P} is monotone and positive–finitizable, it has a least fixpoint, given by O_{P} ↑ ω(∅), which we denote by P′_{d}. This is of course a set of positive disjunctions. We will show below in Lemma 2.5 that P and P′_{d} have the same minimal models.

Let P′′_{d} consist of those elements of P′_{d} which are subsumed by no other element of P′_{d}. According to Lemma 2.4, P′_{d} and P′′_{d} have the same models, and hence the same minimal models. Finally, let P′ be the program obtained by replacing each disjunction

⋁_{b∈B} b

in P′′_{d} by the prerequisite–free clause

c ← ⋀_{b∈B,b≠c} ¬b,

where c is the greatest element of B according to a given ordering ≤ of type ω on U (or of type n if |U| = n for n < ω). Since P′ has the same models as P′′_{d}, Min(P′) = Min(P), as desired. □

It remains to show that the program P and the theory P′_{d} = O_{P} ↑ ω(∅) have the same minimal models:

Lemma 2.5 Let P and P′_{d} be as in Algorithm 2.3 above.

(a) If S is a model of P, then S is a model of P′_{d}.

(b) If S is a minimal model of P′_{d}, then S is a model of P.

(c) S is a minimal model of P if and only if S is a minimal model of P′_{d}.

Proof:

(a) Every element of P′_{d} is obtained by sound inference rules from the propositional theory equivalent to the program P.

(b) Let S be a minimal model of P′_{d}, and let ρ be the clause

p ← ¬p_{1}, …, ¬p_{n}, q_{1}, …, q_{m}

of P. Assume that S satisfies the body of ρ; we will show then that p ∈ S. For each positive entry q_{i} in the body of ρ, there is a disjunction

q_{i} ∨ r_{i,1} ∨ … ∨ r_{i,k_{i}}

(with k_{i} ≥ 0) in P′_{d} for which q_{i} is the sole disjunct belonging to S; for otherwise S − {q_{i}} ⊧ P′_{d}, contradicting the minimality of S. By the construction of P′_{d}, the disjunction

p ∨ p_{1} ∨ … ∨ p_{n} ∨ r_{1,1} ∨ … ∨ r_{1,k_{1}} ∨ … ∨ r_{m,1} ∨ … ∨ r_{m,k_{m}}

belongs to P′_{d}, and therefore holds on S. Since each literal other than p in this disjunction does not belong to S, we conclude that p ∈ S, as desired.

(c) ⟹ Let S be a minimal model of P. By (a), S is a model of P′_{d}. Let S_{m} be a minimal model of P′_{d} such that S_{m} ⊆ S. By (b), S_{m} is also a model of P. By the assumption, then, S_{m} = S, and so S is a minimal model of P′_{d} as well. ⟸ Now let S be a minimal model of P′_{d}. By (b), S is a model of P. Let S_{0} be a model of P such that S_{0} ⊆ S. By (a), S_{0} is a model of P′_{d}. By the assumption, then, S_{0} = S, and so S is a minimal model of P as well. □

Example 2.10 Let P be the program

u_{2} ← ¬u_{1}
u_{3} ← u_{2}
u_{4} ← ¬u_{2}.

We will follow the procedure of Algorithm 2.3 to obtain a prerequisite–free program P′ with the same minimal models.

First we rewrite the clauses of P as follows:

u_{2} ∨ u_{1} ←
u_{3} ← u_{2}
u_{4} ∨ u_{2} ←

Next we generate the set O_{P} ↑ ω(∅) of positive disjunctions: O_{P} (∅) = {u_{2} ∨ u_{1}, u_{4} ∨ u_{2}}. O_{P} (O_{P} (∅)) = {u_{2} ∨ u_{1}, u_{4} ∨ u_{2}, u_{3} ∨ u_{1}, u_{3} ∨ u_{4}}. Application of O_{P} to this set produces the same set, so O_{P} ↑ ω(∅) = {u_{2} ∨ u_{1}, u_{4} ∨ u_{2}, u_{3} ∨ u_{1}, u_{3} ∨ u_{4}}. Recall that this theory has the same minimal models as the given program P.

Finally we obtain program P′ by replacing disjunctions by prerequisite–free clauses formed in accordance with the ordering u_{1} < u_{2} < u_{3} < u_{4} :

u_{2} ← ¬u_{1}
u_{4} ← ¬u_{2}
u_{3} ← ¬u_{1}
u_{4} ← ¬u_{3}

We can easily check that P and P′ have the same minimal models, namely {u_{2}, u_{3}} and {u_{1}, u_{4}}.

We note that in this example the program P′ is not the same as the normal–form program P † with Stab(P †) = Stab(P) which will be discussed in the next chapter.

□

STABLE MODEL CLASSES

One cannot help but notice the formal resemblance between the sentence μ developed here which characterizes the minimal models of a program P and the sentence σ of [36] discussed in Section 1.4 which characterizes its stable models. Recall that μ has the form

⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S]

and σ has the form

⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S]

for certain collections Φ_{u} and Ψ_{u} of finite sets A ⊆ U. As concerns μ, the negative information pertaining to element u ∈ U comes from the supports of u in the clauses of a prerequisite–free program P′ associated with P. To give a similar description concerning σ, we first make explicit a “normal–form” result for stable model classes:

Proposition 3.1 (Prerequisite–free representation) [36] For any propositional logic program P, there is a prerequisite–free program P † such that Stab(P) = Stab(P †).

Proof: Let

⋀_{u∈U}[R(\underline{u}) ↔ ⋁_{A∈Ψ_{u}} ⋀_{a∈A} ¬R(\underline{a})]

be the sentence σ which specifies the stable models of P, so that (U, S, u⃗_{u∈U}) ⊧ σ if and only if

⋀_{u∈U}(u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S).

Recall that Ψ_{u} is the set of supports of minimal proof schemes for u over program P. Let P † be the program consisting of all clauses

u ← ¬A⃗

for u ∈ U and A ∈ Ψ_{u}. For each u ∈ U, the supports of proof schemes for u in P † are exactly the finite sets A ∈ Ψ_{u}. So the sentence σ† which specifies the stable models of P † is σ itself. Thus

Stab(P) = {S : (U, S, u⃗_{u∈U}) ⊧ σ} = Stab(P †). □

For the sentence σ, then, the negative information pertaining to element u ∈ U also amounts to the supports of u in certain prerequisite–free clauses, namely those clauses of the associated program P † which have u as their head. Suppose that P is itself a prerequisite–free program; then P = P′ = P †. For each u, the collection Ψ_{u} (of supports of u in clauses where u is the head) is a subset of Φ_{u} (the supports of u in clauses in which u appears as the head or in the body). So in this case the sentence σ is actually a subexpression of the sentence μ.

We can use this comparison of defining equations for minimal and stable model classes to make a comparison of the classes themselves. Based on the characterization of minimal model classes in Theorem 2.2, we will then be able to characterize stable model classes as well. Because we will be comparing classes associated with different programs, we will use subscript P to identify the defining equations associated with program P.

To begin with, consider an arbitrary minimal model class, say the minimal models of program P. Let P′ be a prerequisite–free program for which μ_{P} = μ_{P′}. Form a new program P^{♯} such that μ_{P′} = σ_{P^{♯}} as follows: For every clause ρ in P′, include in P^{♯} all the clauses formed by rearranging ρ so that different atoms from ρ appear as the head—or, equivalently, all clauses

u ← ¬A⃗

for u ∈ U and A ∈ Φ_{u}, where

⋀_{u∈U}(u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S)

is the sentence μ_{P′}. In this way the class of minimal models of P can be realized as the class of stable models of a related program P^{♯}. In fact by a generalization of this approach, not only can entire minimal classes be realized, but also appropriate subsets of such classes, as suggested by the preceding comparison of defining equations. The following theorem characterizes stable model classes in such terms:

Theorem 3.1 (Characterization of stable model classes (I)) For S ⊆ 2^{U} with the inverse–Scott topology, the following are equivalent:

(i) S is a stable model class. (ii) S is a G_{δ} subset of a minimal model class. (iii) S is a G_{δ} subset of min S̃. (iv) S is a G_{δ} subset of min S̄.

Proof: If S = ∅, then the theorem certainly holds. So we assume throughout that S ≠ ∅.

(i) ⇒ (ii) Suppose that S = Stab(P). Pass to the prerequisite–free program P † which has the same stable models as P. Recall that

σ_{P†} = ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S]

is a subexpression of

μ_{P†} = ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S]

in the sense that Ψ_{u} ⊆ Φ_{u} for each u ∈ U. Then

Stab(P)
= {S : (U, S, u⃗_{u∈U}) ⊧ σ_{P†}}
= {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S]}
= {S : ⋀_{u∈U}[(u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S) ∧ (u ∈ S → ⋁_{A∈Ψ_{u}} A⃗ ∉ S)]}
= {S : (U, S, u⃗_{u∈U}) ⊧ μ_{P†}} ∩ {S : ⋀_{u∈U}[u ∈ S → ⋁_{A∈Ψ_{u}} A⃗ ∉ S]}
= Min(P †) ∩ ⋂_{u∈U}{S : u ∉ S ∨ ⋁_{A∈Ψ_{u}} A⃗ ∉ S}.

We note that each set {S : u ∉ S ∨ ⋁_{A∈Ψ_{u}} A⃗ ∉ S} is open.

(ii) ⇒ (iii) Given that S is a G_{δ} subset of Min(P) for some P, let F = (Mod(P))^{⊇}. Then S = (min F) ∩ ⋂_{k∈ω} G_{k}, where F is closed and each G_{k} is open. We will show that S = (min S̃) ∩ ⋂_{k∈ω} G_{k}. (⊆) Since S̃ ⊆ F, S ⊆ (min F)∩S̃ ⊆ min S̃. By assumption S ⊆ ⋂_{k∈ω} G_{k}. Therefore S ⊆ (min S̃) ∩ ⋂_{k∈ω} G_{k}. (⊇) Let S ∈ (min S̃) ∩ ⋂_{k∈ω} G_{k}. Since S ∈ S̃ ⊆ F, by Lemma 2.1 there exists T ⊆ S such that T ∈ min F. Since open sets are specified by only negative information, S ∈ ⋂_{k∈ω} G_{k} ⇒ T ∈ ⋂_{k∈ω} G_{k}. Hence T ∈ S. But because S ∈ min S̃, we have T = S, so S ∈ S.

(iii) ⇒ (iv) By Propositions 2.1 and 2.3, min S̄ = min(S̄)^{⊇} = min S̃. Therefore S = (min S̄) ∩ ⋂_{k∈ω} G_{k}.

(iv) ⇒ (ii)

We are given that S is a G_{δ} subset of min S̄. Since S ≠ ∅, min S̄ = min(S̄ ∪ {U}). Since S̄∪{U} is closed in the Cantor topology and has U as an element, by the model class characterization theorem of [36] noted in Section 1.4, there is a program P such that S̄ ∪ {U} = Mod(P), hence min(S̄ ∪ {U}) = Min(P). So S is a G_{δ} subset of Min(P).

(ii) ⇒ (i) Let U = {u_{k} : k < |U|}. Let P be a program and G a G_{δ} subset of (2^{U}, Scott^{−1}) such that S = Min(P) ∩ G. By Theorem 2.5, for each k < |U| there is a set Φ_{u_{k}} of finite subsets of U such that

Min(P) = {S : ⋀_{k<|U|}[u_{k} ∈ S ↔ ⋁_{A∈Φ_{u_{k}}} A⃗ ∉ S]}.

Let {G_{k}}_{k∈ω} be a collection of open subsets of (2^{U}, Scott^{−1}) (including if necessary multiple copies of 2^{U}) such that G = ⋂_{k∈ω} G_{k}. First we “preprocess” the list (G_{k})_{k∈ω} as follows: For each k ∈ ω, let

F_{k} = {S ⊆ U : S is finite, max{i : u_{i} ∈ S} = k, and S ∉ ⋂_{i∈ω} G_{i}}.

Then let

G′_{k} = G_{k} − F_{k}^{⊇}.

To simplify the subsequent construction, also let

G′′_{k} = ⋂_{i≤k} G′_{k}

for each k ∈ ω.

We observe the following:

(i) Because F_{k} is finite, it is closed in the Cantor topology. In the inverse–Scott topology, then, F_{k}^{⊇} is closed by Proposition 2.2, so G′_{k} is open. Then G′′_{k}, as the intersection of finitely many open sets, is open as well. So G′′_{k} can be expressed in the form

G′′_{k} = ⋃_{B∈B_{k}}{S : B⃗ ∉ S}

for some collection B_{k} of finite subsets of U.

(ii) Clearly ⋂_{k∈ω} G′′_{k} = ⋂_{k∈ω} G′_{k} ⊆ ⋂_{k∈ω} G_{k}, and G′′_{0} ⊇ G′′_{1} ⊇ G′′_{2} ⊇ ….

We show in addition that ⋂_{k∈ω} G_{k} ⊆ ⋂_{k∈ω} G′_{k}, so that ⋂_{k∈ω} G′′_{k} = ⋂_{k∈ω} G′_{k} = ⋂_{k∈ω} G_{k} :

Suppose that S ∉ ⋂_{k∈ω} G′_{k}. Then for some k ∈ ω, S ∉ G′_{k}, so S ∈ Fk^{⊇}. Then Š ∈ F_{k} for some subset Š of S. By definition, Š ∉ ⋂_{i∈ω} G_{i}, so, for some j ∈ ω, Š ∉ G_{j}. Since G_{j}, as an open subset of (2^{U}, Scott^{−1}), is lower closed, S ∉ G_{j}.

(iii) For any finite set S ⊆ U, if S ∈ G′′_{j} where j = max{i : u_{i} ∈ S}, then S ∈ G_{k} for every k ∈ ω.

Now construct a program Γ as follows: For each k < |U|, let Γ_{k} consist of all clauses

u_{k} ← ¬A⃗, ¬B⃗

for pairs (A, B) with A ∈ Φ_{u_{k}} and B ∈ B_{k}. Let Γ = ⋃_{k<|U|} Γ_{k}. We will show that S = Stab(Γ).

We note first that, since Γ is prerequisite–free, calculations involving the Gelfond– Lifschitz transform relative to any subset of U are particularly simple, because every clause of the transformed program has an empty body. For every S′ ⊆ U, then,

T_{GL(S′,Γ)} ↑ω(∅) = T_{GL(S′,Γ)}(∅)
= {u ∈ U : u ← is a clause of GL(S′, Γ)}
= \{u ∈ U : there is a clause u ← ¬A⃗, ¬B⃗ in Γ with \overline{(A ∪ B)} ∉ S′\}.

(⊆) Let S ∈ S. We will show that S ∈ Stab(Γ) by showing that S = T_{GL(S,Γ)} ↑ ω(∅). By the preceding observation, it will suffice to show that

S = \{u ∈ U : there is a clause u ← ¬A⃗, ¬B⃗ in Γ with \overline{(A ∪ B)} ∉ S\}.

(a) Let u_{ℓ} ∈ S. Since S ∈ Min(P), according to μ_{P} there is a set A ∈ Φ_{u_{ℓ}} such that A⃗ ∉ S. Since S ∈ ⋂_{k∈ω} G′′_{k} ⊆ G′′_{ℓ}, there is also a set B ∈ B_{ℓ} such that B⃗ ∉ S. For this pair (A, B), the clause

u_{ℓ} ← ¬A⃗, ¬B⃗

appears in Γ and \overline{(A ∪ B)} ∉ S.

(b) Let

u_{ℓ} ← ¬A⃗, ¬B⃗

be a clause in Γ such that \overline{(A ∪ B)} ∉ S. By definition of Γ, A ∈ Φ_{u_{ℓ}}. Because by assumption S ∈ Min(P) and hence satisfies the condition

u_{ℓ} ∈ S ↔ ⋁_{A∈Φ_{u_{ℓ}}} A⃗ ∉ S,

we conclude that u_{ℓ} ∈ S, as desired.

(⊇) Now let S ∈ Stab(Γ). As observed above,

S = \{u ∈ U : there is a clause u ← ¬A⃗, ¬B⃗ in Γ with \overline{(A ∪ B)} ∉ S\}.

We will show that S ∈ S by showing that: (a) S ∈ ⋂_{k∈ω} G_{k}, and (b) S ∈ Min(P).

(a) Let ℓ be given. We show that S ∈ G_{ℓ} : \underline{Case 1}. Suppose that there is an element u_{m} ∈ S with m ≥ ℓ. Then there is some clause

u_{m} ← ¬A⃗, ¬B⃗

in Γ_{m} with B ∈ B_{m} such that B⃗ ∉ S. Therefore S ∈ G′′_{m} ⊆ G′′_{ℓ} ⊆ G_{ℓ}.

\underline{Case 2}. Suppose that S = ∅. Recall that S is assumed to be nonempty (because S = ∅ was treated separately), and hence G_{ℓ} ≠ ∅. Since open sets in (2^{U}, Scott^{−1}) are downward closed, S = ∅ belongs to G_{ℓ}. \underline{Case 3}. Otherwise there exists j < ℓ such that u_{j} ∈ S and j = max\{i : u_{i} ∈ S\}. Then there is some clause

u_{j} ← ¬A⃗, ¬B⃗

in Γ_{j} with B ∈ B_{j} such that B⃗ ∉ S. Therefore S ∈ G′′_{j}. By observation (iii) concerning the list (G′′_{k})_{k∈ω}, S ∈ G_{ℓ}.

(b) Let ℓ be given. We show that S satisfies the ℓth conjunct

u_{ℓ} ∈ S ↔ ⋁_{A∈Φ_{u_{ℓ}}} A⃗ ∉ S

of μ_{P} : → Suppose that u_{ℓ} ∈ S. Then there is a clause

u_{ℓ} ← ¬A⃗, ¬B⃗

in Γ_{ℓ} with A ∈ Φ_{u_{ℓ}} such that A⃗ ∉ S. ← Suppose that A⃗ ∉ S for some A ∈ Φ_{u_{ℓ}}. From part (a) we know that S ∈ ⋂_{k∈ω} G′′_{k}, so there is some B ∈ B_{ℓ} such that B⃗ ∉ S. Then the clause

u_{ℓ} ← ¬A⃗, ¬B⃗

appears in Γ_{ℓ}, with \overline{(A ∪ B)} ∉ S. Therefore u_{ℓ} ∈ S, as desired. □

Example 3.1 Consider again the program P

u_{1} ← ¬u_{0}
u_{4} ← ¬u_{1}, ¬u_{2}, ¬u_{3}

of Example 2.5 above. As determined earlier, its minimal models are {u_{1}}, {u_{0}, u_{2}}, {u_{0}, u_{3}}, and {u_{0}, u_{4}}. According to the theorem, any inverse–Scott G_{δ} subset of this collection M is expressible as the set of stable models of an associated program Γ. Let us check the prescription for Γ when the subset to be represented is M itself.

As determined before, the sentence μ_{P} which characterizes Min(P) is

[u_{0} ∈ S ↔ u_{1} ∉ S]

∧ [u_{1} ∈ S ↔ u_{0} ∉ S ∨ (u_{2} ∉ S ∧ u_{3} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{2} ∈ S ↔ (u_{1} ∉ S ∧ u_{3} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{3} ∈ S ↔ (u_{1} ∉ S ∧ u_{2} ∉ S ∧ u_{4} ∉ S)]
∧ [u_{4} ∈ S ↔ (u_{1} ∉ S ∧ u_{2} ∉ S ∧ u_{3} ∉ S)].

For this case, we have S = Min(P) ∩ G, where we take G as ⋂_{k∈ω} G_{k} with G_{k} = 2^{U} for each k ∈ ω. Since \underline{every} subset of U belongs to G, F_{k} = ∅, and so G_{k} = G′_{k} = G′′_{k} = 2^{U}, for each k ∈ ω. As in the theorem, we express G′′_{k} for each k ∈ ω as ⋃_{B∈{∅}}{S : B⃗ ∉ S} (so that B = ∅ is the only element of Φ_{u_{k}}). Then we form the clauses of Γ_{k} for k < 5 as follows:

Γ_{0} = {u_{0} ← ¬u_{1}}

Γ_{1} = {u_{1} ← ¬u_{0}, u_{1} ← ¬u_{2}, ¬u_{3}, ¬u_{4}}
Γ_{2} = {u_{2} ← ¬u_{1}, ¬u_{3}, ¬u_{4}}
Γ_{3} = {u_{3} ← ¬u_{1}, ¬u_{2}, ¬u_{4}}
Γ_{4} = {u_{4} ← ¬u_{1}, ¬u_{2}, ¬u_{3}}

Let Γ then be ⋃_{k=0}^{4} Γ_{k}. By inspection, Stab(Γ) = {{u_{1}}, {u_{0}, u_{2}}, {u_{0}, u_{3}}, {u_{0}, u_{4}}}, as desired. □

From the preceding theorem we can also derive the following characterization of stable model classes which does not mention minimal model classes:

Theorem 3.2 (Characterization of stable model classes (II)) For S ⊆ 2^{U} with the inverse–Scott topology, the following are equivalent:

(i) S is a stable model class. (ii) S is an antichain and a G_{δ} subset of a closed set. (iii) S is an antichain and a G_{δ} subset of S̃. (iv) S is an antichain and a G_{δ} subset of S̄.

Proof: As before, we may assume that S ≠ ∅.

(i) ⇒ (ii) Recall from the introduction that a stable model class forms an antichain. Suppose now that S = Stab(P). Then

S = {S : (U, S, u⃗_{u∈U}) ⊧ σ_{P} }
= {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S]}
= ⋂_{u∈U}{S : ( ⋁_{A∈Ψ_{u}} A⃗ ∉ S) → u ∈ S} ∩ ⋂_{u∈U}{S : u ∈ S → ⋁_{A∈Ψ_{u}} A⃗ ∉ S}
= ⋂_{u∈U}{S : ( ⋀_{A∈Ψ_{u}} ⋁_{a∈A} a ∈ S) ∨ u ∈ S} ∩ ⋂_{u∈U}{S : u ∉ S ∨ ⋁_{A∈Ψ_{u}} A⃗ ∉ S}.

We note that each set {S : u ∉ S ∨ ⋁_{A∈Ψ_{u}} A⃗ ∉ S} is open, and that the set ⋂_{u∈U}{S : (⋀_{A∈Ψ_{u}} ⋁_{a∈A} a ∈ S) ∨ u ∈ S} is closed (and is in fact Mod(P †)).

(ii) ⇒ (iii) We are given that S = F ∩ ⋂_{k∈ω} G_{k} for open sets G_{k} and closed set F. We wish to show that S = S̃ ∩ ⋂_{k∈ω} G_{k}. By definition of closure, S ⊆ S̃ ⊆ F, and by assumption S ⊆ ⋂_{k∈ω} G_{k}. So

S ⊆ S̃ ∩ ⋂_{k∈ω} G_{k} ⊆ F ∩ ⋂_{k∈ω} G_{k} = S.

(iii) ⇒ (iv) We are given that S = S̃∩⋂_{k∈ω} G_{k} for open sets G_{k}. We can show that S = S̄∩⋂_{k∈ω} G_{k} by the same argument as for (ii) ⇒ (iii), but based on the relation S ⊆ S̄ ⊆ S̃ in place of S ⊆ S̃ ⊆ F.

(iv) ⇒ (i) We are given that S is an antichain and S = S̄ ∩ ⋂_{k∈ω} G_{k} for open sets G_{k}. To show that S is a stable model class, by Theorem 3.1 it will suffice to show that S = (min S̄) ∩ ⋂_{k∈ω} G_{k}. (⊇) On the one hand, (min S̄) ∩ ⋂_{k∈ω} G_{k} ⊆ S̄ ∩ ⋂_{k∈ω} G_{k} = S. (⊆) To show the other inclusion, let S ∈ S. By assumption, S ∈ ⋂_{k∈ω} G_{k}, so it remains to show that S ∈ min S̄. Let T then be an element of S̄ with T ⊆ S. Since open sets are specified by negative information, S ∈ ⋂_{k∈ω} G_{k} ⇒ T ∈ ⋂_{k∈ω} G_{k}. Hence T ∈ S. But because S is an antichain, T = S. Therefore S ∈ min S̄, as desired. □

To this point, it has been useful to concentrate on the inverse Scott topology. Now we observe that, for any minimal model class, the topology it inherits as a subspace of (2^{U}, Cantor) is the same as the topology it inherits from (2^{U}, Scott^{−1}) :

Lemma 3.1 Let P be a program. Let S ⊆ 2^{U} be an open subset of Min(P) in the topology on Min(P) inherited from (2^{U}, Cantor). Then S is open in the topology on Min(P) inherited from (2^{U}, Scott^{−1}) as well.

Proof: Let μ_{P} =

⋀_{u∈U}(u ∈ S ↔ ⋁_{W ∈Φ_{u}} W⃗ ∉ S)

be a system of defining equations for Min(P) as in Theorem 2.5. Let

B = {S : ⋀_{a∈A} a ∈ S ∧ ⋀_{b∈B} b ∉ S}

be a basic open subset of (2^{U}, Cantor). Obtain a new set

B′ = {S : ⋀_{a∈A} ⋁_{W ∈Φ_{a}} W⃗ ∉ S ∧ ⋀_{b∈B} b ∉ S}

by replacing each expression of the form a ∈ S in the definition of B by the right–hand side of the defining equation for a in μ_{P} . Clearly

Min(P) ∩ B = Min(P) ∩ B′.

Since A and B are finite, B′ is an open subset of (2^{U}, Scott^{−1}). □

This observation gives a third form of the characterization theorem for stable models classes, which will be useful in Chapters 5 and 7:

Theorem 3.3 (Characterization of stable model classes (III)) For S ⊆ 2^{U} \underline{with the Cantor topology}, the following are equivalent:

(i) S is a stable model class. (ii) S is a G_{δ} subset of a minimal model class. (iii) S is a G_{δ} subset of min S̃. (iv) S is a G_{δ} subset of min S̄.

Proof: By the preceding lemma, each of items (ii), (iii), and (iv) is equivalent to the corresponding item of Theorem 3.1. □

We can now use these results to show by example that the antichain and Cantor G_{δ} properties mentioned in the Introduction are not sufficient to characterize stable model classes:

Example 3.2 Consider again the set S = {{u_{0}}, {u_{1}}, {u_{2}}, …} of Examples 2.1 and 2.2, which, as noted there, is both a G_{δ} set in the Cantor sense and an antichain. We see that min S̄ = {∅}, since ∅ ∈ S̄. Because S then is not a G_{δ} subset of min S̄, by Theorem 3.1 S cannot be a stable model class. □

Finally we use the characterization theorems for minimal and stable model classes to give an example of a stable model class which cannot be realized as a minimal model class:

Example 3.3 Let

S_{0} = {u_{2n} : n ∈ ω, n ≠ 0} ∪ {u_{1}}
S_{1} = {u_{2n} : n ∈ ω, n ≠ 1} ∪ {u_{3}}
S_{2} = {u_{2n} : n ∈ ω, n ≠ 2} ∪ {u_{5}}
⋮
S_{k} = {u_{2n} : n ∈ ω, n ≠ k} ∪ {u_{2k+1}}
⋮

and

S_{∗} = {u_{2n} : n ∈ ω}.

Let S = {S_{k} : k ∈ ω}. Then S̄ = S ∪ {S_{∗}} = min S̄. By Theorem 2.2, S is not a minimal model class, because S ≠ min S̄. However, S is an open subset of min S̄ (or S̄), namely

S = (min S̄) ∩ {S : u_{0} ∉ S ∨ u_{2} ∉ S ∨ u_{4} ∉ S ∨ …}.

So, by Theorem 3.1 (or Theorem 3.2), S is in fact a stable model class.

Furthermore, we can proceed systematically to find a program representing S as a stable model class. By using Algorithm 2.2, we first obtain the following program P_{0} for which S̄ is the class of minimal models:

u_{1} ← ¬u_{0}
u_{2} ← ¬u_{0}
u_{4} ← ¬u_{0}
u_{6} ← ¬u_{0}
u_{8} ← ¬u_{0}
⋮
u_{3} ← ¬u_{2}
u_{4} ← ¬u_{2}
u_{6} ← ¬u_{2}
u_{8} ← ¬u_{2}
⋮
u_{5} ← ¬u_{4}
u_{6} ← ¬u_{4}
u_{8} ← ¬u_{4}
⋮
u_{2j+1} ← ¬u_{2j}
u_{2k} ← ¬u_{2j} for k > j
⋮

Then we obtain a program Γ_{0} for which S is the set of stable models by applying the procedure in the proof of Theorem 3.1 to S as a G_{δ} subset of Min(P_{0}) :

u_{0} ← ¬u_{2}
u_{0} ← ¬u_{4}
u_{0} ← ¬u_{6}
⋮
u_{1} ← ¬u_{0}
u_{2} ← ¬u_{0}
u_{2} ← ¬u_{4}
u_{2} ← ¬u_{6}
⋮
u_{3} ← ¬u_{2}
u_{4} ← ¬u_{0}
u_{4} ← ¬u_{2}
u_{4} ← ¬u_{6}
⋮
u_{5} ← ¬u_{4}
⋮
u_{2j+1} ← ¬u_{2j}
u_{2j} ← ¬u_{2k} for k ≠ j
⋮
□

FINITE PROOF SUPPORT PROPERTY

In [36], the following property was introduced: A program P is said to be \underline{locally finite} if for each atom u of the Herbrand base there are at most finitely many minimal proof schemes from P with conclusion u. In [33], the notion was generalized as follows: A program P is said to have the \underline{finite proof support} property^{1} if for each atom u of the Herbrand base there are at most finitely many distinct minimal supports of proof schemes from P with conclusion u. (Recall that the support of any proof scheme is itself a finite set; the property however concerns finiteness of collections of supports.) In this section we will characterize the stable model classes of finite proof support programs.

We observe first that, as far as minimal model classes are concerned, there is no difference between arbitrary programs and programs with the finite proof support property:

Proposition 4.1

(a) Let S ⊆ 2^{U} be the class of models of a prerequisite–free program. Then there is a program P with the finite proof support property such that S = Mod(P).

(b) Let S ⊆ 2^{U} be a minimal model class. Then there is a program P with the finite proof support property such that S = Min(P).

1 In [33] this was called just the \underline{finite support} property, or fsp. We prefer the longer name to chapter.

emphasize the distinction between structures studied here and the supported models of the next

Proof:

(a) Let P_{0} be a prerequisite–free program such that S = Mod(P_{0}). Let < be an ordering of type ω on U. To obtain a program P with the finite proof support property, replace each clause ρ of P_{0} by the clause

c ← ¬\overline{(B − \{c\})},

where B is the set of atoms which appear in ρ (as head or in the body) and c is the greatest element of B. Each clause of P has the same models as the corresponding clause of P_{0}, so Mod(P) = Mod(P_{0}) = S. Since P is prerequisite–free, each minimal proof scheme for a given c ∈ U corresponds to a clause of P with c as its head. And for each c ∈ U there can be only finitely many such clauses, because each corresponds to a subset of {u : u < c}.

(b) Let P_{1} be a program for which S = Min(P_{1}). By Theorem 2.4, there is a prerequisite–free program P′_{1} with the same minimal models as P_{1}. By part (a) there is then a finite proof support program P with the same models, and therefore the same minimal models, as P′_{1}. □

On the other hand, it is not the case that every stable model class can be realized using a finite proof support program. From the following theorem characterizing stable model classes of finite proof support programs, it will be seen that these sets have a simpler form than the stable model classes of arbitrary programs.

As mentioned in Chapter 1, in [35] a one–to–one correspondence was established between stable model classes of programs with the finite proof support property and closed subsets of (2^{U}, Cantor), with the property that the same Turing degrees are represented in each. In one direction, the argument given in [35] shows that for any finite proof support program P there is a tree T ⊆ 2^{<ω} recursive in P such that the infinite paths through T are the characteristic functions of the stable models of P. This shows that the stable model class of a finite proof support program is itself actually a closed subset of (2^{U}, Cantor). The same conclusion follows also from Marek’s result in [33] that a program P has the finite proof support property if and only if the function F_{P} is continuous in the sense of the Cantor topology, where F_{P} : 2^{U} → 2^{U} is defined by

F_{P} (S) = T_{GL(S,P)} ↑ ω(∅),

since the fixed points of F_{P} are the stable models of P, and the set of fixed points of a continuous function is closed. For our theorem, however, the simple evaluation included below is all that is required. In the converse direction, the proof of the result in [35] involves a degree–preserving mapping from a given closed set in one space to a stable model class actually in a different space. In Chapter 7 we will consider correspondences under that mapping. Here, however, with the object of characterizing stable model classes themselves rather than the classes of the degrees of their elements, we will show that every closed subset of (2^{U}, Cantor) which is an antichain can itself be realized as the collection of stable models of some finite proof support program over U.

Theorem 4.1 (Characterization of stable model classes of programs with finite proof support property) For S ⊆ 2^{U}, the following are equivalent:

(i) S is an antichain and closed in (2^{U}, Cantor). (ii) S is the stable model class of a program with the finite proof support property.

Proof: (ii) ⇒ (i) As shown in the introduction (Chapter 1), S is an antichain. Let P be a program with the finite proof support property such that S = Stab(P). For each u ∈ U there is a \underline{finite} collection Ψ_{u} of finite subsets of U associated with P such that

S = {S : for each u ∈ U, u ∈ S ↔ ⋁_{A∈Ψ_{u}} A⃗ ∉ S}

= ⋂_{u∈U}{S : (u ∉ S ∨ ⋁_{A∈Ψ_{u}} A⃗ ∉ S) ∧ (u ∈ S ∨ ⋀_{A∈Ψ_{u}} ⋁_{a∈A} a ∈ S)}.

Since each Ψ_{u} is finite, the set defined by this expression is closed in (2^{U}, Cantor).

(i) ⇒ (ii) Now suppose that the set S is an antichain and is closed in (2^{U}, Cantor). We will find a finite proof support program P̂ such that S = Stab(P̂).

If S = ∅, we may take as P̂ the program consisting of a single clause

u ← ¬u,

where u is any element of U.

So assume throughout the remainder that S ≠ ∅. By Proposition 2.2, S closed in (2^{U}, Cantor) implies that S^{⊇} is closed in (2^{U}, Scott^{−1}). Since S then satisfies condition (ii) of Theorem 2.2, S is a minimal model class, say S = Min(P). By Theorem 2.5, S is specified by a system μ_{P} of defining equations; that is,

S = {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S]}  (4.4)

where each Φ_{u} is a collection of finite subsets of U. Recall that, by construction, if A ∈ Φ_{u} and y ∈ A, then A − {y} ∪ {u} ∈ Φ_{y}.

As noted previously (preceding Theorem 3.1), the program Γ consisting of all clauses

u ← ¬A⃗

with u ∈ U and A ∈ Φ_{u} has S as its class of stable models. We will select a suitable subset of Γ with the finite proof support property as the program P̂.

First, in order to limit the models of our constructed program to S^{⊇}, for each u ∈ U let Q̂_{u} consist of those clauses

u ← ¬A⃗

with A ∈ Φ_{u} such that u ≥ a for all a ∈ A.

It remains to supply enough clauses to support the elements of each set S ∈ S. Since S is closed, for each u ∈ U the set

S ∩ {S : u ∈ S}

is a closed subset of the compact space (2^{U}, Cantor), hence is itself compact. Since

{{S : A⃗ ∉ S} : A ∈ Φ_{u}}

is an open cover of S ∩ {S : u ∈ S}, there is some finite subset Φ̂_{u} of Φ_{u} such that

S ∩ {S : u ∈ S} ⊆ ⋃{{S : A⃗ ∉ S} : A ∈ Φ̂_{u}}.  (4.5)

Let P̂_{u} consist of those clauses

u ← ¬A⃗

such that A ∈ Φ̂_{u}.

Now let P̂ = ⋃_{u∈U}(P̂_{u} ∪ Q̂_{u}). As desired, P̂ has the finite proof support property. We will show that S = Stab(P̂).

We note first that, since P̂ is prerequisite–free,

T_{GL(S′,_{P})} ↑ ω(∅) = T_{GL(S′,_{P})}(∅)
= {u ∈ U : u ← is a clause of GL(S′, P̂)}
= {u ∈ U : there is a clause u ← ¬A⃗ in P̂ with A⃗ ∉ S′}

for each S′ ⊆ U.

(⊆) Let S ∈ S. We will show that S ∈ Stab(P̂) by showing that S = T_{GL(S,_{P})} ↑ ω(∅). By the preceding observation, it will suffice to show that

S = {u ∈ U : there is a clause u ← ¬A⃗ in P̂ with A⃗ ∉ S}.

(a) Let u ∈ S. By (4.5), there is some A ∈ Φ̂_{u} such that A⃗ ∉ S. By construction, the clause

u ← ¬A⃗

belongs to P̂.

(b) Suppose that there is a clause

u ← ¬A⃗

in P̂ such that A⃗ ∉ S. By definition of P̂, A ∈ Φ_{u}. Then, because S ∈ S satisfies the system μ_{P} of defining equations (as in (4.4)), u ∈ S.

(⊇) Now let S ∈ Stab(P̂). To show that S ∈ S, we will show that S satisfies each defining equation

u ∈ S ↔ ⋁_{A∈Φ_{u}} A⃗ ∉ S

in μ_{P} .

(a) Let u ∈ S. Since S ∈ Stab(P̂), there is some clause

u ← ¬A⃗

in P̂ such that A⃗ ∉ S. By definition of P̂, the set A is an element of Φ_{u}.

(b) Suppose that A ∈ Φ_{u} with A⃗ ∉ S. \underline{Case 1}. If u ≥ a for all a ∈ A, then the clause

u ← ¬A⃗

belongs to Q̂_{u} ⊆ P̂. Since S ∈ Mod(P̂), u ∈ S. \underline{Case 2}. Otherwise let y = max A. As observed above, A − \{y\} ∪ \{u\} ∈ Φ_{y}. So the clause

y ← ¬\overline{(A − \{y\} ∪ \{u\})}

belongs to Q̂_{y} ⊆ P̂. We know that y ∉ S (since y ∈ A). Because S ∈ Mod(P̂), some element of A − {y} ∪ {u} belongs to S. By assumption A⃗ ∉ S, so it must be that u ∈ S. □

Example 4.1 Let

S_{0} = {u_{2n} : n ∈ ω, n ≠ 0} ∪ {u_{1}}
S_{1} = {u_{2n} : n ∈ ω, n ≠ 1} ∪ {u_{3}}
S_{2} = {u_{2n} : n ∈ ω, n ≠ 2} ∪ {u_{5}}
⋮
S_{k} = {u_{2n} : n ∈ ω, n ≠ k} ∪ {u_{2k+1}}
⋮

and

S_{∗} = {u_{2n} : n ∈ ω}.

Let S = {S_{k} : k ∈ ω} ∪ {S_{∗}}. Since S is both closed in (2^{U}, Cantor) and an antichain, according to Theorem 4.1 there is a finite proof support program for which S is the class of stable models. We will follow the approach in the proof of the theorem to find such a program.

We can start with any program which represents S as a minimal model class. One such representation is the program P_{0} obtained as an intermediate step in Example 3.3:

u_{1} ← ¬u_{0}
u_{2} ← ¬u_{0}
u_{4} ← ¬u_{0}
u_{6} ← ¬u_{0}
u_{8} ← ¬u_{0}
⋮
u_{3} ← ¬u_{2}
u_{4} ← ¬u_{2}
u_{6} ← ¬u_{2}
u_{8} ← ¬u_{2}
⋮
u_{5} ← ¬u_{4}
u_{6} ← ¬u_{4}
u_{8} ← ¬u_{4}
⋮
u_{2j+1} ← ¬u_{2j}
u_{2k} ← ¬u_{2j} for k > j
⋮

The defining equations for S as the collection of minimal models of P are as follows:

u_{0} ∈ S ↔ u_{1} ∉ S ∨ u_{2} ∉ S ∨ u_{4} ∉ S ∨ u_{6} ∉ S ∨ …
u_{1} ∈ S ↔ u_{0} ∉ S
u_{2} ∈ S ↔ u_{3} ∉ S ∨ u_{0} ∉ S ∨ u_{4} ∉ S ∨ u_{6} ∉ S ∨ …
u_{3} ∈ S ↔ u_{2} ∉ S
⋮
u_{2j} ∈ S ↔ u_{2j+1} ∉ S ∨ ⋁_{k≠j} u_{2k} ∉ S
u_{2j+1} ∈ S ↔ u_{2j} ∉ S
⋮

As in the proof, we can then form the clauses of each Q̂_{u} as follows:

Q̂_{0} : No clauses  Q̂_{1} :  u_{1} ← ¬u_{0}
Q̂_{2} : u_{2} ← ¬u_{0}  Q̂_{3} :  u_{3} ← ¬u_{2}
Q̂_{4} : u_{4} ← ¬u_{0}  Q̂_{5} :  u_{5} ← ¬u_{4}
u_{4} ← ¬u_{2}
Q̂_{6} : u_{6} ← ¬u_{0}  Q̂_{7} :  u_{7} ← ¬u_{6}
u_{6} ← ¬u_{2}
u_{6} ← ¬u_{4}

⋮

Q̂_{2k} : u_{2k} ← ¬u_{2j} for all j < k  Q̂_{2k+1} : u_{2k+1} ← ¬u_{2k}

⋮ Before continuing, we make the following observations about Q̂ = ⋃_{u∈U} Q̂_{u} :

(a) Q̂ has the finite proof support property.

(b) Q̂ represents S as a minimal model class; that is, S = Min(Q̂). (In fact, Q̂ is the canonical program obtained as in Algorithm 2.2 for representing S as a minimal model class, which is the same as the initial representation P_{0} we chose in this example.)

(c) Q̂ does not have enough clauses to represent S as a stable model class. Consider for instance the set S_{3} = {u_{0}, u_{2}, u_{4}, u_{7}, u_{8}, u_{10}, …}, which is a member of S. None of the first three elements of S_{3} is S_{3}–provable using the clauses of Q̂; that is, u_{0}, u_{2}, and u_{4} are not elements of T_{GL(S_{3},_{Q})} ↑ ω(∅). So S_{3} is not a stable model of Q̂.

It remains then to form the clauses of each P̂_{u} as follows:

P̂_{0} : u_{0} ← ¬u_{1}  P̂_{1} :  u_{1} ← ¬u_{0}
P̂_{2} : u_{2} ← ¬u_{3}  P̂_{3} :  u_{3} ← ¬u_{2}

⋮

P̂_{2k} : u_{2k} ← ¬u_{2k+1} P̂_{2k+1} : u_{2k+1} ← ¬u_{2k}

⋮

Finally, let P̂ = ⋃_{u∈U}(P̂ ∪ Q̂). Then P̂ has the finite proof support property and S = Stab(P̂). □

In this chapter and Chapters 2 and 3 we have characterized (i) stable model classes of finite proof support programs, (ii) minimal model classes, and (iii) stable model classes of arbitrary programs. Theorems 4.1, 2.2, and 3.1 show that, as properties, they are arranged here in order from stronger to weaker; that is, (i) ⇒ (ii) ⇒ (iii). Example 3.3, where we presented a set which is a stable model class but not a minimal model class, shows that property (ii) is strictly stronger than property (iii). Similarly we present next an example to distinguish between (i) and (ii):

Example 4.2 Let U = ω, and let S = {ω − {0}, ω − {1}, ω − {2}, …}. We will show that S is a minimal model class which is not the class of stable models of any finite proof support program. Note first that S is an antichain. To show that S is a minimal model class, it suffices then to show that S^{⊇} is closed in (2^{ω}, Scott^{−1}). We express S^{⊇} as an intersection of basic closed subsets of (2^{ω}, Scott^{−1}) as follows:

S^{⊇} = S ∪ {ω}
= {S : (0 ∉ S → 1 ∈ S) ∧ (0 ∉ S → 2 ∈ S) ∧ (0 ∉ S → 3 ∈ S) ∧ …
∧ (1 ∉ S → 0 ∈ S) ∧ (1 ∉ S → 2 ∈ S) ∧ (1 ∉ S → 3 ∈ S) ∧ …
∧ … }
= ⋂_{i∈ω} ⋂_{j∈ω,j≠i}{S : i ∉ S → j ∈ S}.

By Theorem 2.2, then, S is a minimal model class. On the other hand, since ω ∈ (S̄ − S), the set S itself is not closed, even in (2^{U}, Cantor). So by Theorem 4.1 S is not the stable model class of a finite proof support program. □

In the next chapters we will study logic programming classes which are not necessarily antichains.

SUPPORTED MODEL CLASSES

Another type of structure which arises in connection with the semantics of logic programming is the supported model. Recall from the introduction that a supported model of a program P is a fixpoint of the operator T_{P} , or equivalently a model in the sense of propositional logic of the completion of P consisting of all formulas

u ↔ ⋁_{(A,B)∈Σ_{u}}( ⋀_{a∈A} a ∧ ⋀_{b∈B} ¬b)

for u ∈ U, where Σ_{u} is the set of pairs (A, B) of finite subsets of U such that

u ← A⃗, ¬B⃗

is a clause of P. The collection of supported models of P we denote by Supp(P), and we call S ⊆ 2^{U} a supported model class if S = Supp(P) for some program P. In this section we find a mathematical characterization for supported model classes.

As discussed in Section 1.2, supported models are the intended models associated with a type of nonmonotonic reasoning based on both positive and negative introspection—that is, on both presence and absence of information in a designated interpretation or “context.” Because they depend partly on presence of information, supported models, unlike minimal and stable models, are not constrained to form an antichain. For instance, the supported models of the program

r ← ¬s

p ← q
q ← p

are {r} and {r, p, q}. In general it is not possible to represent a supported model class using a prerequisite–free program, nor to specify a supported model class by a set of defining equations with purely negative conditions on the right–hand side, because these means produce only antichains. We will show, however that a given supported model class can be represented by a program in a canonical form of a different sort. Moreover, as pointed out in the introduction, the conditions

u ∈ S ↔ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)

for u ∈ U obtained from the completion of a program P function as defining equations for the supported models of P.

Just as nearness of interpretations should be measured by absence of information, as in the inverse–Scott topology, when considering default reasoning, so in this case should nearness be specified by both presence and absence of information, as in the Cantor topology. Supported model classes should be identifiable then as subsets with certain properties in (2^{U}, Cantor). In Theorem 5.1, we will use the defining equations to show that every supported model class is a G_{δ} subset of (2^{U}, Cantor). However, the same example we have considered previously shows that this condition by itself is not enough to characterize supported model classes:

Example 5.1 Let S = {{u_{0}}, {u_{1}}, {u_{2}}, …}, as in Examples 2.1 and 3.2. Recall that S is a G_{δ} subset of (2^{U}, Cantor). We claim, however, that S is not a supported model class. For suppose that S = Supp(P). Then ∅ ∈ Mod(P), since ∅ ∈ S̄ and S̄ ⊆ Mod(P), which means that T_{P} (∅) ⊆ ∅. But then ∅ is actually a fixed point of T_{P} , because ∅ ⊆ T_{P} (∅) is vacuously true. Hence ∅ ∈ Supp(P) = S, which is a contradiction. □

To rule out sets such as that of Example 5.1, some more restrictive condition is needed. Such a condition might be sought in the relationship of the minimal elements of a supported model class to models of other sorts. We will show next, however, that certain additional conditions of this sort are too strong by presenting examples of supported model classes for which these properties fail:

Example 5.2 Recall from the introduction that, for a given program P, every stable model of P is both a supported and a minimal model of P; that is,

Stab(P) ⊆ Supp(P) ∩ Min(P).

In general, however, it is not the case that

Stab(P) = Supp(P) ∩ Min(P).

For instance, if P_{1} is the program

p ← ¬q
q ← q,

the model {q} of P_{1} is both supported and minimal, but not stable. □

Example 5.3 In the preceding example the minimal elements {p} and {q} of Supp(P_{1}) are both minimal models of P_{1}. In general, however,

min Supp(P) ⊈ Min(P).

For example, in the program P_{2} given by

a ← ¬b
b ← a
b ← c
c ← c,

{b, c} is the only supported model and {b} the only minimal model. □

Example 5.4 In fact, it may happen that the minimal elements of a supported model class are not among the minimal models of any program at all. For example, let P_{3} be the program

u_{1} ← u_{2}
u_{1} ← u_{3}
u_{1} ← u_{4}
⋮
u_{2} ← u_{2}
u_{3} ← u_{3}
u_{4} ← u_{4}
⋮
u_{2} ← ¬u_{1}.

Let S = min Supp(P_{3}). Then

S = {{u_{1}, u_{j}} : j > 1}

and

min S̄ = {{u_{1}}}.

According to Theorem 2.3, since

S ⊈ min S̄,

there is no minimal class of which S is a subset. □

Example 5.5 Even a supported model class which is itself an antichain need not be a subset of a minimal model class. Consider the program P_{4} formed by adding the clauses

u_{0} ← u_{i}, u_{j}, ¬u_{0}

for i, j > 1, i ≠ j, to the program P_{3} of the last example. We claim that S =

{{u_{1}, u_{2}}, {u_{1}, u_{3}}, {u_{1}, u_{4}}, …}

is the set of supported models of P_{5} (as well as the minimal supported models of P_{3} in Example 5.4). It is easily checked that each element of S is a supported model of P_{4}. So we need to check that there are no other supported models:

• The empty set is not a model.

• Singletons: {u_{1}} is a model, but is not supported. For i ≠ 1, {u_{i}} is not a model.

• Pairs: {u_{0}, u_{1}} is a model, but is not supported. If i ≠ 1 and also j ≠ 1, the pair {u_{i}, u_{j}} is not a model.

• Sets with three or more elements: If S has at least three elements and is a model

of P_{4}, then u_{0} ∈ S. But no set with u_{0} as an element is supported. We see then that S is a supported model class and an antichain. Notice, however, that {u_{1}} ∈ S̄, so it is not the case that S ⊆ min S̄. By Theorem 2.3, there is no minimal model class containing S. □

Example 5.6 Finally we observe that a supported model class, though nonempty, may have no elements which are minimal. Let P_{5} be the program P_{3} of Example 5.4 together with the additional clauses

u_{3} ← u_{2}
u_{4} ← u_{3}
u_{5} ← u_{4}
⋮

For this program, the supported models are the sets of the form

{u_{1}} ∪ {u_{i} : i ≥ N}

for N ≥ 2, so min Supp(P_{5}) = ∅. □

In fact, the argument used in Example 5.1 to show that the G_{δ} set {{u_{0}}, {u_{1}}, …} is not a supported model class pinpoints exactly the additional property which characterizes these classes:

Theorem 5.1 (Characterization of supported model classes) For S ⊆ 2^{U}, the following are equivalent:

(i) S is a supported model class. (ii) S is a G_{δ} subset of (2^{U}, Cantor) such that ∅ ∉ S̄ − S.

Proof: (i) ⇒ (ii) Let P be a program for which S = Supp(P), and let cmp_{P} be the sentence of L_{ω_{1},ω}^{U}, as described in Section 1.4, which specifies its supported models. Then

S = Supp(P)
= {S : (U, S, u⃗_{u∈U}) ⊧ cmp_{P} }
= {S : ⋀_{u∈U}[u ∈ S ↔ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)]}
= ⋂_{u∈U}{S : u ∉ S ∨ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)} ∩

⋂_{u∈U}{S : u ∈ S ∨ ⋀_{(A,B)∈Σ_{u}}( ⋁_{a∈A} a ∉ S ∨ ⋁_{b∈B} b ∈ S)}

= ⋂_{u∈U}{S : u ∉ S ∨ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)} ∩

⋂_{u∈U} ⋂_{(A,B)∈Σ_{u}}{S : u ∈ S ∨ ⋁_{a∈A} a ∉ S ∨ ⋁_{b∈B} b ∈ S}.

This provides an expression for S as a countable intersection of open subsets of (2^{U}, Cantor).

To establish the second condition, suppose that ∅ ∈ S̄. Since S ⊆ Mod(P) and Mod(P) is a closed subset of (2^{U}, Cantor), S̄ ⊆ Mod(P). So ∅ ∈ Mod(P); that is, T_{P} (∅) ⊆ ∅. But then ∅ is actually a fixed point of T_{P} , because ∅ ⊆ T_{P} (∅) is vacuously true. Hence ∅ ∈ S = Supp(P).

(ii) ⇒ (i) If S = ∅, we may take as Γ the program

u ← ¬u

for any u ∈ U, which has no supported models. So we assume throughout the remainder that S ≠ ∅.

Let U = {u_{k} : k < |U|}. Suppose that S = ⋂_{k∈ω} G_{k} for open sets G_{k}. As in the proof of Theorem 3.1, we “preprocess” the list (G_{k})_{k∈ω} as follows: For each k ∈ ω, let

F_{k} = {S ⊆ U : S is finite, max{i : u_{i} ∈ S} = k, and S ∉ ⋂_{i∈ω} G_{i}}

and

G′_{k} = G_{k} − F_{k}.

To simplify the construction, also let

G′′_{k} = ⋂_{i≤k} G′_{k}

for each k ∈ ω.

As in Theorem 3.1, we observe that:

(i) Since F_{k} is finite and hence closed, G′_{k} is open. Then G′′_{k}, as the intersection of finitely many open sets, is open as well. So G′′_{k} can be expressed in the form

G′′_{k} = ⋃_{(A,B)∈Σ_{k}}{S : A⃗ ∈ S ∧ B⃗ ∉ S}

for some collection Σ_{k} of pairs of finite subsets of U.

(ii) ⋂_{k∈ω} G_{k} = ⋂_{k∈ω} G′_{k} = ⋂_{k∈ω} G′′_{k}, and G′′_{0} ⊇ G′′_{1} ⊇ G′′_{2} ⊇ ….

(iii) For any finite set S ⊆ U, if S ∈ G′′_{j} where j = max{i : u_{i} ∈ S}, then S ∈ G_{k} for every k ∈ ω.

Now, for each k < |U|, let Γ_{k} consist of all clauses of the form

u_{k} ← u_{k}, A⃗, ¬B⃗

for (A, B) ∈ Σ_{k}.

To this point, the clauses we have constructed limit the nonempty sets which can occur as supported models. It remains to treat the empty set. If ∅ ∈ S, then no additional clauses are needed, and we let Γ_{−1} be empty. If ∅ ∉ S, then also ∅ ∉ S̄, by the condition stated in the theorem. So there is a basic open set O with ∅ ∈ O such that O ∩ S = ∅. Since ∅ ∈ O, only negative information is involved in the definition of O, so

O = {S : u_{i_{1}} ∉ S ∧ … ∧ u_{i_{n}} ∉ S}

for some u_{i_{1}}, …, u_{i_{n}} ∈ U. Then for every S ∈ S

u_{i_{1}} ∈ S ∨ … ∨ u_{i_{n}} ∈ S,

since S ⊆∼O. In this case we let Γ_{−1} consist of the single clause

u_{i_{1}} ← ¬u_{i_{1}}, ¬u_{i_{2}}, …, ¬u_{i_{n}}.

Note that this clause holds (because the body is false) on every S ∈ S, and that it does not hold on the empty set.

Now let Γ = ⋃_{k≥−1} Γ_{k}. We will show that S = Supp(Γ).

(⊆) Let S ∈ S. We will show that S ∈ Supp(Γ) by showing that S = T_{Γ}(S).

(a) First we show that S ⊆ T_{Γ}(S) : Let u_{ℓ} ∈ S. Since S ∈ ⋂_{k∈ω} G_{k} ⊆ G′′_{ℓ}, there is a pair (A, B) ∈ Σ_{ℓ} such that A ⊆ S and B ∩ S = ∅. So u_{ℓ} ∈ T_{Γ}(S) by the clause

u_{ℓ} ← u_{ℓ}, A⃗, ¬B⃗

of Γ_{ℓ}.

(b) Now we show that T_{Γ}(S) ⊆ S : Let u_{ℓ} ∈ T_{Γ}(S). There is then some clause γ in Γ whose body holds on S and whose head is u_{ℓ}. We know that γ ∉ Γ_{−1} since, if there is a clause in Γ_{−1}, its body does not hold on S. Hence γ belongs to Γ_{ℓ}, say γ =

u_{ℓ} ← u_{ℓ}, A⃗, ¬B⃗.

Since the body of γ holds on S and u_{ℓ} occurs in the body, u_{ℓ} ∈ S.

(⊇) Now let S ∈ Supp(Γ). We will show that S ∈ S = ⋂_{k∈ω} G_{k}. First we show that: (∗) If u_{m} ∈ S, then S ∈ G′′_{m}. Let u_{m} ∈ S. Since S = T_{Γ}(S), there is some clause γ ∈ Γ whose body holds on S and whose head is u_{m}. Suppose (for contradiction) that γ ∈ Γ_{−1}. Then γ has the form

u_{m} ← ¬u_{m}, ¬u_{i_{2}}, …, ¬u_{i_{n}}

for some u_{i_{2}}, …, u_{i_{n}} ∈ U. Since the body of the clause holds on S, u_{m} ∉ S, which contradicts the assumption. Therefore γ ∈ Γ_{m}, say γ =

u_{m} ← u_{m}, A⃗, ¬B⃗

with (A, B) ∈ Σ_{m}. Because the body of γ holds on S, S ∈ G′′_{m}, as desired. Now let ℓ be given. We need to show that S ∈ G_{ℓ} : \underline{Case 1}. Suppose first that S = ∅. Because S ⊧ Γ, Γ_{−1} must be empty and hence ∅ ∈ S.

\underline{Case 2}. Suppose that there is an element u_{m} ∈ S with m ≥ ℓ. By (∗), S ∈ G′′_{m} ⊆ G′′_{ℓ} ⊆ G_{ℓ}. \underline{Case 3}. Otherwise there exists j < ℓ such that u_{j} ∈ S and j = max\{i : u_{i} ∈ S\}. Then S ∈ G′′_{j} by (∗). So by observation (iii) concerning the list (G′′_{k})_{k∈ω}, S ∈ G_{ℓ}. □

Although, as noted above, there is in general no prerequisite–free program which can represent a given supported model class, nonetheless there is a comparable notion of canonical form for this case. The following result will be useful in proving Theorem 6.1 in the next chapter.

Corollary 5.1 (Canonical form representation for supported modelclasses) For every program P, there is a program P § with Supp(P) = Supp(P §) consisting of clauses of the form

u ← u, A⃗, ¬B⃗

for u ∈ U and finite subsets A and B of U, together with at most one clause (which is present if and only if ∅ ∉ Mod(P)) of the form

y ← ¬y, ¬Y

for some y ∈ U and Y a finite subset of U.

Proof: The program obtained in the proof of Theorem 5.1 has the desired form. □

Example 5.7 Let F be any operator on 2^{U} which is monotone and positive–finitizable, as defined in Section 1.1. Recall that then

F ( ⋃_{n∈ω} S_{n}) = ⋃_{n∈ω} F (S_{n})

for S_{0} ⊆ S_{1} ⊆ …. Since U is countable, this is equivalent to the property

F (S) = ⋃{F (A) : A is a finite subset of S}.

We claim that the set of fixed points of F is the same as the set of supported models of some logic program over U. It would be possible to establish this by showing that the set of fixed points satisfies condition (ii) of Theorem 5.1. But in this case it seems more revealing to produce the logic program directly.

Let P consist of all clauses

y ← A⃗

such that y ∈ F (A), where A is any finite subset of U. Then in fact F = T_{P} (that is, F (S) = T_{P} (S) for all S ⊆ U), and consequently the fixed points of F are the same as the supported models of P. Naturally P consists entirely of Horn clauses.

We will make further use of this example in Chapter 7. □

Recall from Example 5.2 at the beginning of this chapter that an interpretation for a given program P may be both a supported and a minimal model of P without being a stable model of P; that is, in general it is not the case that

Stab(P) = Supp(P) ∩ Min(P).

However, from the characterizations of stable and supported model classes, we find a relationship of this sort among classes of models of possibly different programs:

Corollary 5.2 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a stable model class. (ii) S is the intersection of a supported model class with a minimal model class.

Proof: (i) ⇒ (ii) Let P be a program such that S = Stab(P). Let P † be the prerequisite–free program obtained from P as in Proposition 3.1 such that Stab(P) = Stab(P †). Since P † is prerequisite–free, Stab(P †) = Supp(P †). Then, since Stab(P) ⊆ Min(P),

Stab(P) = Supp(P †) ∩ Min(P).

(ii) ⇒ (i) Suppose that

S = S_{1} ∩ S_{2},

where S_{1} is a supported model class and S_{2} is a minimal model class. By the characterization theorem for supported model classes (Theorem 5.1), S_{1} is a G_{δ} subset of (2^{U}, Cantor). Therefore S is a G_{δ} subset of S_{2} in the topology on S_{2} inherited from (2^{U}, Cantor). By Theorem 3.3 of Chapter 3, S is a stable model class. □

As observed in Example 5.5, a supported model class which is an antichain is not necessarily a subset of a minimal model class. If it is, however, then by this corollary it is actually the stable model class of some program. In Chapter 7 we will observe a particular instance of this situation.

FINITE COMPLETION PROPERTY

We consider now a property of programs which is the analogue for supported model semantics of the finite proof support property for stable model semantics. A propositional program P is said to have the \underline{finite completion} property if for each atom u ∈ U there are at most finitely many clauses of P for which u is the head. (For programs which are not propositional, we apply this criterion to the set of ground instances of clauses of the program.^{1}) The finite proof support and finite completion properties are independent of each other. For example, the program

u_{0} ← u_{1}
u_{0} ← u_{2}
u_{0} ← u_{3}
⋮

has the finite proof support property but not the finite completion property, while the program

u_{0} ← ¬u_{1}
u_{0} ← u_{2}

1 So the “covered” predicate logic programs considered by [7], which consist of finitely many clauses in which each variable appearing in the body appears also in the head, have the finite completion property.

u_{2} ← ¬u_{3}
u_{2} ← u_{4}
u_{4} ← ¬u_{5}
u_{4} ← u_{6}

⋮

has the finite completion property but not the finite proof support property.

As with stable model classes of finite proof support programs, the supported model classes of finite completion programs are distinguished among arbitrary supported model classes by their simpler form:

Theorem 6.1 (Characterization of supported model classes of programs with finite completion property) For S ⊆ 2^{U}, the following are equivalent:

(i) S is a closed set in (2^{U}, Cantor). (ii) S is the class of supported models of a program with the finite completion prop-

erty.

Proof: (ii) ⇒ (i) Let P be a program with the finite completion property such that S = Supp(P). For each u ∈ U there is a \underline{finite} set Σ_{u} of pairs (A, B) of finite subsets of U such that

S = {S : for each u ∈ U, u ∈ S ↔ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)}
= ⋂_{u∈U}{S : [u ∉ S ∨ ⋁_{(A,B)∈Σ_{u}}(A⃗ ∈ S ∧ B⃗ ∉ S)] ∧

[u ∈ S ∨ ⋀_{(A,B)∈Σ_{u}}( ⋁_{a∈A} a ∉ S ∨ ⋁_{b∈B} b ∈ S)]}.

Because each Σ_{u} is finite, the set defined by this expression is closed in (2^{U}, Cantor).

(i) ⇒ (ii): Now suppose that S is closed in (2^{U}, Cantor). We will find a program P̂ with the finite completion property such that S = Supp(P̂).

If S = ∅, then the program consisting of a single clause

u ← ¬u

for any u ∈ U has the required properties. So assume throughout the remainder that S ≠ ∅.

Since S is a closed set, it is also a G_{δ} set in (2^{U}, Cantor) with the property that ∅ ∉ (S̄−S). So by Theorem 5.1, S is a supported model class, say S = Supp(P). We may assume that P is in the canonical form for supported models given in Corollary 5.1; that is, for each u ∈ U there is a collection Σ_{u} of pairs (A, B) of finite subsets of U such that P consists of the clauses

u ← u, A⃗, ¬B⃗

for u ∈ U and (A, B) ∈ Σ_{u}, together with at most one clause ξ of the form

y ← ¬y, ¬Y⃗ ,

with Y a finite subset of U, which is present if and only if ∅ ∉ S. We will describe a subset P̂ of P which has the finite completion property and for which S = Supp(P̂).

For each u ∈ U,

{S : S ∈ S ∧ u ∈ S} = S ∩ {S : u ∈ S}

is closed, and hence compact, since S itself is closed. Furthermore

S ∩ {S : u ∈ S} ⊆ ⋃_{(A,B)∈Σ_{u}}{S : u ∈ S ∧ A⃗ ∈ S ∧ B⃗ ∉ S},

since if S ∈ S and u ∈ S, then u is supported on S by the body of some clause other than ξ. By compactness, there is then a finite subset Σ̂_{u} of Σ_{u} such that

S ∩ {S : u ∈ S} ⊆ ⋃_{(A,B)∈_{Σ_{u}}}{S : u ∈ S ∧ A⃗ ∈ S ∧ B⃗ ∉ S}.  (6.6)

Let P̂_{u} consist of those clauses

u ← u, A⃗, ¬B⃗

such that (A, B) ∈ Σ̂_{u}.

Let Q = {ξ} if P has a prerequisite–free clause ξ, and otherwise let Q = ∅. Let P̂ = Q ∪ ⋃_{u∈U} P̂_{u}. Note that P̂ has the finite completion property. We will show that S = Supp(P̂).

(⊆) Let S ∈ S. We will show that S ∈ Supp(P̂) by showing that S = T_{P}(S).

(a) Since P̂ ⊆ P,

T_{P}(S) ⊆ T_{P} (S) = S.

(b) Let u ∈ S. By (6.6), there is some (A, B) ∈ Σ̂_{u} such that A⃗ ∈ S and B⃗ ∉ S. Then S satisfies the body of the clause

u ← u, A⃗, ¬B⃗,

which is one of the clauses of P̂. So u ∈ T_{P}(S).

(⊇) Now let S ∈ Supp(P̂). We will show that S ∈ S = Supp(P) by showing that S = T_{P} (S).

(a) Since P̂ ⊆ P,

S = T_{P}(S) ⊆ T_{P} (S).

(b) We note first that if the prerequisite–free clause ξ of the form

y ← ¬y, ¬Y⃗

belongs to P, by construction it also belongs to P̂. Then by assumption ξ holds on S, which implies that the body of ξ does not.

Let u ∈ T_{P} (S). There is then some clause γ in P whose head is u and whose body holds on S. By what we have just shown, if P has a prerequisite–free clause ξ as above, that clause cannot be γ. Therefore γ has the form

u ← u, A⃗, ¬B⃗

for some finite A, B ⊆ U. Since the body of γ holds on S, we conclude that u ∈ S. □

Example 6.1 Let F be any continuous operator on (2^{U}, Cantor). Then the set of fixed points of F is closed. So by Theorem 6.1 there is a program P with the finite completion property whose supported models are the fixed points of F. □

Recall from Example 5.5 of the preceding chapter that a supported model class which is an antichain is not necessarily a subset of a minimal model class, so in particular is not necessarily a stable model class. Stable and supported model classes of programs with the appropriate finiteness properties, however, do satisfy such a relation:

Corollary 6.1 For S ⊆ 2^{U}, the following are equivalent:

(i) S is the class of stable models of a finite proof support program. (ii) S is an antichain and is the class of supported models of a program with the

finite completion property.

Proof: By Theorems 4.1 and 6.1, both (i) and (ii) are equivalent to: (iii) S is an antichain and a closed subset of (2^{U}, Cantor). □

CHAPTER 7

THE TRANSFORMATION h

Some of the methods of nonmonotonic reasoning described in Section 1.2 have subsequently been extended to systems employing truth values “undefined” and “overdefined” in addition to “true” and “false”. Under this approach, a valuation v corresponds to a pair (S^{+}, S^{−}) of subsets of U, where

v(u) = \{ \begin{matrix}true & if u ∈ (S^{+} − S^{−}) \\ false & if u ∈ (S^{−} − S^{+}) \\ undefined & if u ∉ (S^{+} ∪ S^{−}) \\ overdefined & if u ∈ (S^{+} ∩ S^{−}). \end{matrix}

If S^{+} ∩ S^{−} = ∅, such an interpretation may be called consistent or three–valued; if in addition S^{+}∪S^{−} = U, then it may be called exact or two–valued ([17]). The systems of Fitting ([15]) and Kunen ([27]) generalize the supported model semantics in the sense that, among their intended models, those which are exact are the pairs formed by the supported models and their complements. Similarly in the well–founded semantics of [62] and the stationary semantics of [50, 51], the intended models which are exact are the stable models paired with their complements.

A different generalization to this four–valued setting is provided by “logic programming with classical negation” ([20]). This formalism makes use of an operator “ ¬ ”, to be interpreted as nonmonotonic negation of some sort, as well as an operator “ · ” intended as “classical negation.” A clause is an expression of the form

c ← A⃗, ¬B⃗, where each of the entries a ∈ A, b ∈ B, and c is either an atom or the “classical negation” of an atom. Semantic notions, including interpretations and intended models of various sorts, are determined by treating a “classical negation” program as an ordinary general logic program over an expanded universe U ∪ U̇ containing both the set U of the original atoms and the set U̇ = {u̇ : u ∈ U} of their “classical negations.” An interpretation S ⊆ (U ∪ U̇) of this sort corresponds to the valuation v : U → {true, false, undefined, overdefined} given by

v(u) = \{ \begin{matrix}true & if u ∈ S ∧ u̇ ∉ S \\ false & if u̇ ∈ S ∧ u ∉ S \\ undefined & if u ∉ S ∧ u̇ ∉ S \\ overdefined & if u ∈ S ∧ u̇ ∈ S. \end{matrix}

As above, an interpretation is called consistent if no element of U is valued as overdefined and is called exact if every element of U is valued as either true or false.^{1} If an interpretation S ∈ 2^{U∪U̇} is identified with the pair (S^{+}, S^{−}) ∈ 2^{U} × 2^{U} with S^{+} = S ∩ U and S^{−} = {u : u̇ ∈ (S ∩ U̇)} which is associated with the same valuation, it is clear that “classical negation” programming produces quite a different generalization of ordinary logic programming than the four–valued approaches mentioned above. For instance, if (S_{1}^{+}, S_{1}^{−}) and (S_{2}^{+}, S_{2}^{−}) are distinct stationary models of a given program P which are exact, then S_{1}^{+} and S_{2}^{+} are stable models of P in the original sense and hence are inclusion–incomparable; whereas if S_{1} and S_{2} are exact stable models of a given “classical negation” program, then although S_{1} and S_{2} are

1 In the original version as formulated in [20], a “logic program with classical negation” was considered to contain built–in clauses

u ← v, v̇
u̇ ← v, v̇

for each u, v ∈ U, so that the only inconsistent interpretation permitted as a model of a program is the set U ∪ U̇ itself. Since the results of this section concern exact valuations, it makes no difference here whether or not such built–in clauses are assumed.

inclusion–incomparable as subsets of U ∪ U̇, their positive parts S_{1}^{+} = S_{1} ∩ U and S_{2}^{+} = S_{2} ∩ U may be nested.

Indeed, the extension of a stable representation to classes which are not antichains is the feature for which the “classical negation” approach was developed. In [34] a number of examples were presented of common mathematical constructions which could be represented as the stable models of appropriate logic programs. The last among these was the set of prime ideals of a commutative ring with unit. Since one prime ideal may be a subset of another, it is of course impossible for the ideals themselves to be stable models; rather the ideals taken together with their complements were shown to be the stable models of a “classical negation” program over U ∪ U̇. For this sort of representation, every stable model is required to be exact, so that the one–to–one correspondence

h : S ↦ S ∪ {u̇ : u ∈ (U − S)}

between subsets of U and exact valuations over U ∪U̇ maps the sets to be represented to the stable models of the program. In [35] this correspondence is further applied to the problem of describing the Turing degrees of stable models, since, for each S ⊆ U, S ≡_{T} h(S).

In this section we will determine which subsets of 2^{U} are representable in this extended sense using not only the stable, but also the minimal and the supported model semantics of “classical negation” programs. In [35], in connection with the problem of Turing degrees, it was shown that the image h(S) of any closed subset S of (2^{U}, Cantor) is the stable model class of a finite proof support program over U ∪ U̇; we will include this result, with a different proof, and will also show that every set S with h(S) the stable model class of a finite proof support program is closed. Similarly we will characterize the sets S ⊆ 2^{U} whose image h(S) is the stable, minimal, or supported model class of an arbitrary program or the supported model class of a finite completion program over U ∪ U̇. Naturally these results will make use of the characterization theorems derived in the earlier chapters.

We begin with general properties of the map h defined above. For convenience, let Q ⊆ 2^{U∪U̇} denote the image of 2^{U} under h. For any set A ⊆ U, let Ȧ = {u̇ : u ∈ A}. Throughout this section, it may be helpful to visualize Q as the graph of a certain continuous function.^{2} Namely, let f : (2^{U}, Cantor) → (2^{U}, Cantor) be the function that takes a set S to its complement U − S. Then the graph G_{f} =

{(S, U − S) : S ∈ 2^{U}}

of f is a subset of 2^{U} × 2^{U}. But since U is disjoint from U̇, the mapping

g((X, Y)) = X ∪ Ẏ

from (2^{U}, Cantor)×(2^{U}, Cantor) to (2^{U∪U̇}, Cantor) is a homeomorphism, under which G_{f} corresponds to Q.

The following lemma will be used to transfer results from earlier chapters to this new setting:

Lemma 7.1 As defined above, let h : (2^{U}, Cantor) → (2^{U∪U̇}, Cantor) be the function

h(S) = S ∪ {u̇ : u ∉ S},

and let Q be the set h(2^{U}). Then:

(a) Q is a closed subset of (2^{U∪U̇}, Cantor).

(b) h′ : (2^{U}, Cantor) → (Q, Cantor_{Q}) is a homeomorphism, where h′ is obtained from h by restricting its range and Cantor_{Q} is the subspace topology on Q inherited from (2^{U∪U̇}, Cantor).

(c) S is a closed (resp., G_{δ}) subset of (2^{U}, Cantor) if and only if h(S) is a closed (resp., G_{δ}) subset of (2^{U∪U̇}, Cantor).

2 As pointed out by Steve Ferry.

Proof: We show first that the function h is continuous. Let

O = {W ∈ 2^{U∪U̇} : A⃗ ∈ W ∧ Ċ ∈ W ∧ B⃗ ∉ W ∧ Ḋ ∉ W }

be a basic open subset of (2^{U∪U̇}, Cantor). Then

h^{−1}(O) = {S ∈ 2^{U} : A⃗ ∈ S ∧ C⃗ ∉ S ∧ B⃗ ∉ S ∧ D⃗ ∈ S},

which is a basic open set in (2^{U}, Cantor).

(a) Since (2^{U}, Cantor) is compact and (2^{U∪U̇}, Cantor) is Hausdorff, Q = h(2^{U}) is compact and therefore closed by Theorems 5.5 and 5.3 given in [47].

(b) Since (2^{U}, Cantor) is compact, (2^{U∪U̇}, Cantor) is Hausdorff, and h′ is bijective, by Theorem 5.6 of [47] h′ is a homeomorphism.

(c) \begin{matrix}S is a closed (resp., G_{δ}) subset of (2^{U}, Cantor) \\ ⇔ & h(S) is a closed (resp., G_{δ}) subset of (Q, Cantor_{Q}) \\ ⇔ & h(S) = Z ∩ Q for some closed (resp., G_{δ}) subset Z of (2^{U∪U̇}, Cantor) \\ ⇔ & h(S) is a closed (resp., G_{δ}) subset of (2^{U∪U̇}, Cantor). \end{matrix}

The first equivalence is by part (b), the second by definition of the subspace topology, and the third by part (a). □

Corollary 7.1 Q itself is a minimal model class over U ∪ U̇.

Proof: Q satisfies condition (ii) of Theorem 2.2 characterizing minimal model classes, because Q is an antichain, and, since Q is closed in (2^{U}, Cantor) by the preceding lemma, Q^{⊇} is closed in (2^{U}, Scott^{−1}) by Proposition 2.2. □

Remark 7.1 A program P over U ∪ U̇ for which Q = Min(P) is the program consisting of all clauses

u̇ ← ¬u

for u ∈ U.

Since Q is a minimal model class, we note by Lemma 3.1 that the Cantor topology on Q inherited from (2^{U∪U̇}, Cantor) is the same as the topology inherited by Q as a subspace of (2^{U∪U̇}, Scott^{−1}). Though we will not use this information directly, we will make application below of Theorem 3.3 which was derived in Chapter 3 from Lemma 3.1.

After these preparations, we are ready now to describe sets S for which h(S) has a given structure. We begin with the stable model classes:

Theorem 7.1 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a G_{δ} subset of (2^{U}, Cantor). (ii) h(S) is a stable model class over U ∪ U̇.

Proof: (i) ⇒ (ii) By Lemma 7.1(c), h(S) is a G_{δ} subset of (2^{U∪U̇}, Cantor). Then

h(S) = h(S) ∩ Q

expresses h(S) as the intersection of a G_{δ} subset of (2^{U∪U̇}, Cantor) with a minimal model class over U ∪ U̇ (as shown in Corollary 7.1). By the third form of the characterization theorem (Theorem 3.3), h(S) is then a stable model class over U ∪ U̇. (ii) ⇒ (i) As shown in [36] using defining equations, any stable model class over a given universe is a G_{δ} subset of its power set with the Cantor topology. Applied to h(S), this shows that h(S) is a G_{δ} subset of (2^{U∪U̇}, Cantor). By Lemma 7.1(c), S is a G_{δ} subset of (2^{U}, Cantor). □

Next we show which sets S have the property that h(S) is a minimal model class:

Theorem 7.2 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a closed subset of (2^{U}, Cantor).

(ii) h(S) is a minimal model class over U ∪ U̇.

Proof: (i) ⇒ (ii) By Lemma 7.1(c), h(S) is a closed subset of (2^{U∪U̇}, Cantor). By Proposition 2.2, (h(S))^{⊇} is a closed subset of (2^{U∪U̇}, Scott^{−1}). Furthermore h(S) is an antichain. So by Theorem 2.2 characterizing minimal model classes, h(S) is a minimal model class over U ∪ U̇. (ii) ⇒ (i) Since h(S) is a minimal model class, h(S) also satisfies condition (iv) of Theorem 2.2, namely that

h(S) = min \overline{h(S)}.

Since h(S) ⊆ Q and Q is closed in (2^{U∪U̇}, Cantor), then also \overline{h(S)} ⊆ Q. Therefore

min \overline{h(S)} = \overline{h(S)}

because Q is an antichain. By the two equations, h(S) = \overline{h(S)}; that is, h(S) is closed in (2^{U∪U̇}, Cantor). By Lemma 7.1(c), S is closed in (2^{U}, Cantor). □

But we also have the result of [36] connecting closed S ⊆ (2^{U}, Cantor) with stable model classes of finite proof support programs:

Theorem 7.3 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a closed subset of (2^{U}, Cantor). (ii) h(S) is the stable model class of a finite proof support program over U ∪ U̇.

Proof: By Lemma 7.1(c), condition (i) holds if and only if h(S) is a closed subset of (2^{U∪U̇}, Cantor). The equivalence with (ii) then follows by Theorem 4.1, since h(S) is an antichain. □

Theorems 7.2 and 7.3 show that h(S) is a minimal model class if and only if h(S) is the stable model class of some finite proof support program, since both properties correspond to the condition that S is closed. This is in contrast to our earlier results for sets not necessarily of the form h(S), where we gave an example of a set S which is a minimal model class but which is not the class of stable models of any finite proof support program (Example 4.2).

Similarly the following theorems about supported model classes show that under h more conditions coincide: Theorem 7.4 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a G_{δ} subset of (2^{U}, Cantor). (ii) h(S) is a supported model class over U ∪ U̇. Proof: (i) ⇒ (ii) By Lemma 7.1(c), h(S) is a G_{δ} subset of (2^{U∪U̇}, Cantor). To see that h(S) is a supported model class, we need to check that ∅ ∉ (\overline{h(S)} − h(S)). In fact, ∅ ∉ Q and \overline{h(S)} ⊆ Q because Q is closed, so ∅ ∉ \overline{h(S)}. So by Theorem 5.1, h(S) is a supported model class over U ∪ U̇. (ii) ⇒ (i) By Theorem 5.1, h(S) is a G_{δ} subset of (2^{U∪U̇}, Cantor). By Lemma 7.1(c), S then is a G_{δ} subset of (2^{U}, Cantor). □

Theorem 7.5 For S ⊆ 2^{U}, the following are equivalent:

(i) S is a closed subset of (2^{U}, Cantor). (ii) h(S) is the class of supported models of a finite completion program over U ∪ U̇.

Proof: By Lemma 7.1(c), condition (i) holds if and only if h(S) is a closed subset of (2^{U∪U̇}, Cantor). The equivalence with (ii) then follows by Theorem 6.1. □

Remark 7.2 These two theorems could be proved using Theorems 7.1 and 7.3 from this chapter. We preferred to prove them as translations of the characterization theorems obtained in Chapter 5.

From Theorems 7.1 and 7.4, then, h(S) is a stable model class if and only if h(S) is a supported model class, since both properties correspond to the condition that S is a G_{δ} set. Note that this is not due merely to h(S) being an antichain, since in Example 5.5 we presented a set which is an antichain and a supported model class but not a stable model class, but is rather the result of having h(S) contained in a minimal model class (namely Q). Also according to Theorems 7.3 and 7.5, h(S) is the stable model class of a program with the finite proof support property if and only if h(S) is the supported model class of a program with the finite completion property. In this case, however, such a correspondence actually holds for any antichain, not just for sets of the form h(S) (Corollary 6.1).

We illustrate these theorems with some examples, the first of which is by now familiar:

Example 7.1 Let S = {{u_{0}}, {u_{1}}, {u_{2}}, …}. S has previously provided an example of a G_{δ} set which is not a minimal model class because S ≠ min S̄ (Example 2.1), not a subset of a minimal model class because S ⊈ min S̄ and hence not a stable model class (Example 3.2), and not a supported model class because ∅ ∈ S̄ − S (Example 5.1). In contrast, however, S does have the property that h(S) is a stable model class over U ∪ U̇, since in Theorem 7.1 there is no further requirement on S besides that it be a G_{δ} set in (2^{U}, Cantor).

For this value of S, h(S) consists of the following subsets of U ∪ U̇ :

{u_{0}, u̇_{1}, u̇_{2}, …},
{u̇_{0}, u_{1}, u̇_{2}, …},
{u̇_{0}, u̇_{1}, u_{2}, …},
⋮

These sets are then the stable models of the following program P over U ∪ U̇ :

u_{0} ← ¬u̇_{0}
u̇_{1} ← ¬u̇_{0}
u̇_{2} ← ¬u̇_{0}
⋮
u̇_{0} ← ¬u̇_{1}
u_{1} ← ¬u̇_{1}
u̇_{2} ← ¬u̇_{1}
⋮
u̇_{0} ← ¬u̇_{2}
u̇_{1} ← ¬u̇_{2}
u_{2} ← ¬u̇_{2}
⋮
u̇_{i} ← ¬u̇_{j} for i ≠ j
u_{j} ← ¬u̇_{j}
⋮

Because S is not closed, h(S) can be neither a minimal model class nor the stable model class of a finite proof support program (by Theorems 7.2 and 7.3). Consider by way of contrast the set h(S̄). Since S̄ = S ∪ {∅}, h(S̄) consists of the elements of h(S) listed previously together with the new element

h(∅) = {u̇_{0}, u̇_{1}, u̇_{2}, …} = U̇.

Note that

h(S̄) = min \overline{h(S̄)} = \overline{h(S̄)} = min \overline{h(S)} = \overline{h(S)}.

Thus h(S̄) is a minimal class, and is in fact the minimal class of the program P above. Furthermore h(S̄) is the stable model class of the program P together with the additional clauses

u̇_{0} ← ¬u_{0}
u̇_{1} ← ¬u_{1}
u̇_{2} ← ¬u_{2}
⋮

which, by the procedure of Theorem 4.1, reduces to the finite proof support program

u_{0} ← ¬u̇_{0}
u̇_{0} ← ¬u_{0}
u_{1} ← ¬u̇_{1}
u̇_{1} ← ¬u_{1}
u̇_{1} ← ¬u̇_{0}
u_{2} ← ¬u̇_{2}
u̇_{2} ← ¬u_{2}
u̇_{2} ← ¬u̇_{0}
u̇_{2} ← ¬u̇_{1}
⋮
u_{j} ← ¬u̇_{j}
u̇_{j} ← ¬u_{j}
u̇_{j} ← ¬u̇_{i} for i < j
⋮

□

Example 7.2 Let R = ⟨R, +, ·, 0, 1⟩ be a commutative ring with unit, and let S be the set of its prime ideals. As mentioned at the beginning of this chapter, in [34] this example served to introduce the technique of representing h(S) as a stable model class. According to our Theorem 7.1, for h(S) to have such a representation it suffices that S be a G_{δ} subset of (2^{R}, Cantor). In fact, it turns out from the following expression that S is actually a closed subset of (2^{R}, Cantor) :

S = {I ⊆ R : 0 ∈ I ∧ 1 ∉ I
∧ ⋀_{x∈R}(x ∈ I → −x ∈ I)
∧ ⋀_{x,y∈R}(x ∈ I ∧ y ∈ I → x + y ∈ I)
∧ ⋀_{x,y∈R}(x ∈ I → x · y ∈ I)
∧ ⋀_{x,y∈R}(x · y ∈ I → (x ∈ I ∨ y ∈ I))}.

Thus h(S) is not only a stable model class over R ∪ Ṙ, but is in fact both a minimal model class over R ∪ Ṙ (by Theorem 7.2) and the stable model class of a program over R ∪ Ṙ with the finite proof support property (by Theorem 7.3). We note also that S itself can be represented as the supported model class of a program over R with the finite completion property (by Theorem 6.1). □

Example 7.3 Consider now a set S which not only is a G_{δ} subset of (2^{U}, Cantor) (like the set {{u_{0}}, {u_{1}}, {u_{2}}, …} already considered in Example 7.1), but has the stronger property that it is the supported model class of a program P over U. By following the procedures of Theorem 5.1 (to obtain an expression for S as a G_{δ} subset of (2^{U}, Cantor)), of Lemma 7.1 (to obtain an expression for h(S) as a G_{δ} subset of (2^{U∪U̇}, Cantor)), of Lemma 3.1 (to obtain an expression for h(S) as a G_{δ} subset of (2^{U∪U̇}, Scott^{−1})), and finally of Theorem 3.1, we can obtain a program over U ∪ U̇ for which h(S) is the class of stable models. Such a program P_{h} can be obtained from P more directly, however, as follows: For each clause

u ← A⃗, ¬B⃗

of P, include in P_{h} the corresponding clause

u ← ¬Ȧ, ¬B⃗.

Also include in P_{h} all clauses of the form

u̇ ← ¬u

for u ∈ U. We will show that h(S) = Stab(P_{h}).

We first review the fixpoint definitions for Stab(P_{h}) and for S as the set of supported models of P. From the definition of supported models, the elements of S are those sets S ⊆ U such that

S = T_{P} (S).

The stable models of P_{h} are those sets Z ⊆ (U ∪ U̇) such that

Z = T_{GL(Z,P_{h})} ↑ ω(∅).

Since P_{h} is prerequisite–free, the least fixpoint of T_{GL(Z,P_{h})} is obtained by one application of the operator; that is,

T_{GL(Z,P_{h})} ↑ ω(∅) = T_{GL(Z,P_{h})}(∅)

for any Z ⊆ (U ∪ U̇).

By straightforward arguments, for any S ⊆ U the following hold:

(a) T_{P} (S) = U ∩ T_{GL(h(S),P_{h})}(∅) and

(b) {u̇ : u ∉ S} = U̇ ∩ T_{GL(h(S),P_{h})}(∅).

Now we can show, as required, that h(S) = Stab(P_{h}) : (⊆) Let S ∈ S = Supp(P). To show that h(S) ∈ Stab(P_{h}), we will show that

h(S) = T_{GL(h(S),P_{h})}(∅).

Using (a) and (b), we have that

h(S) = S ∪ {u̇ : u ∉ S}
= T_{P} (S) ∪ {u̇ : u ∉ S}
= [U ∩ T_{GL(h(S),P_{h})}(∅) ∪ [U̇ ∩ T_{GL(h(S),P_{h})}(∅)]
= T_{GL(h(S),P_{h})}(∅),

as desired. (⊇) Let Z ∈ Stab(P_{h}), and let S = U ∩ Z. To show that Z ∈ h(S), we will show that S ∈ S and that Z = h(S).

For the latter, we have that

Z = [U ∩ Z] ∪ [U̇ ∩ Z]
= S ∪ [U̇ ∩ Z]
= S ∪ [U̇ ∩ T_{GL(Z,P_{h})}(∅)]
= S ∪ {u̇ : u ∈ U ∧ u ∉ Z}
= S ∪ {u̇ : u ∈ U ∧ u ∉ S}
= h(S).

Using this result and (a), we have that

S = U ∩ Z
= U ∩ T_{GL(Z,P_{h})}(∅)
= U ∩ T_{GL(h(S),P_{h})}(∅)
= T_{P} (S),

so S ∈ S = Supp(P).

We note that the simplicity of this method for obtaining a program to represent a stable model class depends on the simple form of the defining equations for Q as a minimal model class. From Remark 7.1, each defining equation is an expression of the form

u ↔ ¬u̇

(or of the form

u̇ ↔ ¬u,

which is equivalent). Because there is a single disjunct consisting of a single atom on the right–hand side, positive occurrences of atoms in P can simply be replaced one for one by negative occurrences of associated atoms. □

Example 7.4 Let F be any monotone finitizable operator on 2^{U}, and let S be the set of its fixed points. For each u ∈ U, let Ξ_{u} be the collection of finite A ⊆ U such that u ∈ F (A); then

S = {S ⊆ U : ⋀_{u∈U}[u ∈ S ↔ ⋁_{A∈Ξ_{U}} A⃗ ∈ S]}.

By Theorem 7.1, S has the property that h(S) is a stable model class over U ∪ U̇ because, as this expression shows, S is a G_{δ} subset of (2^{U}, Cantor).

Recall that S was previously considered in Example 5.7 of Chapter 5, where we showed that S is the supported model class of the Horn clause program P consisting of clauses

u ← A⃗

for u ∈ U and A ∈ Ξ_{u}. Thus S is a set of the sort considered in the preceding example (Example 7.3). As shown there, a representation for h(S) as a stable model class over U ∪ U̇ can be given then by the program P_{h} consisting of clauses

u ← ¬Ȧ

and

u̇ ← ¬u

for u ∈ U and A ∈ Ξ_{u}.

This representation is much simpler than one considered previously by the author in connection with an extended version of logic programming ([14]). □

Example 7.5 Let F be a continuous operator on (2^{U}, Cantor), and let S be the set of its fixed points. S then is a closed subset of (2^{U}, Cantor). As noted in Example 6.1 of Chapter 5, S is the set of supported models of some program over U with the finite completion property. By Theorems 7.2 and 7.3, S also has the property that h(S) is both a minimal model class over U ∪ U̇ and the stable model class of a finite proof support program over U ∪ U̇. □

BIBLIOGRAPHY 123

BIBLIOGRAPHY

[1] John W. Addison. Analogies in the Borel, Lusin, and Kleene hierarchies, I. Bulletin of the American Mathematical Society, 61:75, 1955. abstract.

[2] H. Andreka and I. Nemeti. The generalized completeness of Horn predicate logic as a programming language. Acta Cybernetica, 4:3–10, 1978.

[3] K. Apt, H. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–142, Los Altos, CA, 1987. Morgan Kaufmann.

[4] K. R. Apt and H. A. Blair. Arithmetic classification of perfect models of stratified programs. Fundamenta Informaticae, XIV:339–344, 1991.

[5] K. R. Apt and M. H. van Emden. Contributions to the theory of logic programming. Journal of the ACM, 29(3):841–862, 1982.

[6] A. Batarekh and V. S. Subrahmanian. Topological model set deformations in logic programming. Fundamenta Informaticae, XII:357–400, 1989.

[7] Aida Batarekh. Topological aspects of logic programming. PhD thesis, Syracuse University, 1989.

[8] N. Bidoit and Ch. Froixdevaux. Negation by default and unstratifiable logic programs. Theoretical Computer Science, 78:85–112, 1991.

[9] H. Blair, W. Marek, and J. Schlipf. The expressiveness of locally stratified programs. Technical Report SU-CIS-91-28, Syracuse University, 1991.

[10] K.L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and data bases, pages 293–322. Plenum Press, 1978.

[11] P. M. Dung and K. Kanchanasut. A fixpoint approach to declarative semantics of logic programs. In Proceedings of the North American Conference on Logic Programming, pages 604–625, Cambridge, MA., 1989. MIT Press.

[12] T. Eiter and G. Gottlob. Propositional circumscription and extended closed world reasoning are Π_{2}^{P} –complete. Theoretical Computer Science, 1991. to appear.

[13] Erik Ellentuck. A new proof that analytic sets are Ramsey. The Journal of Symbolic Logic, 39(1):163–165, March 1974.

[14] A. P. Ferry. Enriched nonmonotonic rule systems. Master’s thesis, University of Kentucky, 1991.

[15] M. C. Fitting. A Kripke/Kleene semantics for logic programs. Journal of Logic Programming, 2:295–312, 1985.

[16] M. C. Fitting. Bilattices and the semantics of logic programming. Journal of Logic Programming, 11:91–116, 1991.

[17] M. C. Fitting. The family of stable models. Journal of Logic Programming, 17:197–225, 1993.

[18] M. C. Fitting. Metric methods: three examples and a theorem. Journal of Logic Programming, 1993. to appear.

[19] M. Gelfond and V. Lifschitz. The stable semantics for logic programs. In Proceedings of the 5th International Symposium on Logic Programming, pages 1070– 1080, Cambridge, MA., 1988. MIT Press.

[20] M. Gelfond and V. Lifschitz. Logic programs with classical negation. In D. Warren and P. Szeredi, editors, Logic Programming: Proceedings of the 7th International Conference, pages 579–597, Cambridge, MA., 1990. MIT Press.

[21] M. Gelfond, H. Przymusinska, and T. Przymusinski. On the relationship between circumscription and negation as failure. Artificial Intelligence, 38:75–94, 1989.

[22] G. Gottlob. Complexity results for nonmonotonic logics. Technical Report CD-TR91/24, Institut für Informationssysteme, Technische Universität Wien, 1991.

[23] J. Jaffar, J.-L. Lassez, and J. W. Lloyd. Completeness of the negation as failure rule. In Proc. IJCAI-83, Karlsruhe, pages 500–506, 1983.

[24] M. Khamsi, V. Kreinovich, and D. Misane. A new method of proving the existence of answer sets for disjunctive logic programs: a metric fixed point theorem for multi–valued maps. Technical report, Department of Mathematics and Computer Science, University of Texas at El Paso, 1993.

[25] R. A. Kowalski. Predicate logic as a programming language. In Proc. IFIP 74, Stockholm, pages 569–574. North Holland, 1974.

[26] D. W. Kueker. Axiomatizing the minimal models. manuscript, 1985.

[27] K. Kunen. Negation in logic programming. Journal of Logic Programming, 4:289–308, 1987.

[28] K. Kuratowski. Topology, Volume I. Academic Press, New York and London, 1966.

[29] J.-L. Lassez and M. J. Maher. Closures and fairness in the semantics of programming logic. Theoretical Computer Science, 29:167–184, 1984.

[30] V. Lifschitz. Circumscriptive theories: A logic–based framework for knowledge representation. Journal of Philosophical Logic, 17:391–441, 1988.

[31] V. Lifschitz. On the declarative semantics of logic programs with negation. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 177–192, Los Altos, CA, 1988. Morgan Kaufmann.

[32] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984.

[33] W. Marek, A. Nerode, and J. C. Remmel. A class of logic programs with finite derivability property. manuscript.

[34] W. Marek, A. Nerode, and J. C. Remmel. A theory of nonmonotonic rule systems I. Annals of Mathematics and Artificial Intelligence, 1:241–273, 1990.

[35] W. Marek, A. Nerode, and J. C. Remmel. How complicated is the set of stable models of a recursive logic program? Annals of Pure and Applied Logic, 33, 1992.

[36] W. Marek, A. Nerode, and J. C. Remmel. A theory of nonmonotonic rule systems II. Annals of Mathematics and Artificial Intelligence, 5:229–264, 1992.

[37] W. Marek, A. Nerode, and J. C. Remmel. Normal nonmonotonic rule systems. Available from Department of Computer Science, University of Kentucky, 1993.

[38] W. Marek and V.S. Subrahmanian. The relationship between logic program semantics and non–monotonic reasoning. In Proceedings of the 6th International Conference on Logic Programming, 1989.

[39] W. Marek and M. Truszczyński. Modal logic for default reasoning. Annals of Mathematics and Artificial Intelligence, 1:275 – 302, 1990.

[40] W. Marek and M. Truszczyński. Autoepistemic logic. Journal of the ACM, 1991. To appear.

[41] W. Marek and M. Truszczyński. Nonmonotonic Logic: Context–Dependent Reasoning. Springer-Verlag, 1993.

[42] J. McCarthy. Circumscription — a form of non–monotonic reasoning. Artificial Intelligence, 13:27–39, 1980.

[43] J. McCarthy. Applications of circumscription to formalizing commonsense knowledge. Artificial Intelligence, 28:89–118, 1986.

[44] D. McDermott and J. Doyle. Nonmonotonic logic I. Artificial Intelligence, 13:41– 72, 1980.

[45] J. Minker. On indefinite databases and the closed world assumption. Lecture Notes in Computer Science, 138:292–308, 1982.

[46] R .C. Moore. Semantical considerations on non–monotonic logic. Artificial Intelligence, 25:75–94, 1985.

[47] J. R. Munkres. Topology: a First Course. Prentice–Hall, 1975. Englewood Cliffs, New Jersey.

[48] C. Papadimitriou and M. Yannakakis. Tie–breaking semantics and structural totality. In Proceedings of the 11th ACM Symposium on Principles of Database Systems, pages 16–22, 1992.

[49] T. Przymusinski. On the declarative and procedural semantics of stratified deductive databases. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193–216, Los Altos, CA, 1987. Morgan Kaufmann.

[50] T. Przymusinski. Extended stable semantics for normal and disjunctive programs. In D.H.D. Warren and P. Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 459–477, Cambridge, MA, 1990. MIT Press.

[51] T. Przymusinski. Stationary semantics for disjunctive logic programs and deductive databases. In S. Debray and M. Hermenegildo, editors, Logic Programming, Proceedings of the 1990 North American Conference, pages 40–59, Cambridge, MA, 1990. MIT Press.

[52] H. Rasiowa and R. Sikorski. A proof of the completeness theorem of gödel. Fund. Math., 37:193–200, 1950.

[53] R. Reiter. On closed world databases. In H. Gallaire and J. Minker, editors, Logic and data bases, pages 55–76. Plenum Press, 1978.

[54] R. Reiter. A logic for default reasoning. Artificial Intelligence, 13:81–132, 1980.

[55] R. Reiter. Nonmonotonic reasoning. Ann. Rev. Comput. Sci., 2:147–186, 1987.

[56] J. Barkley Rosser. Simplified Independence Proofs. Academic Press, 1969.

[57] Gerald E. Sacks. Saturated Model Theory. W. A. Benjamin, Inc., 1972.

[58] J. Schlipf. The expressive powers of the logic programming semantics. In Ninth ACM Symposium on Principles of Database Systems, 1990.

[59] G. F. Shvarts. Autoepistemic modal logics. In R. Parikh, editor, Proceedings of TARK 1990, pages 97–109, San Mateo, CA, 1990. Morgan Kaufmann.

[60] A. Tarski. A lattice–theoretical fixpoint theorem and its applications. Pacific J. Math., 5:285–309, 1955.

[61] M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

[62] A. Van Gelder, K. A. Ross, and J. S. Schlipf. Unfounded sets and well–founded semantics for general logic programs. In ACM Symposium on Principles of Database Systems, pages 221 – 230, 1988.

[63] A. Yahya and L. J. Henschen. Deduction in non–Horn databases. Journal of Automated Reasoning, 1(2):141–160, 1985.

[64] J. You and L. Yuan. Three–valued formalization of logic programming: is it needed? In Proceedings of the 9th ACM Symposium on Principles of Database Systems, pages 172–182, 1990.