Argumentation Factory: Algorithms and Software for Industrial Strength Inconsistency Tolerance

人类在日常生活中不断地处理相互矛盾的信息，但直到最近，这个问题在很大程度上在计算中被避免了。基于数学思维，处理计算中的不一致性的正常方法是不容忍它。这可以通过任意删除相互矛盾的信息或求助于人为干预来实现。但是，随着计算机被推进到更智能的角色，需要更强的鲁棒性，不一致容忍在计算机科学的许多领域，包括人工智能、机器人、自然语言处理、数据库、信息系统和软件工程，是一个越来越重要的主题。不一致在世界上无处不在。因此，我们需要设计出能够解决普遍存在的不一致所带来的问题和机会的系统。论证理论的最新发展表明，论证系统的发展和应用可以为在广泛的应用中开发健壮的不一致容忍度提供重大的技术进步。论证是人类智能行为的一个重要方面。考虑到不同的专业人士，如政治家、记者、临床医生、科学家和管理人员，他们都需要整理和分析信息，在试图理解问题和做出决定时，寻找重要后果的利弊。因此，为专业人员的决策支持系统开发论证系统是一个有前途的领域。更一般地说，论证系统正越来越多地被考虑用于开发软件工程工具，用于构成协商和解决问题的多代理系统的重要组成部分，以及用于数据+知识融合。在这些类型的应用程序中，需要分析不一致的信息，找到相互矛盾的观点，并解决冲突。通过论证，我们可以确定某个命题是从某些假设中得出的，但是这些假设中的一个可以被我们前提中的其他假设推翻（或“削弱”）。通过这种方式，论证系统可以帮助我们分析哪些假设确实引起了不一致，哪些假设是无害的。论证系统可以用来从不一致的信息中得出论点，并将它们与反论点进行比较。因此，基于逻辑的论证理论有助于分析不一致，并且最近有令人印象深刻的研究进展。然而，论证在计算上是昂贵的，并且很少考虑如何有效地进行论证。因此，我们迫切需要开发算法和软件来生成论证和反论证的星座。为此，我们需要自动推理技术。然而，现有的自动推理并不是为寻找论证而设计的：它可以用来从一组前提中找到推理的证明。但它不是用来寻找最小一致的公式集来证明一些推理。此外，在生成实参和反实参时，对于实参的支持度，一致性检查和极小性检查的重新计算效率非常低。为了解决这些缺点，我们希望探索四个相互关联的研究方向：(1)开发算法和系统的原型实现，以利用现有的自动推理技术来提供蕴涵关系，作为构建论点过程的一部分；(2)开发知识库轮廓（引理生成的一种形式）的算法和原型实现；(3)编写知识库的算法和原型实现；(4)开发近似论证的算法和原型实现。

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, 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. 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. However, argumentation is computationally expensive, and little consideration has been given to how it can be done efficiently.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 a proof of an inference from a set of premises. But it is not intended for finding minimal consistent sets of formulae for proving some inference. Furthermore, with the generating arguments and counterarguments, there is much inefficient recomputation of consistency checks, and of minimality checks, for the supports of the arguments.To address these shortcomings, 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.