An Abductive Framework for General Logic Programs and other Nonmonotonic Systems

1 Background and Motivation

In this paper we investigate the relationship between abduction, logic programming, and other nonmonotonic formalisms . 1 This investigation is interesting for several reasons. Firstly, abduction as a form of nonmonotonic reasoning has gained a lot of interest in recent years, and exploring the relationship between different forms of nonmonotonic reasoning is of interest in itself. Secondly, as we will show in this paper, it is possible to define a simple and elegant extension of Gelfond and Lifschitz's stable model semantics [9] based on abduction. This new abductive semantics has the following properties:

• The semantics is equivalent to stable model seman­ tics for programs which possess at least one stable model.
• A program P has a defined meaning unless P con­ sidered as a set of inference rules is inconsistent. In particular, normal logic programs without stable models are not meaningless.
• The abductive semantics imitates the well-founded model in not assigning a truthvalue to propositions

1 For simplicity we consider only finite propositional logic programs, that is programs with finite Herbrand base, in this preliminary report . All definitions also apply to the general case.

Kurt Konolige

SRI International 333 Ravenswood Ave Menlo Park, CA 94025

whose assertion is self-contradictory.

• The semantics is, without further modification, ap­ plicable to logic programs that contain classical negation and so-called epistemic disjunction [8] .
• The semantics can be applied to other consistency­ based nonmonotonic formalisms, including default logic and autoepistemic logic.

We consider all of these properties as highly desirable. Stable model semantics is currently the most widely ac­ cepted semantics for logic programs which have a stable model. We therefore believe that an extension of stable model semantics should preserve the meaning of those programs. On the other hand , many authors consider it a severe weakness of stable model semantics that not all normal logic programs have stable models; by con­ trast, the well-founded semantics always exists. Our se­ mantics overcomes this weakness , in the same manner as the well-founded semantics, by allowing a truthvalue gap for self-contradictory propositions. At the same time, it does not suffer from the weakness of well-founded se­ mantics, the "floating conclusions" problem. 2 Finally, there has been a great amount of recent work trying to extend the expressiveness of normal logic programs by, among other things, adding classical negation and "epis­ temic" disjunction. It turns out to be a non-trivial task to adapt existing semantics to more general logic pro­ grams. It is therefore clearly an advantage if a simple semantics for normal programs can directly be applied to theses generalizations.

Abduction, informally, is the generation of explana­ tions for a given fact p . Given a background theory T and a set of possible hypotheses or abducibles H, an ex­ planation for p is a subset H' of H such that H' U T is consistent and pis provable from H'UT. Usually, there is a further acceptability criterion that distinguishes pre­ ferred explanations. In our approach we will consider negated atoms as hypotheses, a logic program (viewed as a set of inference rules) as the background theory. Moreover, we introduce a simple criterion defimug the acceptable explanations or, in our terminology, exten­ sion bases. We consider a proposition q derivable " . ..:>m a logic program if it is derivable from all of its extension bases.

2 Floating conclusions are conclusions that are intuitively justified by case analysis yet underivable in well-founded se­ mantics. The standard example is a - -b; b - ~a ; c - a; c - b. Well-founded semantics does not conclude c.

Using abductive frameworks to define a semantics for logic programs is not a new idea. Eshghi and Kowalski [4] were the first to investigate logic programs, in par­ ticular negation as failure, in terms of abduction. More recently, Kakas and Mancarella [13] and Dung [3] have continued this line of research. We will in the rest of this section review these earlier approaches and discuss why we do not consider them entirely satisfactory.

Eshghi and Kowalski show that negation as failure in normal logic programs can be viewed as a special case of abduction . Their analysis is based on abductive frame­ works of the form (T, I, A} where T is a set of definite clauses , I a set of integrity constraints, and A a set of ab­ ducible predicates. Atomic ground formulas built from the symbols in A are called abducibles. A set of ab­ ducibles b. is an abductive solution for q iff T U b. 1- q and TUb. satisfies I.

Since the authors restrict T to definite clauses and the set of abducibles to atomic formulas they have to elimi­ nate negation signs from logic programs to handle nega­ tion as failure in their framework . Given a normal logic program P they introduce for each predicate symbol pin P a new predicate symbol p*. P is then transformed to a program P* by replacing each negative occurrence of a predicate symbol p in the body of a rule by a positive occurrence of p* . Additionally, integrity constraints of the form

are used to make sure that not both p*(t) and p(t) can be true at the same time. Additionally, there are metalevel constraints of the form

Such a disjunctive integrity constraint is satisfied iff p(t) or p*(t) is provable from TUb. . Eshghi an<;! Kowalski show that for every stable model of a program P there is a corresponding abductive solution for the transformed program P* and vice versa. This one-to-one correspon­ dence to stable models shows that the new abductive semantics does not give meaning to programs without stable models and thus inherits the weakness of stable model semantics: the existence for abductive solutions for normal programs is not guaranteed. Consider the program P2

and its transform

The introduction of the metalevel constraint leads to the non-existence of an abductive solution.

Kakas and Mancarella use a similar abductive frame­ work as Eshghi and Kowalski to define a generalization of stable models. In their paper an abductive framework is a triple (P, A, I} where P is a normal logic program, A a set of abducible predicates, and I a set of integrity constraints. Contrary to Eshghi/Kowalski they directly use the notion of a stable model in their definitions. A pre-general stable model of (P, A, I} is a stable model of P U {p- I p E b.}, where b. is an arbitrary set of ab­ ducibles. A general stable model is a pre-general stable model that implies all integrity constraints in I .

The authors then show how negation as failure can be treated through abduction. The approach is similar to Eshghi/Kowalski's but somewhat simpler: the metalevel constraints involving the Demo predicate are replaced by integrity constraints of the form ·

Obviously, the stable models of a normal program P are exactly the general stable models of the abductive frame­ work (P, 0, 0} . From this it is immediate that the exis­ tence of general stable models is not guaranteed. Gen­ eral stable models thus do not solve the problem of non­ existence of stable models for normal programs.

Dung's abductive frameworks [3] are equivalent to Esghi/Kowalski's, that is he requires the programs in frameworks to consist of definite clauses. To be able to handle normal programs he replaces predicate sym­ bols p in negated literals by new symbols p*, as in Es­ hghi/Kowalski's approach. He also uses integrity con­ straints of the form

but no constraints corresponding to the metalevel con­ straints involving the predicate Demo. Atoms built from the new symbols become abducibles .

Dung calls S = P U H a scenario of the abductive framework (P, A, I} if H is a subset of the abducible atoms such that PUHUI is consistent. Let inout(S) de­ note the set of ground atoms provable from a scenarioS. A set of abducible atoms E is a P-evidence for an atom p iff PUE 1- p. An abducible p*(t) isS-acceptable iff for every P-evidence E of p(t), E U inout(S) U I is inconsis­ tent . A scenario Sis admissible if every abducible atom in S is S-acceptable. An admissible scenario is complete iff every abducible atom that is also S-acceptable is con­ tained in S.

The complete scenarios define the semantics of a nor­ mal logic program. Dung was able to show that the set of complete scenarios forms a semi-lattice with respect to set inclusion. The least complete scenario is equivalent to the well-founded model. Stable models correspond to maximal complete scenarios. However, not every maxi­ mal complete scenario represents a stable model. Con­ sider the program P3 :

The transform of the program, P*3 , is:

Additionally we have, for x E {a, b, c} the integrity con­ straints

We get two maximal complete scenarios, namely

S1 corresponds to the single stable model {a} of P3 . S2, although maximal, does not correspond to a stable model. This raises the question what the "interesting" ones among the complete scenarios are. Dung argues that two views are reasonable: a skeptical view which considers the least complete scenario only, and a credu­ lous view which considers all maximal complete scenar­ ios. In examples like the one just discussed there seems to be no reason to dispense with stable semantics, un­ less one adheres to the skeptical view. In a sense, Dung's credulous view seems to move too far away from stable semantics, whereas the two abductive approaches men­ tioned earlier stick with it too closely.

The abductive framework we present in this paper is distinct from this earlier work in the following respects:

1. We do not restrict the abducibles to atoms. This has the advantage that we can operate on the original programs directly and do not have to use any kind of transformation of the programs. Moreover, this makes the use of integrity constraints unnecessary.
2. The above approaches treat program rules as clauses and need some implicit device to obtain the direct­ edness of rules. We consider the rules of a program as a set of inference rules, not as clauses.
3. We apply a new simple maximality criterion that guarantees that the right sets of abducibles are cho­ sen. This criterion models the intuition that unde­ finedness should be minimized.
4. Our framework is simpler than the above ap­ proaches and can, unlike them, be applied to logic programs with classical negation and epistemic dis­ junction, as well as other consistency-based non­ monotonic formalisms .

The rest of the paper is organized as follows: in Section 2 we introduce our abductive framework and show how it can be used to formalize normal logic programs. In Section 3 we treat general logic programs with classical negation and epistemic disjunction in the heads. Section 4 applies our abductive method to default logic, Section 5 applies it to autoepistemic logic.

2 The abductive framework

In this section we introduce our abductive semantics for normal logic programs . We define the notion of an ex­ tension for a logic program. This terminology reflects the similarity to other work in nonmonotonic reasoning, in particular default logic.

By Lit- we mean the set of literals, that is, any sen­ tence of the form a or "'a, where a is an atom.

Definition 1 A norma/logic program P is a set of rules of the form

where a is an atom and the b; are in Lit-.

We use NEG(P) to denote the set of negative literals relevant to a logic program P, i.e. NEG(P) = {"'a E Lit- I a is a subformula of P}.

The notion of consistency plays a predominant role in abduction. We therefore have to define its meaning in the context of a logic program:

Definition 2 Let L ~ NEG(P) be a set of negative lit­ erals, P a norma/logic program. The closure of L under P, Cp(L), is the smallest set such that

Definition 3 Let L ~ NEG(P) be a set of negative lit­ erals, P a normal logic program. L is ?-consistent iff Cp(L) is consistent.

Definition 4 Let P be a normal logic program. P is consistent iff 0 is ?-consistent.

Similar to the earlier abductive treatments of logic pro­ grams we model negation as failure abductively. How­ ever, since we do not require abducibles to be atoms, we do not need to transform programs but can directly use NEG(P) as the set of abducibles. The main diffi­ culty is that we cannot consider all maximally consistent subsets of NEG(P) as representing the intended mean­ ing of a program. This simple approach fails to capture the intuitions underlying logic programming as can be demonstrated by our program P1 .

The standard reading of this program is that b is deriv­ able and a underivable. However, there exists a maximal ?-consistent subset of NEG(P), namely H 1 = {""b} that fails to capture this intuition. The closure of H1 under P1 contains a but not b. This clearly violates all of the standard semantics for logic programs, and H 1 should not be considered an acceptable set of hypotheses.

What then are the acceptable sets of hypotheses, or­ in our terminology - the extension bases, that can be used to define the meaning of a logic program? It turns out that an idea used in (15] for reasoning about sim­ ple causal systems can be applied to solve this problem. The reader may observe that among the two maximally consistent subsets of NEG(P) in the above example, the wanted subset, H 2 = { ""C, "'a} allows us to derive b, that is refutes the remaining hypothesis in NEG(P). The un­ intended subset, on the other hand, does not refute the hypothesis "'C. It turns out that, to capture the intuition behind logic programs, we have to maximize not just the set of hypotheses, but also the set of refuted hypotheses. This leads to the following definitions:

Definition 5 Let P be a logic program, H ~ NEG(P), and C a ?-closure of H. The P-cover of C, COV p(C), is the set

Definition 6 Let P be a logic program, H ~ NEG(P), and C a ?-closure of H . C is an extension of P iff

1. C is consistent,
2. there is no H' ~ NEG(P) with consistent closure C' such that COVp(C) c COVp(C').

If C is an extension, H is called an extension base of P .

For normal logic programs there is only one closure of any setH~ NEG(P) , so extension bases and extensions are isomorphic. For disjunctive logic programs there may be several closures, so we give the more general definition here.

It is obvious that our example gives only rise to one extension, as intended, since COV p(Cp(H1)) = {--a,--b} C {--a, -b, -c} = COVp(Cp(H2)). This ex­ tension coincides with the unique stable model of the program. This is not incidental. We can show that our semantics and stable model semantics coincide in cases where stable models exist .

Proposition 1 Let P be a normal logic program for which a stable model exists. M is a stable model of P iff it is an extension of P .

Obviously, the existence of extensions for normal logic programs is guaranteed since every such program must be consistent. This is achieved because, contrary to sta­ ble models, extensions do not have to contain either a or -a for every atom a. Consider the following example:

This program has no stable model, yet it has an exten­ sion generated by the extension base { -c}.

Extensions thus have the well-known property of the well-founded semantics [20) in allowing truthvalue gaps, that is , neither a nor -a is in the extension of the above program. But like stable models, extensions do not suf­ fer from the problem of "floating conclusions ." In the following example, the well-founded semantics does not conclude p, while pis part of every extension.

We discussed several related abductive approaches and their weaknesses in the introduction already. Another approach which can, in a sense, be considered dual to ours is that of Inoue [12) . He distinguishes between a set of necessary rules T and a set of hypothetical rules H . A model in his system is a stable model of TU H', where H' is a maximal subset of H such that a stable model exists. Inoue thus dispenses with some of the hypothetical rules if necessary and sticks with stable semantics otherwise, whereas we leave the truth values of atomic propositions undecided if necessary.

A further - non-abductive- approach of interest here is that of Sacca and Zaniolo [19) . It is based on the notion of ?-stable models. Such models are partial, i.e., not all atomic propositions need to get a truth value. We cannot give the exact definition of this notion here, but want to stress that it is intended to capture "the three key properties considered highly desirable by researchers in this area" . According to the authors these properties are

• consistency: no proposition should be true and false at the same time in a model,
• justifiability: every positive conclusion should be demonstratable using the directed rules of the pro­ gram,
• minimal undefinedness: the number of undefined facts should be reduced as much as possible.

As Sacca and Zaniolo show ?-stable models do not guar­ antee minimal undefinedness: ?-stable models can be proper subsets of other ?-stable models. The authors therefore propose "that the minimal undefinedness prin­ ciple should be enforced by restricting our attention to the class of ?-stable models that are maximal ." Unfortu­ nately, maximality is insufficient to guarantee minimal­ undefinedness as can be demonstrated by the program P3 used earlier in the introduction:

Besides the uncontroversial maximal ?-stable model sl = {a, -b, -c} we also obtain the ?-stable model s2 = {-a, b} . s2 clearly is maximal, as the addition of ....,c leads to inconsistency whereas the addition of c cannot be justified by any of the available rules. Nev­ ertheless, s2 does not minimize undefinedness: c has no truth value in S2 but is false i~ S1 . In our framework the single extension corresponds to S1 . There is no extension corresponding to s2.

3 General Logic Programs

In this section we will consider general logic programs, that is, programs where negations and disjunctions may appear in the head of a rule, and in addition there is a classical negation operator. It turns out that all we have to do is slightly generalize the notion of ?-closure.

As in [7), we use two negation operators, ....., and ....... . ....., is classical negation, while ....... is negation as failure to prove. By Lit we mean the set of classical literals, and by Lit+, the set of literals of the form I or ....... /, where I is in Lit.

Definition 1 A genera/logic program P is a set of rules of the form

where all the literals c, and bi are in Lit+ .

Note that this definition generalizes (7) slightly by allow­ ing negation-as-failure literals in the head of a clause. As usual, by NEG(P) we mean the set of negative literals { -/ I either I or -I is a literal of P} .

We interpret disjunction in the head in the same way as Gelfand and Lifschitz, that is, it is epistemic disjunc­ tion. The condition on the ?-closure is that at least one of the literals in the head must appear in the closure.

Definition 8 Let L be a set of literals from NEG(P) . C is a ?-closure of L if it is a smallest set such that

1. L~ C,
2. if I and ....... / or a and ...,a are in C, then C = Lit+,
3. if c1l · · ·I em +- b1, ... , bn E P, and b1, . . . , bn E C then for at least one of the c,, c, E C .

Note that there is not necessarily a unique P-closure of a program; however, if it has a consistent P-closure, then all its P-closures are consistent . The unique incon­ sistent P-closure is the set of all literals. We say L is ?-consistent if it has a consistent P-closure. All other definitions from the last section can now be applied with­ out further changes to general logic programs. Here is an example involving disjunctions in the head of a rule:

We obtain two extensions, E1 = {a, ...... c, ...... b} and E2 = {b, ...... c, ---a}. Both have the cover NEG(P) . Note that {---a, ...... b} is not an extension since its cover does not contain ---c.

The following slight modification of the last example involves a negation in the head:

Now there is only one extension, namely {---a, ---b, ...... c} .

General programs can be used to implement many of the standard default reasoning examples. Here is a bird example:

We obtain one extension from the extension base { ---ab2} (we omit the irrelevant literals ---fly, ..__...,fly, etc.). The P-cover of this extension is NEG( P). Note that the set of abducibles { ...... abl} is not an extension base as its P-cover does not contain ---ab2. As intended the more specific rule gets priority.

As with normal logic programs, extensions of general logic programs correspond to the answer sets of Gelfond and Lifschitz, when the latter exist .

Proposition 2 Let P be a genera/logic program with no negation-as-failure literals in the head and suppose it has at least one consistent answer set. Let C facts( L) denote the set of classical literals (without weak negation) in L. C facts is a bijective mapping from the set of extensions of P to the set of answer sets of P.

If there are multiple extensions, then they are always disjoint.

Proposition 3 If F and F' are two extensions, then F U F' is inconsistent.

It should be noted that the introduction of negation in the heads of rules, of either type, leads to a situa­ tion where the existence of extensions can no longer be guaranteed for all programs. The reason is that the pr~ grams themselves may become inconsistent. Recall that a program P is inconsistent if the (single) P-closure of the empty set is inconsistent . It is not difficult to prove the following lemma: 3

3 The proof is easy since, as mentioned in the begin­ ning, we only consider propositional programs with finite Herbrand base in this report. However, there are cases in which, for infinite NEG(P), there is an infinite ascending cha.in COVp(Cp(Ht)) c COVp(Cp(H2)) c ... , a.nd hence no extensions.

Lemma 1 Let P be a logic program. P has an extension iff P is consistent.

Obviously, all programs where the negation sign (and .l) does not appear in the head of a rule are consistent and therefore have at least one extension. This includes normal logic programs.

Sometimes it is convenient and useful to restrict the set of abducibles to a proper subset of NEG(P) . A logic program then consists of a set of rules P together with a set HYP of negated literals representing the atoms as­ sumed to be false by default. The P-cover of a closure of a set of abducibles H ~ HYP is, as before, the set of abducibles which are either assumed or refuted.

For instance, in the bird example we get the de­ sired results if we restrict the abducibles to HYP = { ---ab1, ---ab2} . Again we get one extension containing -,fly. The extension base is {---ab2}. Note that the cover of this extension is HYP, whereas the cover of the closure of H 2 = { ---abl} does not contain ---ab2 . H 2 therefore is not an extension base.

There is also no reason why we should not some­ times let positive information, that is unnegated atoms, or even arbitrary formulas be contained in the set of abducibles. This gives us the possibility to generalize "negation as failure to derive" to "assertion as failure to refute" . Assume we represent the bird example in the followin$, equivalent way

Letting HYP = { normah, normaJ2} obviously yields re­ sults which are equivalent to those of our original repre­ sentation using ab-predicates.

Another interesting extension of this approach are pri­ oritized logic programs. We may introduce explicit prior­ ities among the hypotheses, e.g. in the style of preferred subtheories (1]. The set of assumables HYP can be di­ vided into preference levels H 1, H 2, . . .. An extension base E1 is preferred to an extension base E2 iff there is an i such that

Here is an example

Let HYP = { ---ab1, ---ab2} and assume we want to give the Quaker rule priority. This can be done by splitting HYP to H1 = {---abl} and H2 = {---ab2} . There are two extension bases, H1 and H2. It is easy to see that, according to our definition, the first one is preferred over the second one.

Remark: In this example this is the same as adding ab2 ..,_ ---ab1 to the program, that is we have a choice whether we want to represent priorities explicitly using an ordering on HYP, or via additional rules using the available implicit prioritization. We suspect that explicit orderings make programs often more readable. Note that in case of a conflict between explicit and implicit priori­ ties the implicit ones win since only extension bases are compared in our definition of preferred extension bases, and these respect the implicit priorities.

4 Default logic

The same abductive method for general logic programs is applicable to default logic as well. In fact, default logic rules can be viewed as a generalization of logic program rules to the full sentences, rather than just literals.

We use the more general disjunctive default theories of Gelfond et al. [8], since there is a direct correspondence to disjunctive logic programs . A disjunctive default has the form

where all the arguments are arbitrary sentences.

We begin by recalling the definition of an extension of a default theory (W, D) .

Definition 9 Let f(S) be any least set such that:

1. W ~ f(S) .
2. r(S) is deductively closed.
3. If a E f(S) and all {3; are consistent with S then one of li is in f(S) .

An extension of (W, D) is any setS that is equal to some r(s) .

As was the case with general logic programs, the closure operator is not necessarily unique .

To make the connection with the abductive method, note that the hypothesized set S are the sent~nces that are supposed to be in the extension, rather than the complement, as for logic programs. The operator f(S) corresponds to the closure of a program. With this in mind, we can rewrite the above definition in the abduc­ tive spirit .

Definition 10 Let C be some f(S). The cover COV 6 (C) with respect to .6. = (W, D) is the set:

where S are all sentences not in S .

Given the identification of S with the complement of the abductive hypotheses, this definition corre~onds to that for the cover of logic programs. The set S are the sentences assumed to be unproven in the default theory, and the added set are those hypotheses refuted by the theory. Once again, abductive extensions are formed by maximizing this union.

Definition 11 Let C be some f(S). C is an abductive extension of .6. iff:

1. c~ s.
2. COV 6 (C) is maximal.

The first condition is easily seen to be a consistency con­ dition, as it is equivalent to saying the whenever a sen­ tence ¢ appears in S, it does not appear in f(S) . The second condition is the familiar maximality filter. It is obvious that COY 6(f(S)) is maximal and consistent if S = f( S), precisely the requirement for standard exten­ sions. Hence the following proposition.

Proposition 4 If the default logic theory .6. = (W, D) has an extension and if W is consistent, then E is an abductive extension of .6. if and only if it is an extension of .6..

Even in the cases where there is no default extension, there is an abductive extension.

Proposition 5 If a default theory .6. = (W, D) has a finite set of justifications {over all defaults) and if W is consistent, then it has an abductive extension.

Finally, the relation between logic programs with clas­ sical negation and default theories pointed out by Gel­ fond et al. holds for abductive extensions as well .

Proposition 6 Let D be a set of defaults formed from the logic program P by the translation:

where the a;, bj, and Ck are all classical literals. L zs an answer set for P if and only if it is the set of literals contained in an extension of the default theory (0, D) .

5 Autoepistemic logic

The same abductive approach is also applicable to au­ toepistemic (AE) logic and its variants, including the minimal-knowledge logic MBNF [16). We will just show the results for standard AE logic here.

We give a brief review of AE logic concepts; for a more complete reference see [14) . In AE logic, the language Cis formed by augmenting a propositional language Co with a modal operator L for self-belief. The construction -.LS is the set { -.L¢ I ¢ E S} . Finally, deduction under the modal system /( 45 is denoted by f-K 45 .

Definition 12 Let A be a set of sentences of C. Let U be a subset of Co and U its complement Co - U. U is a moderately-grounded extension of A iff it satisfies the equation:

We have used the definition of moderately-grounded ex­ tensions because it is easier to see the correspondence to the logic programming and default logic cases. The hypotheses will be a set of negative modal literals -.LS, and the closure of an AE theory A under the hypothe­ ses is given by CA(S) = {¢ E Co I AU -.LS f-K45 ¢} . The cover of the theory is defined as the hypotheses S, together with all those hypotheses refuted by the closure.

Definition 13 The cover of an AE theory A under hy­ potheses S, COV A(CA(S)), is given by:

As before, an abductive extension is a consistent maxi­ mal hypothesis set .

Definition 14 The closure of an AE theory A, CA(S), is an abductive extension of A iff

1. CA(S) is consistent.
2. COV A(CA(S)) is maximal.

The main theorems about abductive extensions is that they always exist (if A has a finite set of modal liter­ als) and that they are equal to AE moderately-grounded extensions, when the latter exist .

Proposition 7 If A is K 45-consistent and has a finite number of modal atoms that appear positively, then A has an abductive extension.

Proposition 8 If A is K 45-consistent and has an AE moderately-grounded extension, then U is such an exten­ sion if and only if it is an abductive extension of A.

The key feature of abductive extensions is that a proposi­ tion may be neither believed (Lp) nor disbelieved (-.Lp) in the extension. This corresponds to the truthvalue gaps of logic programming extensions. Morris [17] defines an alternative method for giving extensions to extensionless AE theories. However, he does so by adding propositions necessary to make the fixpoint consistent, rather than leaving the belief in the propositions undecided.

6 Conclusion

We have demonstrated an abductive approach to the major consistency-based nonmonotonic formalisms . Our approach improves over previous attempts in having a straightforward relationship to the standard semantics for these formalisms, and generalizing to more complex languages. We have shown how the same idea, maxi­ mizing assumed and refuted hypotheses, can be used to establish extensions in logic programs, default logic, and autoepistemic logic. The common characteristic of these abductive extensions is that they always exist (for finite theories), they reduce to the standard extensions when the latter exist, and they allow a truthvalue gap in the cases where standard extensions do not exist.

Given the abductive nature of the definition, it might be possible to use the abundant literature in abductive methods to find approximate proof-theory methods for these formalisms (see, for example, [10, 2, 5, 18, 11, 6]) .