Reasoning with infinite stable models

1 Introduction

There is a complexity gap between propositional and firstorder non-monotonic theories. Finite propositional theories are decidable (as in first-order logic), while the consequences of first-order theories are not recursively enumerable, in general. A computationally complete (Turing-equivalent) layer is missing between the two classes of theories. For this reason, most of the research on automated reasoning and proof-theory for nonmonotonic logics has been focussed on finite propositional theories or equivalent formalisms, such as function-free logic programs. In this way, the ability of reasoning about recursive data structures and infinite domains (such as lists, trees, XML/HTML documents, time, and so on) is completely lost. This is a strong limitation, both for standard tasks-such as reasoning about action and change when time is explicitly represented-and for emerging applications-such as using XML document bases as knowledge bases.

Of course, there may exist interesting, semi-decidable fragments of first-order nonmonotonic logics. For example, in some cases, the second-order circumscription formula can be expressed as a finite first-order formula. Similar examples are missing so far for Default Logic and Autoepistemic Logic.

Normal logic programs under the stable model semantics can be regarded as a fragment of both logics. In this paper we introduce a Turing-equivalent class of programs, called finitary programs, that opens the way to effective default and autoepistemic reasoning about infinite domains. The main theoretical features of finitary programs are the following:

• a0 Their domain may be infinite.
• a0 Nontheless both credulous and skeptical reasoning are semi-decidable. Ground queries are decidable.
• a0 A form of compactness holds.
• a0 Finitary programs are computationally complete, i.e. each Turing machine can be simulated by some finitary program.
• a0 Finitary programs are defined by two conditions on their dependency graph, that are minimal, in the sense that if any condition were dropped, then semi-decidability and compactness would not be guaranteed anymore.

The paper is organized as follows: after a few technical preliminaries (Section 2), we characterize the subprogram needed to reason about a given ground formula ✁ (Section 3). Then we introduce finitary programs (Section 4) and study their theoretical properties and expressiveness. In Section 5, the completeness proof for the skeptical resolution calculus introduced in [Bonatti, 1997] (originally formulated for function-free programs) is extended to all finitary programs and a generalization thereof (almost finitary programs). After a brief sketch of how existing credulous reasoners can be extended to finitary programs (Section 6), we conclude with a discussion of the results and related work. Some of the proofs are omitted due to space limitations.

2 Preliminaries

We assume the reader to be familiar with the classical theory of logic programming [Lloyd, 1984]. Normal logic programs (hereafter called simply "programs") are sets of rules of the form ✂ ✄ ✆ ✞ ✠ ☛ ☛ ☛ ✠ ✆ ✎ (✑ ✒ ✔ ) such that ✂ is a logical atom and each ✆ ✖ (✘ ✙ ✛ ✠ ☛ ☛ ☛ ✑ ) is a literal. As usual by "head" and "body" of such a rule we mean ✂ and ✆ ✞ ✠ ☛ ☛ ☛ ✠ ✆ ✎ , respectively. A program is positive if it contains no occurrences of ✥ . The ground instantiation of a program ✦ is denoted by ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ . The Gelfond-Lifschitz transformation ✦ ✵ of program ✦ w.r.t. an Herbrand interpretation ✷ (represented, as usual as a set of ground atoms) is obtained by removing from ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ all the rules containing a negative literal

✥ ✻ such that ✻ ✽ ✷ , and by removing from the remaining rules✿ all negative literals. An interpretation ❀ is a stable model of ✦ if ❀ is the least Herbrand model of ✦ ❁ . A formula ✁ is credulously (resp. skeptically) entailed by ✦ iff ✁ is satisfied by some (resp. each) stable model of ✦ .

The dependency graph of a program ✦ is a labelled directed graph whose vertices are the ground atoms of ✦ 's language. Moreover, i) there exists an edge from ✻ to ✂ iff there is a rule ❂ ✽ ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ with ✂ in the head and an occurrence of ✻ in the body; ii) such edge is labelled "negative" if ✻ occurs in the scope of ✥ , and "positive" otherwise. An atom ✂ depends positively (resp. negatively) on ✻ if there is a directed path from ✻ to ✂ in the dependency graph with an even (resp. odd) number of negative edges. A program is callconsistent if no atom depends negatively on itself. By oddcycle we mean a cycle in the dependency graph with an odd number of negative edges. Call-consistency coincides with the absence of odd-cycles. Every call-consistent program has at least one stable model [Dung, 1992].

In the context of normal logic programs, a splitting set for a program ✦ [Lifschitz and Turner, 1994] is a set of atoms ❆ containing all the atoms occurring in the body of any rule ❂ ✽ ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ whose head is in ❆ . The set of rules ❂ ✽ ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ whose head is in ❆ -called the "bottom" of ✦ w.r.t. ❆ -will be denoted by ❉ ❊ ✰ ✦ ✳ . By ❋ ❊ ✰ ✦ ✠ ✷ ✳ we denote the following partial evaluation of ✦ w.r.t. ✷ ❍ ❆ : remove from ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ each rule ✂ ✄ ✆ ✞ ✠ ☛ ☛ ☛ ✠ ✆ ✎ such that some ✆ ✖ containing an atom of ❆ is false in ✷ , and remove from the remaining rules all the ✆ ✖ containing a member of ❆ . The following is a specialization to normal programs of a result in [Lifschitz and Turner, 1994].

Theorem 2.1 (Splitting theorem) Let ❆ be a splitting set for a normal logic program ✦ . An interpretation ❀ is a stable model of ✦ iff ❀ ✙ ▲ ▼ ✷ , where

1. ✷ is a stable model of ❉ ❊ ✰ ✦ ✳ , and
2. ▲ is a stable model of ❋ ❊ ✰ ✦ a80 ❉ ❊ ✰ ✦ ✳ ✠ ✷ ✳ .

3 Relevant subprograms

This section contains the basic technical results needed to investigate decidability and undecidability issues. These results prove that a certain strict subset of ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ suffices to decide credulous and skeptical entailment. Intuitively, all is needed for inference are the rules affecting the behavior of odd-cycles (which may generate inconsistencies in the form of instability) and the definitions of the predicates on which the given goal ✁ depends.

Definition 3.1 [Relevant universe and subprogram] The relevant universe for a ground formula ✁ (w.r.t. program ✦ ), denoted by ❚ ✰ ✦ ✠ ✁ ✳ , is the set of all ground atoms ✂ such that the dependency graph of ✦ contains a path from ✂ to an atom occurring either in ✁ or in some odd-cycle of the graph.

The relevant subprogram for a ground formula ✁ (w.r.t program ✦ ), denoted by ❱ ✰ ✦ ✠ ✁ ✳ , is the set of all rules in ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ whose head belongs to ❚ ✰ ✦ ✠ ✁ ✳ .

Example 3.2 Consider the program ✦ consisting of the rules:

Note that for all rules ❂ ✽ ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ , if the head of ❂ belongs to ❚ ✰ ✦ ✠ ✁ ✳ then also all the other atoms in ❂ belong to ❚ ✰ ✦ ✠ ✁ ✳ . The next proposition follows easily.

Proposition 3.3 ❚ ✰ ✦ ✠ ✁ ✳ is a splitting set for ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ , and ❱ ✰ ✦ ✠ ✁ ✳ coincides with ❉ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ ✳ .

Now the basic technical results can be proved.

Lemma 3.4 For all ground formulae ✁ , ❱ ✰ ✦ ✠ ✁ ✳ has a stable model ❀ a115 iff ✦ has a stable model ❀ such that ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ❀ a115 .

Proof. ("If" part) Suppose ❀ is a stable model of ✦ . By Proposition 3.3, ❚ ✰ ✦ ✠ ✁ ✳ is a splitting set for ✦ and ❱ ✰ ✦ ✠ ✁ ✳ ✙ ❉ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ ✳ . Then, by the splitting theorem [Lifschitz and Turner, 1994], there exist a stable model ✷ of ❱ ✰ ✦ ✠ ✁ ✳ , and a stable model ▲ of ❋ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ a80 ❱ ✰ ✦ ✠ ✁ ✳ ✠ ✷ ✳ , such that ❀ ✙ ✷ ▼ ▲ . By definition, no atom in ❚ ✰ ✦ ✠ ✁ ✳ occurs in ❋ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ a80 ❱ ✰ ✦ ✠ ✁ ✳ ✠ ✷ ✳ , therefore ▲ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ⑥ . It follows that ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ✷ , and hence ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ is a stable model of ❱ ✰ ✦ ✠ ✁ ✳ .

("Only if" part) Suppose ❱ ✰ ✦ ✠ ✁ ✳ has a stable model ❀ a115 . By definition, all the atoms occurring in an oddcycle belong to ❚ ✰ ✦ ✠ ✁ ✳ . Consequently, the dependency graph of ❋ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ a80 ❱ ✰ ✦ ✠ ✁ ✳ ✠ ✷ ✳ contains no odd-cycles, i.e. ❋ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ a80 ❱ ✰ ✦ ✠ ✁ ✳ ✠ ✷ ✳ is call-consistent. Then, by a wellknown result in [Dung, 1992], ❋ ❧ ♠ ♦ a113 a115 a116 ✰ ✦ a80 ❱ ✰ ✦ ✠ ✁ ✳ ✠ ✷ ✳ has a stable model ▲ . Let ❀ ✙ ▲ ▼ ❀ a115 . By the splitting theorem, the interpretation ❀ is a stable model of ✦ . Moreover, since ▲ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ⑥ (cf. point 1), ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ❀ a115 .

Theorem 3.5 For all ground formulae ✁ ,

1. ✦ credulously entails ✁ iff ❱ ✰ ✦ ✠ ✁ ✳ does.
2. ✦ skeptically entails ✁ iff ❱ ✰ ✦ ✠ ✁ ✳ does.

Proof. if ✦ credulously entails ✁ , then there exists a stable model ❀ of ✦ such that ❀ ❽ ✙ ✁ . By Lemma 3.4, ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ is a stable model of ❱ ✰ ✦ ✠ ✁ ✳ . Moreover, since by definition ❚ ✰ ✦ ✠ ✁ ✳ contains all the atoms occurring in ✁ , ✁ must have the same truth value in ❀ and ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ , and hence ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ❽ ✙ ✁ . As a consequence ❱ ✰ ✦ ✠ ✁ ✳ credulously entails ✁ .

Conversely, suppose that ❱ ✰ ✦ ✠ ✁ ✳ credulously entails ✁ . Then there exists a stable model ❀ a115 of ❱ ✰ ✦ ✠ ✁ ✳ such that ❀ a115 ❽ ✙ ✁ . By Lemma 3.4, ✦ has a stable model ❀ such that ❀ ❍ ❚ ✰ ✦ ✠ ✁ ✳ ✙ ❀ a115 . Then the models ❀ and ❀ a115 must agree on the valuation of ✁ (cf. the "only if" part of the proof) and hence ❀ ❽ ✙ ✁ , which means that ✦ credulously entails ✁ . This completes the proof of 1).

To prove 2), we demonstrate the equivalent statement:

✦ does not skeptically entail ✁ iff ❱ ✰ ✦ ✠ ✁ ✳ does not skeptically entail ✁ .

This statement is equivalent to: ✦ credulously entails ✥ ✁ iff ❱ ✰ ✦ ✠ ✁ ✳ credulously entails ✥ ✁ , that follows immediately from 1).

4 Finitary programs

Now we introduce a class of programs whose consequences are recursively enumerable, although their domain may be infinite.

Definition 4.1 [Finitary programs] We say a program ✦ is finitary if the following conditions hold:

1. For each node ✂ of the dependency graph of ✦ , the set of all nodes ✻ such that ✂ depends (either positively or negatively) on ✻ is finite.
2. Only a finite number of nodes of the dependency graph of ✦ occurs in an odd-cycle.

For example, most classical programs on recursive data structures such as lists and trees (e.g. predicates member, append, reverse) satisfy the first condition. In these programs, the terms occurring in the body of a rule occur also in the head, typically as strict subterms of the head's arguments. This property clearly entails Condition 1.

The second condition is satisfied by most of the programs used for embedding NP-hard problems into logic programs [Cholewi´nski et al., 1995; Eiter and Gottlob, 1993; Gottlob, 1992]. Such programs can be (re)formulated by using a single odd cycle involving one atom ❳ and defined by simple rules such as ❳ ✄ ✥ ❳ and ❳ ✄ ❨ ✠ ✥ ❳ (if ❳ does not occur elsewhere, then ❨ can be used as the logical constant false in the rest of the program).

An example of finitary program without odd-cycles is illustrated in Figure 1. It credulously entails a ground goal ➂ ✰ ➃ ✳ iff ➃ encodes a satisfiable formula. By adding rule ➄ ✄ ✥ ➂ ✰ ➆ ✳ ✠ ✥ ➄ we obtain another finitary program with one odd-cycle, such that ➂ ✰ ➃ ✳ is skeptically entailed iff the formula encoded by ➃ is a logical consequence of the one encoded by ❨ .

The following proposition follows straightforwardly from the definitions of ❚ ✰ ✦ ✠ ➇ ✳ , ❱ ✰ ✦ ✠ ➇ ✳ and finitary programs. It will be needed to prove computability results.

Proposition 4.2 If ✦ is finitary then, for all ground goals ➇ , ❚ ✰ ✦ ✠ ➇ ✳ and ❱ ✰ ✦ ✠ ➇ ✳ are finite.

4.1 Compactness

In classical first-order logic, an infinite set of formulae is inconsistent iff it contains an inconsistent finite subset. A similar property-that in general does not apply to nonmonotonic logics-is enjoyed by finitary programs, too.

Definition 4.3 An unstable kernel for a program ✦ is a subset ➈ of ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ with the following properties:

1. ➈ is downward closed, that is, for each atom ✂ occurring in ➈ , ➈ contains all the rules ❂ ✽ ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ whose head is ✂ .
2. ➈ has no stable models.

Theorem 4.4 (Compactness) A finitary program ✦ has no stable models iff it has a finite unstable kernel.

Proof. Let ➇ be any ground atom in the language of ✦ . From Lemma 3.4, it follows that ✦ has no stablemodels iff ❱ ✰ ✦ ✠ ➇ ✳ has no stable models. Clearly, ❱ ✰ ✦ ✠ ➇ ✳ is downward closed by definition. Moreover, by Proposition 4.2, ❱ ✰ ✦ ✠ ➇ ✳ is finite. Therefore ✦ has no stable models iff ❱ ✰ ✦ ✠ ➇ ✳ is a finite unstable kernel of ✦ .

4.2 Decidability and semi-decidability of inference

Hereafter we focus on the complexity of inference within the class of finitary programs. This subsection deals with upper bounds. We start with the proof that, for all ground goals, both credulous and skeptical inference are decidable.

Theorem 4.5 For all finitary programs ✦ and ground goals ➇ , both the problem of deciding whether ➇ is a credulous consequence of ✦ and the problem of deciding whether ➇ is a skeptical consequence of ✦ are decidable.

Proof. By Theorem 3.5, ➇ is a credulous (resp. skeptical) consequence of ✦ iff ➇ is a credulous (resp. skeptical) consequence of ❱ ✰ ✦ ✠ ➇ ✳ . Moreover, by Proposition 4.2, ❱ ✰ ✦ ✠ ➇ ✳ is finite, so the set of its stable models can be computed in finite time. It follows that the inference problems for ✦ and ➇ are both decidable.

It follows easily that existentially quantified goals are semidecidable.

Theorem 4.6 For all finitary programs ✦ and all goals ➇ , both the problem of deciding whether ➉ ➇ is a credulous consequence of ✦ and the problem of deciding whether ➉ ➇ is a skeptical consequence of ✦ are semi-decidable.

Proof. The formula ➉ ➇ is credulously (res. skeptically) entailed by ✦ iff there exists a grounding substitution ➋ such that ➇ ➋ is credulously (res. skeptically) entailed by ✦ . The latter problem is decidable (by Theorem 4.5), and all grounding ➋ for ➇ can be recursively enumerated, so existential entailment can be reduced to a potentially infinite recursive sequence of decidable tests, that terminates if and only if some ➇ ➋ is entailed.

We shall see in the following section that this is a strict bound, i.e. existential entailment can be undecidable (cf. Corollary 4.11).

4.3 Minimality and expressiveness

Next we focus on lower bounds to the complexity of inference for the class of finitary programs and relaxations thereof. The next two results show that both of the conditions in Definition 4.1 are necessary for semi-decidability, i.e. Definition 4.1 is in some sense minimal.

Proposition 4.7 Credulous and skeptical inference are not semi-decidable for the class of all programs satisfying Condition 2 of Definition 4.1.

Proof. Note that locally stratified programs trivially satisfy Condition 2 of Definition 4.1 while some of them may violate Condition 1. For locally stratified programs, credulous and skeptical inference coincide with the well-founded semantics [Gelfond and Lifschitz, 1988] and are not semi-decidable [Schlipf, 1990], so the proposition immediately follows.

➂ ✰ ➍ ➎ ➏ ✰ ➐ ✠ ➑ ✳ ✳ ✄ ➂ ✰ ➐ ✳ ✠ ➂ ✰ ➑ ✳ ➂ ✰ ➒ ➓ ✰ ➐ ✠ ➑ ✳ ✳ ✄ ➂ ✰ ➐ ✳ ➂ ✰ ➒ ➓ ✰ ➐ ✠ ➑ ✳ ✳ ✄ ➂ ✰ ➑ ✳ ➂ ✰ ➎ ➒ → ✰ ➐ ✳ ✳ ✄ ✥ ➂ ✰ ➐ ✳ ➂ ✰ ➣ ✳ ✄ ↔ ➙ ↔ ➜ ➙ ➓ ✰ ➣ ✠ ➝ ➞ ✠ ➟ ✠ ➓ ✠ ➂ ➠ ✳ ✠ ✥ ➎ ➂ ✰ ➣ ✳ ➎ ➂ ✰ ➣ ✳ ✄ ↔ ➙ ↔ ➜ ➙ ➓ ✰ ➣ ✠ ➝ ➞ ✠ ➟ ✠ ➓ ✠ ➂ ➠ ✳ ✠ ✥ ➂ ✰ ➣ ✳ ↔ ➙ ↔ ➜ ➙ ➓ ✰ ➣ ✠ ➝ ➣ ❽ ➡ ➠ ✳ ↔ ➙ ↔ ➜ ➙ ➓ ✰ ➣ ✠ ➝ ➢ ❽ ➡ ➠ ✳ ✄ ↔ ➙ ↔ ➜ ➙ ➓ ✰ ➣ ✠ ➡ ✳

The other lower-bound results are based on positive programs that decide whether a given Turing machine terminates using a fixed portion of its tape.

Let ➤ be an arbitrary Turing machine; let ➥ and ➦ be ➤ 's set of states and vocabulary, respectively. Recall that the actions of ➤ are defined by 5-tuples ➧ ❵ ✠ ➨ ✠ ➨ ➩ ✠ ❵ ➩ ✠ ➫ ➭ , where ❵ and ➨ are the current state and symbol, respectively, ➨ ➩ is the symbol to be overwritten on ➨ , ❵ ➩ is the next state, and ➫ specifies ➤ 's head movement.

Consider the positive program ✦ ➲ in Figure 2. The reader may easily verify that → ✰ ➳ ✠ ➡ ✠ ➸ ✠ ➺ ✳ is entailed by ✦ ➲ iff there exists a finite computation of ➤ , starting from a configuration with state ❵ and tape described by ➡ ✠ ➸ ✠ ➺ , and using only the finite portion of tape corresponding to ➡ ✠ ➸ ✠ ➺ . Here ➡ is a list representing a finite portion of the tape on the left of ➤ 's head, in reverse order; ➸ is the current symbol; ➺ is a (non reversed) finite portion of the tape on the right of ➤ 's head.

Program ✦ ➲ satisfies Condition 1 of Definition 4.1. To prove this, note that the recursive calls to predicate → preserve the length ➻ of the portion of tape encoded in the head. Therefore, for each ground atom → ✰ ❵ ✠ ➼ ✠ ➨ ✠ ❂ ✳ , the number of atoms → ✰ ❵ ➩ ✠ ➼ ➩ ✠ ➨ ➩ ✠ ❂ ➩ ✳ connected to → ✰ ❵ ✠ ➼ ✠ ➨ ✠ ❂ ✳ by a directed path in the dependency graph is bounded by ❽ ➥ ❽ ➾ ❽ ➦ ❽ ➪ .

The next two results are based on ✦ ➲ and prove that if Condition 2 in Definition 4.1 were dropped, then inference would not be semi-decidable anymore. More precisely, the theorems say that some inferences would be as complex as deciding the termination of an arbitrary Turing machine.

Theorem 4.8 For each Turing machine ➤ with initial state ❵ and tape ➶ with non-blank portion ➧ ➨ ➹ ✠ ➨ ✞ ✠ ☛ ☛ ☛ ✠ ➨ ✎ ➭ , a program ✦ ✞ ➲ and a goal ➇ can be recursively constructed, such that ✦ ✞ ➲ satisfies only Condition 1 in Definition 4.1, and ✦ ✞ ➲ skeptically entails ➇ iff ➤ terminates.

Proof. (Sketch) Let ✦ ✞ ➲ consist of the program defined in Figure 2 plus the rules

➘ ✰ ➡ ✠ ➺ ✳ ✄ ➜ ➷ ➍ ➎ ➬ ➷ ➮ ➂ → ✰ ➡ ✳ ✠ ➜ ➷ ➍ ➎ ➬ ➷ ➮ ➂ → ✰ ➺ ✳ ✠ → ✰ ➳ ✠ ➡ ✠ ✃ ❐ ✠ ➝ ✃ ❒ ✠ ☛ ☛ ☛ ✠ ✃ ❮ ❽ ➺ ➠ ✳ ✠ ✥ ➘ ✰ ➡ ✠ ➺ ✳ ☛ ➜ ➷ ➍ ➎ ➬ ➷ ➮ ➂ → ✰ ➝ ➠ ✳ ☛ ➜ ➷ ➍ ➎ ➬ ➷ ➮ ➂ → ✰ ➝ a207 ❽ ➡ ➠ ✳ ✄ ➜ ➷ ➍ ➎ ➬ ➷ ➮ ➂ → ✰ ➡ ✳ ☛

where ❉ represents the blank symbol. ✦ ✞ ➲ satisfies Condition 1 of Definition 4.1 (cf. the argument for ✦ ➲ ). Condition 2 of Definition 4.1 is violated, as there exist infinitely many odd-cycles, one for each ground atom ➘ ✰ a208 ✠ a209 ✳ . Clearly, for any grounding substitution ➋ , the goal

a210 a211 a213 a214 a215 a216 a213 a217 a218 a219 a210 a220 a221 a222 a211 a213 a214 a215 a216 a213 a217 a218 a219 a210 a223 a221 a222 a219 a210 a224 a222 a220 a222 a226 a227 a222 a228 a226 a230 a222 a231 a231 a231 a222 a226 a232 a233 a223 a235 a221 a221 a236

can be derived from the subprogram ✦ ➲ and the clauses for blank list iff ➤ terminates using the portion of ➶ represented by ➡ ➋ ✠ ✃ ❐ ✠ ➝ ✃ ❒ ✠ ☛ ☛ ☛ ✠ ✃ ❮ ❽ ➺ ➋ ➠ . At the same time, ✦ ✞ ➲ has a stable model iff the above goal cannot be derived from ✦ ➲ , because of the odd-cycle containing ➘ ✰ ➺ ✠ ➡ ✳ ➋ . It follows that for all ➇ consisting of a propositional symbol not occurring in ✦ ✞ ➲ , ✦ ✞ ➲ skeptically entails ➇ iff ➤ terminates.

Theorem 4.9 For each Turing machine ➤ with initial state ❵ and tape ➶ with non-blank portion ➧ ➨ ➹ ✠ ➨ ✞ ✠ ☛ ☛ ☛ ✠ ➨ ✎ ➭ , a program ✦ a237 ➲ and a goal ➇ can be recursively constructed, such that ✦ a237 ➲ satisfies only Condition 1 in Definition 4.1, and ✦ a237 ➲ credulously entails ➇ iff ➤ terminates.

Proof. Let ✦ a237 ➲ ✙ ✦ ✞ ➲ ▼ ❣ ❳ ❤ , where ❳ is a new propositional symbol not occurring in ✦ ✞ ➲ , and let ➇ ✙ ❳ . Clearly ✦ a237 ➲ credulously entails ➇ iff ✦ a237 ➲ has a stable model. Since ✦ a237 ➲ has a stable model iff ➤ terminates (cf. the previous proof), the theorem immediately follows.

The next result is based on amodification of ✦ ➲ that keeps track of the result of the computation. The modified program ✦ a238 ➲ has one extra argument to return the final state of the tape. The theorem proves that the class of finitary programs is computationally complete by showing how any Turing machine can be simulated by a suitable finitary program.

Theorem 4.10 For each Turing machine ➤ with initial state ❵ and tape ➶ with non-blank portion ➧ ➨ ➹ ✠ ➨ ✞ ✠ ☛ ☛ ☛ ✠ ➨ ✎ ➭ , a (positive) finitary program ✦ a238 ➲ and a goal ➞ ✰ ➡ ✠ ➺ ✠ ➐ ✳ can be recursively constructed, in such a way that for all grounding substitutions ➋ , ✦ a238 ➲ ❽ ✙ ➞ ✰ ➡ ✠ ➺ ✠ ➐ ✳ ➋ iff ➤ terminates and ➐ ➋ encodes the final tape of the computation.

Corollary 4.11 The problems of deciding whether a finitary program ✦ credulously/skeptically entails an existentially quantified goal ➉ ➇ are not decidable.

5 Resolution calculus

Here the results of the previous sections are applied to the resolution calculus for skeptical stable model semantics introduced in [Bonatti, 1997]. In the original paper, the resolution calculus was proved complete w.r.t. function-free programs (soundness holds for all programs). In this section, we extend the completeness result to all finitary programs.

Theorem 5.1 Let ✦ be a finitary program, and let ✰ a239 a240 a242 a239 ➇ ✳ a243 be a ground skeptical consequence of ✦ , where a240 and ➇ are sequences of literals. Then the skeptical goal ✰ ➇ ❽ a240 ✳ has a successful skeptical derivation from ✦ with answer substitution ➋ more general than a243 .

→ ✰ ➳ ✠ ➡ ✠ ✃ ✠ ➝ ➸ ❽ ➺ ➠ ✳ ✄ → ✰ ➳ ➩ ✠ ➝ ✃ ➩ ❽ ➡ ➠ ✠ ➸ ✠ ➺ ✳ for all 5-tuples ➧ ❵ ✠ ➨ ✠ ➨ ➩ ✠ ❵ ➩ ✠ ➓ ➮ a246 a247 → ➭ → ✰ ➳ ✠ ➝ ➸ ❽ ➡ ➠ ✠ ✃ ✠ ➺ ✳ ✄ → ✰ ➳ ➩ ✠ ➡ ✠ ➸ ✠ ➝ ✃ ➩ ❽ ➺ ➠ ✳ for all 5-tuples ➧ ❵ ✠ ➨ ✠ ➨ ➩ ✠ ❵ ➩ ✠ ➷ ➙ a248 → ➭ → ✰ ➳ ✠ ➡ ✠ ✃ ✠ ➺ ✳ if there exists no tuple for ❵ and ➨ .

Proof. Let ✁ ✙ ✰ a239 a240 a242 a239 ➇ ✳ a243 . Since ✁ is a ground skeptical consequence of ✦ , then ✁ is also a skeptical consequence of a253 ✰ ✦ ✠ ✁ ✳ (by Theorem 3.5). Moreover, a253 ✰ ✦ ✠ ✁ ✳ is finite (by Proposition 4.2). Then, by the original completeness result [Bonatti, 1997], ✰ ➇ ❽ a240 ✳ a243 has a ground skeptical derivation from a253 ✰ ✦ ✠ ✁ ✳ a255 ✧ ★ ✩ ✪ ✬ ✮ ✰ ✦ ✳ . By standard lifting techniques (cf. [Lloyd, 1984]), a corresponding skeptical derivation of ✰ ➇ ❽ a240 ✳ from ✦ with answer substitution ➋ more general than a243 can easily be obtained.

Example 5.2 Consider again the program ✦ of Example 3.2. This finitary program has no stable model, because of its third rule. Figure 3 shows a successful skeptical derivation for the skeptical conclusion ❳ ✰ ❩ ✳ , with empty answer substitution (whichmeans that ✁ ❩ ☛ ❳ ✰ ❩ ✳ is a skeptical consequence of ✦ ). The Restricted Split of type II introduces two subgoals, each with a new hypothesis ( ❛ ✰ ❜ ✳ and ✥ ❛ ✰ ❜ ✳ , respectively), obtained from an atom occurring in some odd-cycle. The Contradiction rule replaces the left-hand side of a goal with the negation of some hypothesis. Intuitively, the goal is proved by showing that the hypotheses on the right hand side cannot be satisfied. The Failure rule rewrites a goal with one of its counter-supports. In this example the counter-support of ❛ ✰ ❜ ✳ is ❛ ✰ ❜ ✳ itself (obtained by negating the unique support ❣ ✥ ❛ ✰ ❜ ✳ ❤ of ❛ ✰ ❜ ✳ ). Resolution can be performed either with a program rule or with one of the hypotheses (treated as facts). Finally, the Success rule removes goals where there is nothing left to prove. As usual, the empty goal sequence is denoted by ✂ .

With the help of the resolution calculus it can be shown that a class of normal programs larger than finitary programs is Turing equivalent. The extended class-called almost finitary-admits the kind of rules typically used to generate inconsistencies, without the restrictions of Definition 4.1.

Definition 5.3 [Almost finitary programs] A normal program ✦ is almost finitary iff it can be partitioned into two (disjoint) subsets, ✦ ✞ and ✦ a237 , such that ✦ ✞ is finitary, and ✦ a237 consists of rules of the form ✂ ✄ ✻ ✞ ✠ ☛ ☛ ☛ ✠ ✻ ✎ ✠ ✥ ✂ ☛

Note that there is no restriction on ✦ a237 's rule variables. Given a ground instance ✰ ✂ ✄ ✻ ✞ ✠ ☛ ☛ ☛ ✠ ✻ ✎ ✠ ✥ ✂ ✳ ➋ of a rule in ✦ a237 , ✂ ➋ may depend on infinitely many ground atoms ✻ (i.e., Condition 1 of Definition 4.1 can be violated).

Theorem 5.4 The skeptical resolution calculus is complete (in the sense of Theorem 5.1) for all almost finitary programs.

Corollary 5.5 The set of skeptical consequences of the form ➉ ✰ a239 a240 a242 a239 ➇ ✳ , where a240 and ➇ are sequences of literals, is semi-decidable for almost finitary programs.

Remark 5.6 For almost finitary programs, ground credulous inference is not semi-decidable. This means that skeptical inference from almost finitary programs cannot be implemented through credulous inference. Only direct approaches such as the resolution calculus are possible.

6 Credulous automated reasoners

For function-free programs, there exist powerful automated reasoners based upon stable model generation, such as SMODELS [Niemel¨ a and Simons, 1997] and DLV [Eiter et al., 1997]. Internally, these engines operate on ground programs; for this reason they embody smart program instantiation routines. Such routines are applied before any other form of reasoning. It seems not difficult to extend the instantiation routines to deal with all finitary programs, so that given a ground goal ➇ 1 , only the relevant (ground and finite) subprogram a253 ✰ ✦ ✠ ➇ ✳ (or an equivalent subset thereof) 2 is generated. The rest of the engine needs no modification. By Theorem 3.5, soundness and completeness are preserved. In this way, our results can be used to extend the applicability range of this class of automated reasoners, with no modification to the core of their reasoning mechanisms. 3

7 Summary and related work

For the first time, semi-decidable fragments of the stable model semantics have been explored in depth, and related to the number of atoms involved in odd-cycles. The main contributions of this paper can be summarized by recalling that finitary programs (Def. 4.1) are computationally complete (Theorem 4.10), can deal with function symbols, and enjoy a compactness result (Theorem 4.4) that guarantees semi-decidability of inference (Theorem 4.6). Finitary programs are characterized by two conditions on their dependency graph that are minimal, in the sense that if any of them were dropped, then inference would not always be semidecidable (Theorems 4.7, 4.8 and 4.9). We proved that the skeptical resolution calculus is complete for finitary and almost finitary programs (Theorems 5.1 and 5.4), and sketched how other engines for nonmonotonic reasoning can be extended to deal with finitary programs (Section 6). We are currently extending our results to larger classes of programs, and to partial stable models. 4

The work on finitary programs contributes to providing nonmonotonic logics with classical proof- and model-

1 These engines can only deal with ground queries

2 The smart instantiation routines remove some non-applicable rule instances.

3 As noted by an anonymous referee, the same idea can be applied to function-free programs, in order to reduce the cost of program instantiation.

4 The latter idea and evidence to its feasibility have been suggested by an anonymous referee.

theoretic tools and results. Work in a similar direction comprises some pretty standard axiomatizations based on Hilbertstyle systems [Levesque, 1990] 5 and sequent calculi [Olivetti, 1992; Bonatti and Olivetti, 1997]. These axiomatizations for Default and Autoepistemic logic should be extended to firstorder theories, perhaps adapting the techniques introduced in this paper. An infinitary proof-theory can be found in [Milnikel, 1999]. In [Rosati, 1999], issues related to decidable nomonotonic reasoning in MKNF are investigated. In [Cenzer et al., 1999], sufficient conditions for the existence of recursively enumerable stable models are identified. They do not ensure that all stable models are r.e., so skeptical and credulous reasoning are not semi-decidable.

Acknowledgments

The author is grateful to the anonymous referees for their deep and careful reviews, and for their precious suggestions.