Defeasibility in Answer Set Programs via Argumentation Theories

Paper Title: 
Defeasibility in Answer Set Programs via Argumentation Theories
Authors: 
Hui Wan, Michael Kifer, Benjamin Grosof
Abstract: 
Defeasible reasoning has been studied extensively in the last two decades and many different and dissimilar approaches are currently on the table. This multitude of ideas has made the field hard to navigate and the different techniques hard to compare. Our earlier work on Logic Programming with Defaults and Argumentation Theories (LPDA) introduced a degree of unification into the approaches that rely on the well-founded semantics. The present work takes this idea further and introduces ASPDA (Answer Set Programs via Argumentation Theories) — a unifying framework for defeasibility of disjunctive logic programs under the Answer Set Programming (ASP). Since the well-founded and the answer set semantics underlie almost all existing approaches to defeasible reasoning in Logic Programming, LPDA and ASPDA together capture most of those approaches. In addition to ASPDA, we obtained a number of interesting and non-trivial results. First, we show that ASPDA is reducible to ordinary ASP programs. Second, we study reducibility of ASPDA to the non-disjunctive case and show that head-cycle-free ASPDA programs reduce to the non-disjunctive case—similarly to head-cycle-free ASP programs, but through a more complex transformation.We also shed light on the relationship between ASPDA and some of the earlier theories such as Defeasible Logic and LPDA.
Full PDF Version: 
Submission type: 
Full Paper
Responsible editor: 
Decision/Status: 
Major Revision
Reviews: 

Submission for RR2010 special issue.

Resubmission after a "reject and resubmit", now requesting "major revisions"

Second round reviews:

Solicited review by Wolfgang Faber:

I think the authors did a good job with the revision, which I would
recommend for acceptance now. I have just some minor observations to
be taken into account for the final version:

At the end of Definition 7, there is an explanation for when a
defeasible rule is true, and one of the possibilities is that "it is
defeated", but it has not been explained what that means, and it is
not straightforward to see from the definition. It should say that the
rule is defeated if $defeated(r,L_i) holds for all L_i.

In Definition 4, $defeated_{AT} should be a binary predicate, not unary.

p.8 will have the reducts of R -> will have any reducts of R

p.8 Theoren

I am not sure about the choice of fonts for several of the predicates:
For instance why are $definitely and $conflict set in different fonts?
I thought that you want to set $defeated in a different font, as it is
an "important" predicate and auxiliary predicates like $conflict in a
less bold font; but then I would have expected $definitely to be set
in the same font as $conflict. Adding some comment on the used fonts
would be very helpful.

Solicited review by Guido Governatori:

The authors failed to address several comments in my previous review. Accordingly, I cannot recommend acceptance of the paper. The paper has some interesting ideas, but the comparison with related work is not appropriate, and in some places is technically wrong.

Item 10 of the answer: AT^DL does not correspond to the defeasible logic of [1]. Consider the defeasible theory/program

@r1 b :- b.
@r2 not b :- not b.
@r3 c :- b
@r4 -c :- true.

overrides(r3,r4)

r3 is stronger than r4.

The logic of [1] fails to prove "-c", while, AT^DL has an answer set with {-c}.

$defeated(@r4,-c):- $overruled(@r4).

$overruled(@r4):- $conflict(@r4,@r3), $candidate(@r3), naf refuted(@r3).

$candidate(@r3):- body(@r3,b), b.

But "b" is false, thus $defeated(@r4,-c) is false, and thus I(-c)=true.

To make the example work you should consider the defeasible logic under well-founded semantics, i.e., the logic described in

inproceedings{DBLP:conf/aaai/MaherG99,
author = {Michael J. Maher and
Guido Governatori},
title = {A Semantic Decomposition of Defeasible Logics},
booktitle = {AAAI/IAAI},
year = {1999},
pages = {299-305},
ee = {http://www.aaai.org/Library/AAAI/1999/aaai99-044.php},
crossref = {DBLP:conf/aaai/1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

Item 11. It is not about criticizing Defeasible Logic for its limitations. It is not doing a fair comparison. Why don't you compare with the logic in Billington 2001? That logic admits disjunction in the head (and whether this corresponds to disjunctive logic programming as in ASP or logic with disjunction is totally another matter, somebody could argue that logical disjunction is wrong, or disjunctive logic programming is wrong. They could claim "wrongness" because they have different intuitions of what is disjunction). It there are no disjunctions and negations are atomic the logics of Billington 2001 and [1] are equivalent. For naf have you considered Theorem 5.1 of Antoniou Maher Billington 2000 (Defeasible Logic versus Logic Programming without Negation as Failure) stating essentially that adding naf to Defeasible Logic of [1] does not increase the expressive power.

About the concern of the ASP philosophy, a:-a plus the proposed transformation fails to prove "a" and "nafa". If you want to compare with ASP you have to take the logic of Maher and Governatori 1999 with the well-founded semantics. Where you get that "a" is false and "naf a" is true.

Also this point reinforces what I wrote that you have to do a much better comparison/analysis if you want to discuss sceptical and credulous reasoning (and the same for disjunction).

Item 12. I pointed out a paper where different variants that can handle different intuitions. So why don't you consider the variant of Defaesible Logic that handle such intuition? And also item 4 points out the there is a family of defeasible logic based on the same framework (based on meta-programs), and that different variants are taken by modifying some parameters. So you can take the right parameters and compare with the appropriate variants.

Item 13. No you don't. Please add the rules

nafloc1 neg nafloc(?s,?,?to):- loc(?s,?,?to).
nafloc2 nafloc(?s,?,?to):- true.

and replace

naf loc(?s,?,?to)

in the first @move rule with

nafaloc(?s,?,?to).

What do you get?

Item 14. Please add a comment on the meaning of the program, thus a readers can decide on the various proposed solution.

Solicited review by anonymous reviewer:

I believe the paper has been improved in this revision. I have checked the changes made in response to the comments of the reviews including my own.

I still have one comment regarding the response the authors gave to one of my observations. My comment was:

2. The use of the terminology of Argumentation Theory is not really appropriated. The main reason is that there is a different meaning currently in use by the researchers in Argumentation; nevertheless, this is not a real problem
because there is no risk of people getting confused.

and the response was:

[Answer]: We do not believe that this term can or should be restricted to one particular stream of work. Multiplicity of meanings is commonplace in CS and other sciences. The two senses are clearly related, however: our
argumentation theories are sets of arguments for arguing the defeat of LP rules. Dung et al., on the other hand, study the logic of argumentation itself.

I have to say that I disagree with the authors; the use of a terminology that is not used by a fully established community to express the same things, or to use the same terminology with different meaning, is inappropriate. If I write in my own language, or use your language in the wrong way, I am sure you will point out that to me (you might be thinking about doing so right now). That behavior is not helpful to the effort of making things as clear as possible for the reader who comes to this paper following its title. You clearly are talking about the same things the researchers in the area of argumentation are; so, why use an equivocal language?

First round reviews:

Solicited review by Wolfgang Faber:

This paper presents ASPDA. Essentially it is a generalization of the
logic programming variant ASP by defeasibility via so-called
argumentation theories. The argumentation theories are essentially
non-defeasible logic programs with predicates that have a special
meaning, most notably $defeated, which encodes defeasibility. Despite
the name, there is no apparent relationship to argumentation à la
Dung.

In contrast to other languages that allow for encoding of
defeasibility, this language is syntactically quite general. However,
this generality also allows for specifying argumentation theories, the
meaning of which is quite unclear (at least to me) and provides a
semantics for it, which may or may not be the intended
one. Unfortunately, this aspect is not discussed in the paper. Rather,
in the paper only two argumentation theories are discussed, which are
supposed to be fixed for large classes of programs.

I think there should be at least a discussion on what the semantics
does for programs like

@r a.
$defeated(handle(r,a)).

@r a.
$defeated(handle(r,a)) :- a.

@r a.
$defeated(handle(r,a)) :- naf a.

and similar. Even if these look like artifacts, they are valid
programs in the proposed language and the semantics given to them
should be justified. This is really something that should have been
done in the paper on LPDA already. I understand that in that paper a
different path was taken, in which "well-behaved" argumentation
theories are identified; however this is not mentioned in this paper.

Apart from this issue, the paper has some major errors. The first is a
rather crucial definitional problem. Definition 2 defines handles for
rules and their head literals. But then, when defining truth
valuations for defeasible rules in Definition 8, handle is used with a
rule head, which in general will be a disjunction and not a
literal. From the rest of the text, it seems that what is meant is
that for a rule to evaluate as true, either all head literals are
defeated or the rule implication is satisfied. This definition must be
repaired.

The second and main problem is that the reduction from ASPDA to ASP
does not appear to work for any program in which a rule is defeated,
thus Theorem 2 is incorrect for most interesting cases. In fact, the
reduction also does not work for Example 2 (used as the running
example). The problem is that according to Definition 14, (defeasible)
rules are deleted whenever head literals are deleted. This is not
properly reflected in the reduction, that is, when K is emptyset, a
rule with "empty head" (or rather a head with the neutral element of
disjunction, f) is created, which will not be satisfied. Also in the
proof of Theorem 2 this problem surfaces, since if K_0 = emptyset,
the rule is not in P_1, but some rule is present in P_2, contradicting
the statement at the end of the last-but-one paragraph of the proof of
Theorem 2. A solution might be to omit the creation of the rule for
K=emptyset, but I did not check whether everything works with this
modification.

Even if the reduction is fixed, the issue that it requires exponential
space remains. My feeling is that a reduction from ASPDA to ASP does
not have to require exponential space. Since there is no complexity
analysis in the paper, this remains my conjecture, but at the same
time the paper does not provide a justification for the exponential
behavior of the reduction. In general, I do not see why reasoning
tasks over stable models of ASPDA would be more complex than those
over ASP.

In the introduction but also at other points in the paper, it is
stated that defeasible reasoning in the presence of disjunctive
information has not been considered so far. I believe this depends on
what is meant precisely by "defeasible reasoning" - in a wide sense
this term encompasses nonmonotonic logics in general and of course
disjunctive information has been studied intensively in that
field. But also in a more narrow sense there are several studies of
formalisms that allow for disjunction and defeating, to quote just one
example:
Disjunctive logic programs with inheritance
F Buccafurri, W Faber, N Leone
Theory and Practice of Logic Programming 2 (3), 293-321

When looking at Fig. 1 I was wondering whether any pair of literals x
and neg x should automatically oppose each other (rather than having
to specify that explicitly) - does it make sense in some scenario to
not have them oppose each other?

At the beginning of section 3, syntactic and semantic differences are
mentioned. But it is not clear with respect to what.

I don't think that Lloyd's book is good reference for the "Lloyd-Topor
extensions" mentioned in footnote 1 (on p.4, there is another footnote
1 on p.1, which should be corrected). Why not cite directly John
W. Lloyd, Rodney W. Topor: Making Prolog more Expressive. JLP 1(3):
225-240 (1984)?

In footnote 1 it is stated that the definition is "easy to generalize
to allow Lloyd-Topor extensions". This would be fine if these
extensions are not used later in the paper; however, they are: the
result of the shifting does create disjunctions in rule bodies, which
is not described in the syntax, but are part of the only implicitly
mentioned Lloyd-Topor extensions. So either it should be described
what the extensions are and how to treat them or they should not be
used in the remainder of the paper.

Why is it so important that a rule tag is not a rule identifier? Does
this really make any difference? What does it mean if two completely
different rules have the same tag? This remained unclear to me
throughout the paper and should be explained (if it is really
important) or dropped.

It is not clear whether the Herbrand Base also contains neg neg A, neg
neg neg A etc.

In the 1st item of Definition 8, delete the second if. In the last
item, F can be a disjunction, but handles were defined for
literals. This leaves ambiguities and must be corrected.

Why do you use the term quotient and not reduct, as in I believe
almost all works on ASP? I suggest to align the terminology for
clarity.

In Definition 9, a model of an aspda is defined, but the next
definition is labelled Model of ASPDA. The difference is that in
Def. 9 no argumentation theory is considered. I suggest to improve the
terminology to make a clear difference between a program with and a
program without argumentation theory.

In Definition 12 and also others: If tags are removed, the program is,
strictly speaking, no longer in the syntax of Definition 1.

At the end of page 7, "If not such a" should become "If no such".

In the third paragraph of the proof for Theorem 3, the mentioned rule
may not exist (it is deleted if all head literals are defeated). Later
in the proof, I think some arguments are cut a little bit short, for
instance "By the definition of quotient ..." - here and in other
similar statements, it should not only be stated what can be
concluded, but rather why.

First sentence of section 4, delete first of and affects instead of
affect.

When discussing argumentation theories, sometimes it is stated that
some argumentation theory only supports certain classes of program. By
the definition of argumentation theries, restrictions like these are
not foreseen, so these restrictions are exogenous to the formalism. It
is also unclear why one has to formulate such restrictions, as a
semantics is defined for all programs, and not just those in the
"supported" classes. Does it mean that the semantics give unintuitive
results for unsupported programs? Are there other problems?

The third sentence of 4.1 needs rephrasing.

In Example 2: "the another", "if does".

In Example 3 it is stated that the result "curiously" stays the same
under the well-founded semantics. I don't think that this is curious,
I would have thought it strange if there would have been a difference
here.

In Example 5, the "facts" are literals.

I would refrain from calling [7] recent (it is from 2004).

"Delgrande's framework" would be Delgrande et al.'s framework or similar.

"Leone et al." would be Eiter et al.; it is strange to write that the
framework in this paper lacks a model theoretic semantics. It is
really an encoding in ASP for a couple of semantics of programs with
preferences. I don't see where one should define a odel theoretic
semantics there (the programs with preferences have model theoretic
semantics and the host language is not new and hass a model theoretic
semantics as well).

Summing up, I believe that the work has good potential, but the
problems outlined above need to be addressed in a major revision of
the paper.

Solicited review by Guido Governatori:

GENERAL COMMENTS

The paper investigates of the representation of defeasibility in Answer Set Programming (ASP) and stable semantics. This means, that for ASP programs are extended with disjunction in the head of rules.

The treatment of defeasibility is handle by what in the paper is called Argumentation Theory (or in other terms metaprograms), where the metaprograms are then interpreted according to various logic program semantics (stable or ASP), where the metaprograms use some predicates specific to defeasibility (defeated, overrides, opposes, and eventually others).

The idea of metaprogram is to offer an uniform treatment of defeasibility. It seems to me that the apporach could introduce even more fragmentation. One could "randomly" generate a metaprogram and then say that the result is an apporach to defeasible reasoning. The issue is that we have no ideas of what would be the meaning of the logic (and what are the intuitions supported by it).

In general the paper appears to be technically correct (there are a few issues to fix), but, it seems to me that the comparison with other apporaches is partisan and not objective.

SPECIFIC COMMENTS

Page 1, col 1: you mention that defeasibile reasoning has been successfully used to model various domains. Can you give references to works describing these applications?

Page 1, col 2: You mention [14,6] as works discussing how to compare apporches to defeasible reasoning, and then you mention other works (again you should give references).

Page 1, col 2: the framework proposed by Antoniou, Billington, Governatori and Maher can do what you specify in the second paragraph of col 2. In addition to [29].

Page 2, col 1: Defaesible reasoning and disjunction. You should consider the work by Billington on Plausible logic, e.g.,

@article{DBLP:journals/sLogica/BillingtonR01,
author = {David Billington and
Andrew Rock},
title = {Propositional Plausible Logic: Introduction and Implementation},
journal = {Studia Logica},
volume = {67},
number = {2},
year = {2001},
pages = {243-269},
ee = {http://dx.doi.org/10.1023/A:1010551204574},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

Also, you should ask why disjunction has not been considered for defeasible resoning. Typically defeasible reasoning is sceptical, and there are fundamental concpetual issues to behind this that must be addresses first.

Page 3, col 1: it is possible to introduce a new predicate corresponding to the disjunction in other approaches. Simply you have to blow the size of the theory. Also the approach with ordered disjunction can (partially) handle that.

Page 9, Definition 18: The expressions in (2) are not rules according to Definition 1. The body of a rule is a conjunction of literals, and naf L_i vee $defeated(handle(r,L_i) is a disjunction, not a literal.

A possible solution is to introduce dummy literals and rules for them, e.g.:

dummy_i :- naf L_i
dummy_i :- $defeated(handle(r,L_i))

Also I would write the rules in a more precise way:

@r L_i :- Body wedge bigwedge_{1leq jlen n, jneq i) naf L_j vee $defeated(handle(r,L_j)).

It seems to me that the result of Theorem 3 holds. But the proof should be adjusted (based on a revised Definition 18).

Page 9, col 2, first line of Section 4: Can you check the expression "introduce of two"?

Page 10, line 6 of Section 4.1: Can you check the sentence "It is this argumentation theory that implied in all the earlier examples in this paper."?

Page 11, col 2: The argumentation theory for Defeasible Logic works for well-founded/stable and answer set semantics, but it does not corresponds to Defeasible Logic as defined in [1]. Take for example the rules B => B and ~B => ~B. $candidate fails. But you cannot resolve the loop in the logic of [1]. You can do in the well-founded version:

Page 11, col 2, first bullet point: Defeasible logic with or without naf have the same expressive power.

@r_a neg nafa :- a
@r_nafa nafa :- true

#overrides(r_a,r_nafa)

See:
@article{DBLP:journals/jlp/AntoniouMB00,
author = {Grigoris Antoniou and
Michael J. Maher and
David Billington},
title = {Defeasible Logic versus Logic Programming without Negation
as Failure},
journal = {J. Log. Program.},
volume = {42},
number = {1},
year = {2000},
pages = {47-57},
ee = {http://dx.doi.org/10.1016/S0743-1066(99)00060-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

In addition I think it is not appropriate to compare a sceptical approach to a credulous approach.

Typically, the sceptical extension corresponds to the intersection of the credulous extensions (intersection of the answer sets). Thus given the program

a V b V c

there are 3 minimal models {a}, {b}, {c}, and the intersection is {}.

A better comparison would be with the logic of

@inproceedings{DBLP:conf/jelia/Billington08,
author = {David Billington},
title = {Propositional Clausal Defeasible Logic},
booktitle = {JELIA},
year = {2008},
pages = {34-47},
ee = {http://dx.doi.org/10.1007/978-3-540-87803-2_5},
crossref = {DBLP:conf/jelia/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/jelia/2008,
editor = {Steffen H{"o}lldobler and
Carsten Lutz and
Heinrich Wansing},
title = {Logics in Artificial Intelligence, 11th European Conference,
JELIA 2008, Dresden, Germany, September 28 - October 1,
2008. Proceedings},
booktitle = {JELIA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5293},
year = {2008},
isbn = {978-3-540-87802-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

or

@article{DBLP:journals/sLogica/BillingtonR01,
author = {David Billington and
Andrew Rock},
title = {Propositional Plausible Logic: Introduction and Implementation},
journal = {Studia Logica},
volume = {67},
number = {2},
year = {2001},
pages = {243-269},
ee = {http://dx.doi.org/10.1023/A:1010551204574},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

Page 11, col 2, last paragraph: There are several different variants of Defeasible logic (to capture different intuitions like the one you discuss here). See

@article{DBLP:journals/tocl/BillingtonAGM10,
author = {David Billington and
Grigoris Antoniou and
Guido Governatori and
Michael J. Maher},
title = {An inclusion theorem for defeasible logics},
journal = {ACM Trans. Comput. Log.},
volume = {12},
number = {1},
year = {2010},
pages = {6},
ee = {http://doi.acm.org/10.1145/1838552.1838558},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

Page 12, Example 4: See, again the previous comment on naf and Defeasible logic.

Page 5, Example 5: It seems to me that here there is a clash of intuition on what should be the correct answer.

A loop in the superiority relation represents an inconsistency in the factual knowledge of a theory/program. And defeasible logic output inconsistency in the the monotonic/factual part. Thus, I would say that not being able to derive the a, b might be a problem with A-GCLP.

However, I would say that this is a matter of intuition.

And in

@article{DBLP:journals/tocl/AntoniouBGM01,
author = {Grigoris Antoniou and
David Billington and
Guido Governatori and
Michael J. Maher},
title = {Representation results for defeasible logic},
journal = {ACM Trans. Comput. Log.},
volume = {2},
number = {2},
year = {2001},
pages = {255-287},
ee = {http://doi.acm.org/10.1145/371316.371517},
bibsource = {DBLP, http://dblp.uni-trier.de}
}

The theorem about consistency clearly states that if the superiority relation is cyclic there could be inconsistencies

Solicited review by anonymous reviewer:

This paper extends previous work of the authors on Logic Programming with Defaults and Argumentation Theories (LPDA). Here the authors present ASPDA where the system permits the use of disjunctive rules, and where defeasibility on the reasoning is obtained through the use of argumentation theories based on answer set programming (ASP). It is interesting to note that ASPDA can be reduced to ASP programs; the results of this reduction exhibit a substantial increase (exponential) in the computational cost associated with the ASP program. For the case for non-disjunctive aspda programs the increase in size is shown to be lineal. The relations between ASPDA and Defeasible Logic, and ASPDA and LPDA are discussed.

The presentation of the paper is good and the ideas are clearly introduced; the authors have included examples that help the reader to understand these ideas. It would be interesting to see an example where the elements being developed in the paper are meaningful to the reader. The abstract examples are fine for checking the definitions and exercising the formalism but convey little intuitive meaning. In particular, it would be interesting to see how the transformation from ASPDA to ASP programs keeps the meaning clear. The reference context is correct.

The content of this paper is closer to Nute's d-prolog and recent developments in defeasible logic than to modern views in argumentation. This comment is not an attempt to diminish the importance of this research, but to frame it in the right context. I am convinced that this work is important as a development in the area of Logic Programming extending the capabilities of current systems by integrating some of the ideas used in the argumentation community.

I believe that the paper could be published with the minor changes that I suggested before.

Minor comments:

The use of the terminology of Argumentation Theory is not really appropriated. The main reason is that there is a different meaning currently in use by the researchers in Argumentation; nevertheless, this is not a real problem because there is no risk of people getting confused.

Although the meaning is clear, it would be helpful to spell out the acronym ASPDA at the beginning of the paper.

Definition 6 has the tag Herbrand Universe, but in the definition Herbrand Base is also defined.

The first phrase at the beginning of Section 4 has a typo. I believe that the word "of" can be removed.

In the text of reference 13 there is a double comma after Lifschitz.

Tags: