Donald.nute.ws

Ambiguity Propagating Defeasible Logic and the Department of Computer Science and Artificial Intelligence Center Abstract. The most recent version of defeasible logic (Nute, 1997) is related tothe well-founded semantics by translating defeasible theories into normal logicprograms using a simple scheme proposed in (Brewka, 2001). It is found thatby introducing ambiguity propagation into this logic, the assertions of defeasibletheories coincide with the well-founded models of their logic program transla-tions. Without this addition, the two formalisms are found to disagree in impor-tant cases.
A translation in the other direction is also provided. By treating default negatedatoms as presumptions in defeasible logic, normal logic programs can be con-verted into equivalent defeasible theories.
This paper relates the most recent version of defeasible logic described in (Nute, 1997)to the well-founded semantics for normal logic programs via a translation scheme.
After the scheme is presented, it is shown that in important cases the conclusions ofa given defeasible theory do not correspond with the logic program's well-foundedmodel. However, by modifying the proof system of defeasible logic, a new ambiguitypropagating variant is created, and for this new variant the correspondence holds.
The translation scheme used here was first proposed in (Brewka, 2001) and was used to compare logic programs under a prioritized well-founded semantics to a variantof defeasible logic presented in (Antoniou et al., 2000). For the purposes of this paper,we will call the defeasible logic presented in (Nute, 1997) NDL to distinguish it fromother variants. The ambiguity propagating variant presented here will be called ADL.
NDL goes beyond the variants presented in (Antoniou et al., 2000) by including a moreextensive treatment of the ways that defeasible rules may conflict and by explicitlyconsidering failures of proofs due to cycles in rules. Both of these are important im-provements in defeasible logic, and the impact of these changes are discussed in detailin (Nute, 2001).
Another translation scheme for NDL is found in (Maier & Nute, 2006). Defeasible theories are translated into logic programs via the introduction of new literals explicitlyrepresenting rules and conflicts. The scheme has the virtue of allowing one to suc-cessfully embed defeasible theories of NDL into logic programs, but it does not revealany deep connection between defeasible logic and logic programming. The translation there is in turn based upon one found in (Antoniou & Maher, 2002) which uses a nota-tional variant of an earlier version of defeasible logic described in (Nute 1992, 1994).
Antoniou and Maher show a relationship between this variant and stable models, butthe result is limited to defeasible theories without cycles in their rules. They establisha more general relationship between all defeasible theories and Kunen's three-valuedsemantics (Kunen, 1987).
The main contribution of this paper is the development of the ambiguity propagating defeasible logic ADL and a demonstration of a correspondence between the assertionsof ADL theories and the well-founded models of the translations. The well-foundedsemantics can thus be viewed as indirectly providing a semantics for ADL. This resultallows us to use the translation method together with a proof method that is sound withrespect to the well-founded semantics as an implementation of ADL.
Furthermore, it is shown here that normal logic programs can be translated into ADL theories in such a way that the well-founded model of a given logic programcorresponds to the assertions of its translation. Each default negated literal 'not p' ofthe program is treated as a defeasible rule ∅ ⇒ ¬p of the defeasible theory (stating, ineffect, that ¬p presumably holds).
This section presents the language of NDL and its ambiguity propagating counterpartADL as well as proof systems for each. NDL is presented first, and ADL is presented asa modification of NDL's proof system. For a fuller discussion of NDL, see (Nute, 2001).
The well-formed formulas in the common language of NDL and ADL are literals (atomic sentences and their negations). The language also contains strict rules, writtenA → p (where p is a literal and A a finite set of literals), defeasible rules (written A ⇒p), and undercutting defeaters or simply defeaters (written A to stand for any rule, whether strict, defeasible, or defeater. Where A is the empty set or a singleton, we will often omit the braces (writing ⇒ p instead of{} ⇒ p).
The basic idea behind the proof theory for NDL is that we can derive a literal p from a defeasible theory just in case p is the head of some strict or undefeated defeasible rulein the theory and all of the literals in the body of the rule are also derivable. A strict rulewith an empty body is called a fact and the head of such a rule is by definition alwaysderivable. A defeasible rule with an empty body is called a presumption and may bedefeated by other rules. The role of defeaters is solely to defeat other arguments thatmight otherwise establish a literal. E.g., the defeater q proving p, but it cannot be used to directly prove ¬p.
Definition 1: A defeasible theory D is a triple R, C, ≺ , where R is a finite set of rules,each with a possibly empty antecedent, C a set of finite sets of literals in the languageof D such that for any literal p appearing in D, {p, ¬p} ∈ C, and ≺ an acyclic binarysuperiority relation over the non-strict rules in R.
Let D = R, C, ≺ be a defeasible theory. The sets of literals in C are called conflict sets. Each conflict set cs ∈ C specifies a set of literals that cannot simultaneouslyconsistently hold. If C only contains sets of the form {p, ¬p}, we say D has a minimal conflict set. We say that the conflict set C is closed under strict rules if, for all cs ∈ C,if A → p is a rule and p ∈ cs, then {A ∪ (cs − {p})} ∈ C. It is not a necessarycondition that a defeasible theory be closed under strict rules, but it is certainly anattractive condition. We will call a defeasible theory closed if its conflict set is closedunder strict rules.
The proof theory for NDL is based upon argument trees.
Definition 2: Let D be a defeasible theory and p a literal appearing in D. The expressionD |∼ p is called a positive defeasible assertion, while D ∼| p is called a negativedefeasible assertion. When it is clear which theory is in question, the assertions may beabbreviated |∼ p and ∼| p Informally, D |∼ p and D ∼| p are interpreted to mean that a demonstration (re- spectively, a refutation) exists for p from D. Note that D ∼| p is equivalent to neitherD |∼ ¬p nor D |∼ p. D ∼| p means that there is a demonstration that there is nodefeasible proof of p from D.
Definition 3: τ is an argument tree for D iff τ is a finite tree such that every node of τis labeled either |∼ p or ∼| p (for some literal p appearing in D).
Definition 4: The depth of a node n is k iff n has k ancestors in τ. The depth of a treeis taken to be the greatest depth of any of its nodes.
Definition 5: Let A be a set of literals, and n a node of a defeasible argument tree τ : 1. A succeeds at n iff for all q ∈ A, there is a child m of n such that m is labeled |∼ q.
2. A fails at n iff there is a q ∈ A and a child m of n such that m is labeled ∼| q.
Definition 6: τ is a defeasible proof in NDL iff τ is an argument tree for D, and foreach node n of τ , one of the following obtains: a. there is a strict rule r : A → p ∈ R such that A succeeds at n, orb. there is a defeasible rule r : A ⇒ p ∈ R such that A succeeds at n and for all cs ∈ C, if p ∈ cs, then there is a q ∈ cs − {p} such that for all ruless : B q ∈ R, either B fails at n or else s ≺ r.
a. for all strict rules r : A → p ∈ R, A fails at n, andb. for all defeasible rules r : A ⇒ p ∈ R, either ii. there is a cs ∈ C such that p ∈ cs, and for all q ∈ cs − {p}, there is a rule q ∈ R such that B succeeds at n and s ⊀ r.
3. n is labeled ∼| p and has an ancestor m in τ labeled ∼| p, and all nodes between n and m are negative defeasible assertions.
Condition 6.3 is called failure-by-looping. Since conclusions cannot be established by circular arguments, failure-by-looping can help to show that a literal cannot be de-rived from a defeasible theory.
Definition 7: Where D is a defeasible theory and p is a literal appearing in D, D |∼NDLp iff there is a defeasible proof τ in N DL such that the root of τ is labeled |∼ p.
D ∼|NDL p iff there is a defeasible proof τ such that the root of τ is labeled ∼| p. If Sis a set of literals appearing in D, D |∼NDL S if and only if for all p ∈ S, D |∼NDL p.
D ∼|NDL S iff for some p ∈ S, D ∼|NDL p.
Some important formal properties of NDL are established in the following theo- Theorem 1 (Coherence): If D is a defeasible theory and D |∼NDL p, then D ∼|NDLp.
Theorem 2 (Consistency): If D = R, C, ≺ is a defeasible theory, C is closed understrict rules, S ∈ C, and D |∼NDL S, then {A → p : A → p ∈ R}, C, ≺ |∼NDL S.
Theorem 3 (Cautious Monotony): If D = R, C, ≺ is a defeasible theory, D |∼NDLp, and D |∼NDL q, then R ∪ {→ p}, C, ≺ |∼NDL q.
Theorem 1 assures us that we cannot both prove and demonstrate the absence of any proof for the same literal. Theorem 2 says that when conflict sets are closed understrict rules, any incompatible set of literals in NDL derivable from a defeasible theorymust be derivable from the strict rules alone. In other words, the defeasible rules ofa theory can never introduce any new incompatibilities. Of course, this interpretationof Theorem 2 assumes that all possible incompatibilities are captured in the conflictset of the theory. Cautious Monotony is a principle which many authors working onnonmonotonic reasoning propose as a necessary feature for any adequate nonmonotonicformalism.
The advantages of adding failure-by-looping to our proof theory should be obvious.
Consider the simple defeasible theory D1 below.
In earlier versions of defeasible logic that lacked failure-by-looping, although we could easily see that there was no way to show D1 |∼ bat, we could not demonstratethis in the proof theory, that is, we could not show D1 ∼| bat. Consequently, neithercould we show D1 |∼ ¬f lies. Failure-by-looping provides a mechanism for showingD1 ∼|NDL bat, which then allows us to show D1 |∼NDL ¬f lies.
When we later define a translation of defeasible theories into standard logic pro- grams in such a way that the consequences of a theory correspond to the well-foundedmodel for the logic program, this example will also serve to show that failure-by-looping is necessary to get this correspondence. Where the theory D1 above is trans-lated into ΠD , the literals bat, f urry, and has wings are all unfounded, but ¬f lies is well-founded. The corresponding literals are undetermined in versions of defeasiblelogic without failure-by-looping. Where a defeasible theory has cyclic rules, failure- by-looping is needed to capture within the proof theory the concept of a literal beingunfounded.
Adding explicit conflict sets and closing them under strict rules provides an alter- native solution to a class of examples that have always seemed odd to the authors.
Consider the defeasible theory D2 = {⇒ p, ⇒ q, p ⇒ r, q ⇒ r, p → ¬q, q → ¬p}, C, ∅ where C is closed under the strict rules in R. The corresponding default theory is R2 = {¬(p ∧ q)}, { :p , :q , p:r , q:r } The classical part of R2 containing the sentence ¬(p ∧ q), acts like the conflict set in thedefeasible theory and ensures that p and q do not both belong to the same extension. R2has two extensions containing {p, r} and {q, r}, and the intersection of these extensionscontains {r}. r is a "floating conclusion" of R2 because it belongs to every extensioneven though there is no sentence that supports it that belongs to every extension.
This seems unintuitive to us. In NDL, the rules ⇒ p and ⇒ q conflict with each other since {p, q} is a conflict set in the theory. Neither rule takes precedence overthe other; so neither consequent is defeasibly derivable. Thus neither of the rules toestablish r is satisfied, and r is also not defeasibly derivable. Our proof theory avoidsthese floating conclusions in an intuitively reasonable way.
Consider the defeasible theory below in which conflict sets are minimal (from Brewka2001).
D3 = {⇒ p, ⇒ ¬p, ⇒ q, p ⇒ ¬q}, C, ∅ We have D3 ∼|NDL p, D3 ∼|NDL ¬p, D3 ∼|NDL ¬q, and D3 |∼NDL q. This shows that NDL is ambiguity blocking. An argument exists for p, and hence ¬q, but thisdoes not prevent us in NDL from concluding q. Many feel that ambiguity propagatingsystems, where such conclusions are forbidden, are intuitively more reasonable. Anambiguity propagating defeasible logic is presented in (Antoniou & Maher, 2002), andit is this variant that Brewka in (2001) considers for translation into logic programs. Hedismisses an earlier, ambiguity blocking variant.
It turns out that a very minor modification to the proof system of NDL produces an ambiguity propagating defeasible logic (ADL), and it is precisely this modification thatensures that the results of a defeasible theory match those of its logic program counter-part under Brewka's translation (so that D |∼ADL p if and only if p ∈ wf m(ΠD) andD ∼|ADL p if and only if ¬p ∈ wf m(ΠD)). The modification creating ADL affectsonly part 2.b.ii of Definition 6. It specifies that p is defeated only if every defeasible rule in support of p fails or else is defeated by a satisfied strict rule or a defeasible ruleof strictly higher precedence for each element q ∈ cs − {p}. In NDL, a rule of equalprecedence can be used. The modification (Definition 8) is shown below.
Definition 8: τ is a defeasible proof in ADL iff τ is an argument tree for D, and foreach node n of τ , one of the following obtains: a. there is a strict rule r : A → p ∈ R such that A succeeds at n, orb. there is a defeasible rule r : A ⇒ p ∈ R such that A succeeds at n and for all cs ∈ C, if p ∈ cs, then there is a q ∈ cs − {p} such that for all ruless : B q ∈ R, either B fails at n or else s ≺ r.
a. for all strict rules r : A → p ∈ R, A fails at n, andb. for all defeasible rules r : A ⇒ p ∈ R, either ii. there is a cs ∈ C such that p ∈ cs, and for all q ∈ cs − {p}, there is a rule q ∈ R such that B succeeds at n and s is strict or else r ≺ s.
3. n is labeled ∼| p and has an ancestor m labeled ∼| p, and all nodes between n and m are negative defeasible assertions.
Apart from this modification, all other aspects of the proof system are left alone.
In example 3 above in ADL, one sees that since the rules for p and ¬p are of thesame precedence, neither D3 ∼|ADL p nor D3 ∼|ADL ¬p can be shown. BecauseD3 ∼|ADL p cannot be shown, D3 ∼|ADL ¬q cannot be shown, and so neither canD3 |∼ADL q. Each of these literals is underdetermined in ADL, neither defeasiblyproven nor refuted.
The default theory corresponding to D3 is R3 has three default extensions containing {p, q}, {p, ¬q}, and {¬p, q}. Notice that theintersection of these three extensions is "empty". So the "sceptical" interpretation ofR3 agrees with ADL in this case.
By examining the definition of proof trees for both NDL and ADL, it can be seen that every valid proof in ADL is a valid proof in NDL.
Theorem 4: If D is a defeasible theory and D |∼ADL p, then D |∼NDL p. If D ∼|ADLp, D ∼|NDL p.
ADL versions of Theorems 1, 2, and 3 also hold.
The Well-Founded Semantics for Normal Logic Programs A logic program Π consists of a set of rules having the form where p and each subgoal qi is an atomic formula, or else such a formula preceded bythe symbol not (often called negation-as-failure or negation-by-default). We will call asubgoal in which not occurs negative. The other subgoals are positive.
If a program contains no negative subgoals, then it is called definite and has a unique Herbrand model (Emden & Kowalski, 1976). This is often taken to be the intendedmeaning of the program. Programs in which not appears are called normal programs.
Importantly, normal programs need not have a single least Herbrand model. E.g., theprogram p :− not q has two minimal Herbrand models: {p} and {q}. The well-foundedsemantics (Gelder, Ross, & Schlipf, 1988), (Gelder, Ross, & Schlipf, 1991) was devel-oped to provide a reasonable interpretation of logic programs containing negation. Forevery program, a unique well-founded model exists. The well-founded model for theprevious program is {p, ¬q}.
Let Π be a normal logic program containing only ground atoms and BΠ the set of atoms appearing in Π. An interpretation I of Π is any consistent set of positive andnegative literals whose atoms are taken BΠ. If p appears in I, then p is said to be truein I. If ¬p appears in I, then p is false in I. If neither p nor ¬p appears in I, then p issaid to be undefined in I.
A set of atoms S ⊆ BΠ is said to be unfounded with respect to an interpretation I iff for each p ∈ S and for each rule r of Π with head p, there exists a positive ornegative subgoal q of r such that 1. q is false in I, or2. q is positive and q ∈ S.
Unfounded sets are closed under union, and so for any Π and I, there exists a greatest unfounded set of Π wrt I, denoted UΠ (I): {A | A is an unfounded set of Π with respect to I}.
UΠ (I) can be viewed as a monotone operator and is used to derive the negative consequences of a program. The immediate consequence operator T , defined below, isused to derive the positive consequences of a program.
TΠ (I) = {p | r is a rule of Π with head p, and each qi in the body of r is in I}.
These two operators are combined to form a third: where ¬. UΠ (I) is the element-wise negation of UΠ (I). UΠ (I), TΠ (I), and WΠ (I)are all monotonic, and can be used to define the sequence The well-founded model of Π, wf m(Π), is the limit of this sequence.
Translating Defeasible Theories into Logic Programs (Brewka, 2001) provides a simple and natural translation scheme to compare a ver-sion of defeasible logic (Antoniou & Maher, 2002) to logic programs using a priori-tized well-founded semantics. Several examples are presented to demonstrate that thetwo systems do not agree, and it is argued there that the results of the defeasible theoryare less reasonable.
We have altered the translation scheme to account for extended conflict sets and will use it to compare ADL to the WFS for normal programs. Only finite grounded defea-sible theories and programs are considered. Since conflict sets are sufficient to encodenegation, we will assume all literals appearing in a defeasible theory are positive (¬p isrepresented as p ). The translation thus necessarily yields a normal logic program. Fur-thermore, since (as discussed in the next section) defeaters and the precedence relationdo not add to the expressiveness of defeasible logic, we will assume that no defeatersoccur in the theory and that the precedence relation is empty.
Let D = R, C, ≺ be a defeasible theory such that no defeaters occur in R and ≺= ∅. We define the logic program ΠD as follows.
1. If q1, q2,. , qn → p ∈ D, then p :−q1, q2,. , qn ∈ ΠD.
2. Let cs1, cs2,. , csm be the conflict sets of D containing p and (a1, a2,. , am) any tuple in (cs1 − {p}) × (cs2 − {p}) ×. × (csm − {p}). If q1, q2,. , qn ⇒ p∈ D, then p :− not a1,. , not am, q1, q2,. , qn ∈ ΠD.
Each ai corresponds to some literal of a conflict set containing p, and in order for adefeasible rule to succeed at least one literal from each conflict set must fail. Signifi-cantly, if conflict sets are minimal, then the above translation of defeasible rules reducesto p :− not p , q1, q2,. , qn.
As the following examples show, the results of NDL are often incorrect with respect to the well-founded model of the Brewka inspired translation.
D4 = {⇒ p, ⇒ p }, {p, p }, ∅ΠD = {p :− not p., p :− not p.} Here, D4 ∼|NDL p and D4 ∼|NDL p but the well founded model of ΠD is empty.
According to the WFS, p is undefined.
D5 = {p → p}, {p, p }, ∅ΠD = {p :−p} Both D5 ∼|NDL p and D5 ∼|ADL p. Without failure-by-looping, neither of theseresults could be derived. p is unfounded in the well-founded model of ΠD.
ΠD = {p :− not p., p :− not p. , q :− not q, p., q :− not q.} D4 and D5 together show in general that, for a defeasible theory D, D ∼|NDL p is equivalent to neither ¬p ∈ wf m(ΠD) nor p undefined. In Example 6, we haveD3 ∼|NDL p, D3 ∼|NDL p , D3 ∼|NDL q , and D3 |∼NDL q. NDL is ambiguityblocking. However, the well-founded model of the logic program is empty. In general,for a defeasible theory D, D |∼NDL p does not imply p ∈ wf m(ΠD). In some casesat least, the well-founded semantics is more conservative than NDL. In contrast, theassertions of ADL are correct with respect to the well-founded semantics.
Theorem 5: Let D = R, C, ∅ be a defeasible theory of ADL without defeaters. ThenD |∼ADL p if and only if p ∈ wf m(ΠD), and D ∼|ADL p if and only if ¬p ∈wf m(ΠD).
In Example 4, no superior argument exists for either p or p , and so none of D4 ∼|ADL p, D4 ∼|ADL p , D4 |∼ADL p, or D4 |∼ADL p can be shown. In Example 5, in agree-ment with both NDL and the WFS, D ∼|ADL p can be shown using failure-by-looping.
In Example 6, arguments exist for both p and p , but no superior argument exists for ei-ther. They are both ambiguous, and this ambiguity prevents concluding anything aboutq or q.
Eliminating Precedence and Defeaters from Defeasible Logic Theorem 5 assumes that the defeasible theory to be translated does not contain anydefeaters and that the precedence relation is empty. However, eliminating these fromdefeasible logic does not lessen its expressiveness.
For any defeasible theory D = RD, CD, ≺D we can construct another, E, lacking defeaters and with an empty precedence relation, such that D and E agree on all theliterals appearing in D.
The conflict sets in E are minimal and defined using literals from RE, and ≺E is empty.
RE is constructed by explicitly representing the rules of D, as described below.
1. If r: A → p ∈ D, then ra = A → supported(r), rb = supported(r) → f ires(r), and rc = f ires(r) → p appear in RE.
2. If r: A ⇒ p ∈ D, then ra = A → supported(r), rb = supported(r) ⇒ f ires(r), p ∈ D, then ra = A → supported(r) and rb = supported(r) ⇒ 4. Let cs = {q1, q2,. qn, p} be a conflict set of D, r a defeasible or defeater rule with head p and s1, s2,. , sn rules such that si has head qi and si ⊀ r. If for eachsi, si is strict or r ≺ si, the rule supported(s1),. supported(sn) → ¬f ires(r)occurs in E. Otherwise, the rule supported(s1),. supported(sn) ⇒ ¬f ires(r)occurs in E.
Theorem 6: Let D and E be defeasible theories as defined and p a literal of D. ThenD |∼ADL p if and only if E |∼ADL p, and D ∼|ADL p if and only if E ∼|ADL p.
We have added new literals of the form f ires(r) and supported(r) which explicitly encode when a rule r of D may fire (i.e., the head is derivable) and when it is supported(ie., its body is derivable). Intuitively, if r is strict, then it may fire if and only if itsbody is supported. This is represented in ra, rb, and rc, all of which are strict. If r isdefeasible or a defeater, rb is defeasible, meaning that a rule in E with head ¬f ires(r)can potentially defeat it. If r is a defeater, ra and rb bear no relation to p and cannot beused to derive it.
In the item 4 above, we have explicitly represented when a set of rules s1,. , sm can be used to defeat another r. We need only consider an si if it is not inferior to r, forinferior rules cannot be used to defeat r.
Translating Normal Logic Programs into Defeasible Logic Here we show that normal logic programs can also be translated into defeasible theoriesso that the assertions of the theory match the well-founded model. Let Π be a normalprogram and BΠ the set of atoms in Π. For each atom b ∈ BΠ , define b to be a newatom not appearing in Π. Given these, we define a new program Φ as follows.
1. If p :−a1,. , an, not b1,. , not bm ∈ Π, then p :−a1,. , an, b ,. , b As each new atom b has exactly one rule, and the only subgoal of that rule is not b, boccurs in the well-founded model of Φ if and only if ¬b does.
Lemma 1: Let Π and Φ be programs as defined above. For any bi ∈ BΠ , b ∈ wf m(Φ) iff ¬bi ∈ wf m(Φ). Also, ¬b ∈ wf m(Φ) iff b We may view b as the positive representation of '¬b' (and for normal programs it isimpossible for b and b to both be in the well-founded model). Furthermore, with respectto the original atoms of BΠ , Π and Φ are equivalent under the WFS.
Lemma 2: Let Π and Φ be programs as defined above. For all p ∈ BΠ , p ∈ wf m(Π)iff p ∈ wf m(Φ), and ¬p ∈ wf m(Π) iff ¬p ∈ wf m(Φ).
The relationship between Π and Φ makes a translation of Π into a defeasible theory DΠ apparent. Let r = p :−a1,. an, not b1,. , not bm be a rule of Π. Define rDΠto be a1,. an, b. , b occurs in some rule of Π}. Given this, DΠ is defined as follows: where C is minimal. The default literals in the program have become presumptions inthe defeasible theory. The rules of the original program are strict in the defeasible logictheory.
It is clear given the above definition that translating DΠ into a logic program yields Φ. From Lemma 1 and Theorem 5 it follows that p is provable in DΠ if and only if p is refutable, and p is provable if and only if p is refutable. Furthermore, since according toTheorem 5 the assertions of DΠ correspond to the well-founded model of Φ, by Lemma2 the assertions of DΠ agree with the well-founded model of Π wrt BΠ.
Theorem 7: Let DΠ be defined as above. For any p ∈ BΠ , DΠ |∼ADL p iff DΠ ∼|ADLp , and DΠ |∼ADL p iff DΠ ∼|ADL p.
Theorem 8: Let Π be a normal program and DΠ its defeasible logic translation. Forany atom p ∈ BΠ , DΠ |∼ADL p iff p ∈ wf m(Π), and DΠ ∼|ADL p iff ¬p ∈wf m(Π).
Here we have replaced in the rules of Π each subgoal not p (alternatively not q) with p (alternatively q ) and added the rules p :− not p and q :− not q. The explicitlynegative literals p and q occur nowhere in the original program Π and so it is safe toequate, e.g., not p with p. The well-founded model of both Π and Φ is empty. In DΠ ,the presumption of p prevents concluding q , but there is no superior argument for q,and so q is not refuted, either. The same holds for p , and because of this nothing canbe determined for p or q. The set of assertions of DΠ is empty.
In an extended logic program, an explicitly negative literal p might already appear in Π, and so the manoeuver of replacing not p with p is no longer acceptable (theequivalence of Φ and Π would no longer hold. For instance, if Π = {p :−∅, p :−∅, q : − not p}, then the well-founded model is {p, p , ¬q}. However, Φ = {p :−∅, p :−∅, q :−p , p :− not p}, and the well-founded model of Φ is {p, p , q}.
If we instead replace not p with some entirely new literal cp, then the equivalence is restored. However, in the defeasible logic translation, p and p do not conflict (theprogram rule cp : − not p would be interpreted as a ∅ ⇒ cp and cp and p wouldconflict). This at first seems very odd. However, strictly speaking, there really is noconnection between p and p in the WFS, either. The literal p is just a rather strangelooking atom.
The two versions of defeasible logic presented here differ in that one, NDL, blocksambiguity while the other, ADL, does not. In a previous paper (Maier and Nute, 2006)we showed how to translate finite defeasible theories into normal logic programs in sucha way that the consequences of the theory in NDL correspond to the well-founded modelof the logic program. In this paper, we showed a similar result for ADL. Furthermore,we showed in this paper how to translate finite normal logic programs into defeasibletheories in such a way that the correspondence between the well-founded model ofthe program and the consequences of the defeasible theory in ADL are preserved. The correspondence between logic programs and defeasible theories seems to depend on thefact that ADL is ambiguity propagating rather than ambiguity blocking. The translationfrom defeasible theories to normal logic programs seems to us simpler and more directfor the case of ADL than NDL. Some might consider this a reason to prefer ADLover NDL. But different researchers have taken different positions on this issue, andour intuitions favor ambiguity blocking despite the closer correspondence of ADL withwell-founded semantics.
In Example 3, the two presumptions ⇒ p and ⇒ ¬p defeat each other, but in ADL ⇒ p and p ⇒ ¬q are still available to defeat the presumption ⇒ q, creating a "zom-bie path" (Makinson & Schechta, 1991), an argument path that has been "killed" bya defeater but that still has the power to defeat or "kill" other arguments. So we getD1 |∼NDL p and D1 ∼|NDL {p, ¬p, ¬q}, while we get D1 |∼ADL ∅ and D1 ∼|ADL ∅.
In the corresponding default theory, the intersection of all extensions was empty, agree-ing with ADL. Nevertheless, we think that lacking overriding reasons for acceptingeither p or ¬p, we should take neither into account when considering q, the approachtaken in NDL.
So far as positive consequences are concerned, Example 2 is handled in the same way by both NDL and ADL: we get neither D2 |∼NDL r nor D2 |∼ADL r. In bothsystems, the two presumptions ⇒ p and ⇒ q conflict because {p, q} is a conflict setin D2. We believe this is the correct result in examples of this sort. However, we getD2 ∼|NDL {p, q, r}, but D2 ∼|ADL ∅.
Our results for defeasible theories and logic programs assume that the theories and programs are finite, but they should also hold for theories that do not have infinite chainsof dependency. In a theory like D = {⇒ p, q1 ⇒ ¬p} ∪ {qi+1 ⇒ qi : i a positive integer }, C, ∅ our defeasible logics and well-founded semantics for logic programs diverge. Sinceproof trees in either NDL or ADL are finite, not even failure-by-looping will allow usto show that p is derivable in either system. However, p will be in the well-foundedmodel for the corresponding logic program. Suppose we admit semi-infinite proofs inNDL and ADL. A semi-infinite proof would be a tree all of whose infinite brancheshave a node n such that all descendants of n in the infinite branch are labeled withnegative defeasible assertions. We think that no additional conditions are needed forsemi-infinite proofs, but we have not investigated this problem further. The questionwhether the consequences of an infinite defeasible theory in such a system correspondsto the well-founded model for the corresponding infinite logic program is interesting inprincipal, but finite, constructive proof procedures for such theories and logic programswould in the general case not exist.
Translating defeasible theories into logic programs offers one way to implement NDL and ADL. Whether this or some more direct method for computing consequencesis the better method depends in large part on the cost of translating defeasible theoriesinto logic programs. We have not done a complete analysis of the complexity issuesyet, but at first glance it appears that when conflict sets are closed under strict rules,translating a defeasible theory into a logic program might require more than polynomialtime. This might not be so bad if the translation only had to be performed once or if the translation procedure were modular. If new facts are added to a defeasible theory, thenthese facts can be translated into an already existing program in linear time. But addingnew rules, and particularly new defeasible rules, looks like it will also require more thanpolynomial time. So in applications where new rules will not be added very often, thentranslation into a logic program seems to be a reasonable approach. The more oftennew rules, including new presumptions, are added to a theory, the less attractive thisapproach appears.
Antoniou, G., and Maher, M. J. 2002. Embedding defeasible logic into logic programs. In Antoniou, G.; Billington, D.; Governatori, G.; Maher, M. J.; and Rock, A. 2000. A family of defeasible reasoning logics and its implementation. In ECAI, 459-463.
Brewka, G. 2001. On the relationship between defeasible logic and well-founded semantics. In Emden, M. H. V., and Kowalski, R. 1976. The semantics of predicate logic as a programming language. Journal of the ACM 23:733-742.
Gelder, A. V.; Ross, K. A.; and Schlipf, J. 1988. Unfounded sets and well-founded semantics for general logic programs. In Proceedings 7th ACM Symposium on Principles of DatabaseSystems, 221-230.
Gelder, A. V.; Ross, K. A.; and Schlipf, J. 1991. The well-founded semantics for general logic programs. Journal of the ACM 221-23.
Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4:289-308.
Maier, F., and Nute, D. 2006. Relating defeasible logic to the well-founded semantics for normal logic programs. In Delgrande, J. P., and Schaub, T., eds., NMR.
Makinson, D., and Schechta, K. 1991. Floating conclusions and zombie paths: two deep difficul- ties in the 'directly skeptical' approach to inheritance nets. Artificial Intelligence 48:199-209.
Nute, D. 1992. Basic defeasible logic. In del Cerro, L. F., and Penttonen, M., eds., Intensional Logics for Programming. Oxford University Press. 125-154.
Nute, D. 1994. Defeasible logic. In Gabbay, D., and Hogger, C., eds., Handbook of Logic for Artificial Intelligence and Logic Programming, Vol. III. Oxford University Press. 353-395.
Nute, D. 1997. Apparent obligation. In Nute, D., ed., Defeasible Deontic Logic, Synthese Library.
Dordrecht, Netherlands: Kluwer Academic Publishers. 287-315.
Nute, D. 2001. Defeasible logic: Theory, implementation, and applications. In Proceedings of INAP 2001, 14th International Conference on Applications of Prolog, 87-114. Tokyo: IFComputer Japan.
Reiter, R. 1980. A logic for default reasoning. Artificial Intelligence 13:81-132.

Source: http://donald.nute.ws/Research/MaierNuteJelia06.pdf