Argumentation Factory
Algorithms and Software for Industrial Strength Inconsistency Tolerance
An EPSRC Funded Project (to start in autumn 2006 for 3 years)
For more information on the project, please contact
Anthony Hunter (University College London).
Summary
In this project, we want to develop the argumentation factory
as a software system that acts as a middle layer (or hub) between:
(1) knowledge resources such as available in relational databases,
logical knowledgebases, ontologies, and argumentbases
(marked up in for example the forthcoming Argument Interchange Format);
(2) existing automated theorem proving technology;
and
(3) diverse applictations of agumentation systems such as
for decision support,
for multi-agent negotiation,
for knowledge fusion, and
for software requirements engineering.
To realise this goal, we plan to extend and refine the theoretical foundations and algorithms for argumentation, and undertake theoretical and empirical evaluations of our proposals.
The main problem we will address is the inherent computational complexity involved in constructing arguments and counterarguments. Our approach will be to develop four avenues:
(1) Harness existing automated reasoning techology for constructing arguments and counterarguments;
(2) Compile knowledgebases for more efficient generation of arguments and counterarguments;
(3) Develop a technique called contouring for a form of ``lemma generation"
that is particular to the needs of argumentation;
and
(4) Undertake argumentation with approximate arguments and approximate counterarguments.
Background
Humans constantly deal with conflicting information in their
everyday lives, but until recently the problem has been largely
avoided in computing. Being based on mathematical thinking,
the normal approach to inconsistency in computing is
to not tolerate it. This is done either by arbitrary removal of
conflicting information or by recourse to human intervention.
But as computers are being pushed into more intelligent roles
with the need for greater robustness, there is an increasing
recognition that we need to develop our response to inconsistency.
As a result, inconsistency tolerance
is an increasingly important topic in many areas of computer
science including artificial intelligence, robotics, natural
language processing, databases, information systems, and
software engineering. Inconsistency is omnipresent in the
world. So we need to design systems that can address the
problems and the opportunities raised by the widespread existence
of inconsistency. By better understanding the nature of
inconsistency, in particular, by developing industrial strength technology for analysing
inconsistency in data and knowledge, we can tackle these challenges.
Recent developments in the theory of argumentation are
suggesting that the development and application of argumentation systems could
offer a significant technological advance in the development
of robust inconsistency tolerance in a wide range of applications.
Argumentation is a vital aspect of intelligent behaviour by humans.
Consider diverse professionals such as politicians, journalists, clinicians,
scientists, and administrators, who all need to collate and analyse
information looking for pros and cons for consequences of importance
when attempting to understand problems and make decisions.
Hence, the development of argumentation systems for decision-support systems
for professionals is a promising area.
More generally, argumentation systems are increasingly being considered
for applications in developing software engineering tools,
for constituting an important component of multi-agent systems
for negotiation and problem solving,
and for data + knowledge fusion.
In these kinds of application there is a need to analyse inconsistent information,
find competing viewpoints, and resolve conflicts.
By argumentation, we can determine that a certain proposition follows from certain
assumptions but that one of these assumptions could be disproved
(or ‘undercut’) by other assumptions in our premises.
In this way an argumentation system could help us analyse
which assumptions were really giving rise the inconsistency
and which assumptions were harmless. Argumentation systems
can be used to draw arguments from inconsistent information,
and to compare them with counterarguments.
The theory of logic-based argumentation is therefore helpful
in analysing inconsistency and there have been impressive research advances
recently.
There are a number of proposals for logic-based formalisations
of argumentation.
These proposals allow for the representation of arguments for and against some conclusion,
and for attack relationships between arguments.
In a number of key examples of argumentation systems,
an argument is a pair where the
first item in the pair is a minimal consistent set of formulae
that proves the second item which is a formula.
Furthermore, in these approaches, the notion of attack is a form of undercut,
where one argument undercuts another arguments
when the conclusion of the first argument negates the premises of the second argument.
A limitation to the application of argumentation systems is that
there has been relatively little effort directed to implementations
of these systems. Part of the reason for this is that
argumentation incorporates computationally expensive reasoning
that involves some form of consistency checking
as well as finding a minimal set of premises that entail the conclusion of the argument.
In this project, we will develop viable algorithms for
constructing constellations of arguments and counterarguments.
Suppose we need to look for undercuts to an argument, and by recursion, we look for undercuts to undercuts. We wish to find all these arguments. This means a pruning strategy, such as incorporated into defeasible logic programming, would not meet our requirements since some undercuts would not be obtained, and the resulting constellation would be incomplete.
Let us start by considering the construction of individual arguments. If K is a knowledgebase, and we are interested in a consequent p, can we find an argument (X,p) where X is a subset of K. Deciding whether a set of propositional classical formulae is classically consistent is an NP-complete decision problem and deciding whether a set of propositional formulae classically entails a given formula is a co-NP-complete decision problem. However, if we consider the problem as an abduction problem, where we seek the existence of a minimal subset of a set of formulae that implies the consequent, then the problem is in the second level of the polynomial hierarchy. Even worse deciding whether a set of first-order classical formulae is consistent is an undecidable decision problem. So even finding the basic units of argumentation is computationally challenging.
Proof procedures and algorithms have been developed for finding preferred arguments from a knowledgebase following for example Dung's preferred semantics.
However, these techniques and analyses do not offer any ways of ameliorating the computational complexity inherent in finding arguments and counterarguments even though it is a significant source of computational inefficiency.
We therefore have a pressing need to develop algorithms and software for generating constellations of arguments and counterarguments. For this, we need automated reasoning technology. However, existing automated reasoning is not designed for finding arguments: It can be used to find proofs of consequents from a set of premises. But it is not intended for finding minimal sets of formulae for formulae.
To address this shortcoming, we want to explore four inter-connected lines of research:
(1) Develop algorithms and prototype implementation of system
for harnessing existing automated reasoning technology
for providing the entailment relation as part of the process of constructing arguments;
(2) Develop algorithms and prototype implementation
for contouring (a form of lemma generation) of knowledgebases;
(3) Develop algorithms and prototype implementation for compilation of knowledgebases; and
(4) Develop algorithms and prototype implementation for approximate argumentation.
Even if we have viable algorithms for arguments and counterarguments
there may be further computational expense required for argumentation.
Argumentation with classical formulae allows for a constellation
of conflicting perspectives to be presented to a user. Naive arrangement
of arguments, just in terms of rebuttal and undercut
relationships, normally leads to an overwhelming amount
of information being presented to the user. We have been developing formal techniques
for restricting the number and nature of the arguments
being presented to the user. Criteria that we have explored
so far include the believability of the arguments, and the impact
of the arguments with respect to the a desideratabase [Hun04a, Hun04b].
In this research programme, we will develop algorithms and prototype software
for these and further criteria including
criteria based on information theory and on measures of
inconsistency.
We will integrate the modules implemented in the research programme, into an Argumentation Factory Prototype (see Figure 1). This will be a ``factory" for constructing constellations of arguments and counterarguments, together with annotations for believability, impact, and conflict, for applications. The prototype will be designed to be used by diverse applications that can harness the analysis of knowledgebases in terms of arguments and counterarguments. Whilst the research programme will be focused on classical logic, to ensure some generality in the development of the technology, there will be some flexibility to harness theorem provers for other logics within the prototype.
To illustrate how an application might use the Argumentation Factory, consider a requirement to build a medical decision-support system where pros and cons for a treatment plan are presented to a clinician. By using the Argumentation Factory, the decision-support system could be more robustly and quickly constructed by effectively sub-contracting all the argumentation to the Argumentation Factory and its associated automated reasoning technology. The developer of the medical decision-support systems could then concentrate on developing the necessary knowledge resources, and for interacting with the user.
Further reading