基于增强序列演算和动态推导的逻辑论证方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）21-37www.elsevier.com/locate/entcs基于增强序列演算和动态推导的Ofer Arieli1特拉维夫大学计算机科学学院以色列特拉维夫克里斯蒂安·斯特拉瑟2德国波鸿鲁尔大学第二哲学研究所摘要近年来，基于逻辑的论证分析和评估方法得到了广泛的研究，产生了各种形式化的基于论证的推理方法。本文的目标是提供一个抽象的，证明理论的逻辑论证，其中参数表示的序列，参数之间的冲突表示的消元规则，并通过动态证明系统扩展标准的微积分的演绎。保留字：逻辑论证、逻辑演算、动态推导。1引言逻辑论证（有时称为演绎论证）是一种基于逻辑的方法，用于形式化辩论，分歧和蕴涵关系，以便从基于论证的设置中得出结论[8，17，18，20]。在这个上下文中的基本实体称为参数。一个论点是一对有限的公式集（Γ，支撑集）和一个公式（结论），用任意的命题语言表达，使得后者根据某种潜在的逻辑从前者得出。正如[1]和[4]中所指出的，这引起了与根岑的后继概念[ 13 ]相关联1电子邮件：oarieli@mta.ac.il。由以色列科学基金会资助（批准号：817/15）。2电子邮件：Christian. ruhr-uni-bochum.de。由亚历山大·冯·洪堡基金会和德国教育和研究部支持。http://dx.doi.org/10.1016/j.entcs.2016.06.0031571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。22O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21以形式为Γ的。因此，逻辑论证归结为对这些句法对象进行推理的形式化方法的阐述。基于序列的逻辑论证的证明理论研究的第一步在[3]中完成。在本文中，我们修改和扩展的工作。特别地，我们引入了一种改进的证明理论方法，并表明这种方法比[3]更适合于基于论证的推理（参见下面的注释5）。为此，在下一节中，我们将回顾一般的抽象论证和特别的（基于序列的）逻辑论证中的一些基本概念。然后，在第3节中，我们考虑从给定的基于序列的参数集合中得出结论的通用方法，该方法容忍不同的逻辑，语言和参数之间的攻击关系。这是通过引入动态证明的概念来实现的，动态证明的目的是在论证框架中阐明实际推理。与“标准”证明方法不同在第4节中，我们给出了一些演示，表明尽管动态推导具有非单调性，但仍然可以得出可靠的结论，这些结论忠实于手头逻辑论证框架的预期语义。这在第5节中得到了形式证明，其中讨论了底层蕴涵关系的几个性质，包括自反性和单调性的一些限制形式。最后，在第6节中，我们对未来的工作进行了简要的展望2预赛我们首先回顾[4]中定义的基于序列的论证的概念首先，我们回顾抽象论证框架的更一般的概念2.1论辩框架及其语义抽象论证框架是有向图，其中节点表示（抽象）参数，箭头表示参数之间的攻击，如下面定义的。定义2.1（抽象）论证框架 [11]是一对AF=Args，AttackArgs，其中Args是一组可枚举的元素，称为参数，Attack是Args上的二元关系，其实例称为攻击。给定一个论证框架，理解它的一个关键问题是确定什么样的论证组合（称为扩展）可以被集体接受。为此，我们回想起无冲突和防御的概念。定义2.2设AF=Args，Attack是一个论证框架，A∈Args是一个论证，EArgs是一组论证。我们说E攻击参数A，如果有一个参数B∈E攻击A（即，（B，A）∈Attack）。被E攻击的参数集记为E+。我们说E为O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2123A如果E攻击所有攻击A的论点。 我们用Def（E）表示由E所保护的所有元素的集合。如果集合E不攻击它的任何元素（即，E+E=），如果E是无冲突的，并且保护它的所有元素（即，E是完备的，如果它是可容许的，并且包含它所维护的所有参数（E=Def（E））。上面定义的要求表达了框架的每个合理扩展应该具有的基本属性。直觉上，一组参数是无冲突的，如果它的所有元素“可以站在一起”（因为它们不互相攻击），并且可能够通过自己成员的攻击来应对任何攻击（参见[5，6]）。接下来，我们回顾一些可接受性语义的论证框架。定义2.3[11]设AF=Args，Attack是一个论证框架。• Args的最小完备子集是AF的接地扩张，• Args的最大完全子集是AF的优选扩展，• 攻击Args\E中每个参数的Args的完全子集E是AF的稳定扩展。我们用Cmpl（AF）（分别为Grnd（AF），Prf（AF），Stbl（AF））表示AF的所有完备（分别为所有固定的、优选的、稳定的）扩张的集合。如[11]所示，一个论证框架总是有一个唯一的扎根扩展，但不一定是稳定扩展。如果确实存在稳定的扩展，那么它也是首选。考虑其他扩展，例如，在[5，6]中。例2.4考虑以下论证框架：DA B CE这里，{A}，{B}和{B，D}是容许集，除了{B}之外，它们都是完备集。固定的扩展名是，首选扩展名是{A}和{B，D}，稳定扩展名是{B，D}。2.2基于序列的论证框架当涉及到形式论证的具体应用时，对论证的结构和论证攻击的具体性质进行具体说明通常是有用的。如前所述，我们通过遵循[1，4]中介绍的基于网络的方法来这样做。通过这种方式，我们能够完全抽象出论证的概念，并将其完全建立在支持和结论之间的逻辑依赖关系上。此外，将参数视为序列允许24O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21结合成熟的证明理论方法，用于自动构造，识别和推理参数（参见[1，4]以获得进一步的证明）。在下文中，我们将用L表示任意命题语言。L中的原子公式用p、q、r表示，L中的任意公式集用S、T表示，有限公式集用Γ、Δ表示定义2.5语言L的（命题）逻辑是一对L=L，L，其中► 是L的（塔斯基）后果关系，即，公式集和L中的公式之间的二元关系，满足以下条件：复显性：如果ε∈ S，则S εε。单调性：如果S且S SJ，则Sj。传递性：如果S且SJ，φ，则S，SJφ。此外，我们将假设L是无穷的，也就是说：如果S是无穷的，则有一个有限的理论Γ是这样的，3我们假设语言L至少包含以下连接词：• a-否定<$，满足：p/<$$>p和<$p/<$p（对于每个原子p），4和• 一个-连词，满足：SφiS和Sφ。对于一个有限集合Γ，我们用Γ表示Γ中所有公式的合取2.2.1作为序列有几种方法可以定义一个论点的结构下一个定义来自这样一种理解，即相继式对于表示逻辑论证是有用的，因为它们可以被视为特定类型的判断（再次参见[1，4]）。定义2.6设L=L，L是命题逻辑，S是L-公式的集合• 一个L-公式（简称L-公式）是一个形式为Γ Δ的表达式，其中Γ和Δ是L-公式的有限集合，而是一个保留符号（不在L中）。• 一个L-变元是一个形式为Γ的L-变元，其中Γ。• 一个基于S的L-变元是一个L-变元Γ，其中Γ S。 所有基于S的L-自变量的集合记为ArgL（S）.注1：显然，对于某些（有限的）Γ<$S i<$S <$$>，Γ < $S ∈ArgL（S）。对序列（以及参数等）进行操作的证明系统称为递归演算[13]。这里考虑的微积分由以下形式的推理规则组成：（一）Γ 1 Δ 1.. . I n I n.Γ ⇒Δ3.最后一个性质被每一个具有适当证明系统的逻辑所满足，并且在下面的内容中将是有用的（参见，例如，注1）。[4]关于否定连接词应该满足的性质，没有普遍的一致意见（参见，例如，论文集[12]。本文中对否定连接词O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2125的要求是一个非常小的要求，取自[2，16]。26O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21公理：ψ⇒ψ结构规则：弱化：切割：逻辑规则：Γ ΔΓ，ΓJΔ， ΔJΓ1 Δ1，Γ2， Δ2Γ1， Γ2< $Δ1， Δ2[]Γ， Δ Γ， ΔΓ，， Δ[编辑]ΓΔ，Γ Δ，Γ⇒ Δ,ψ∧ϕ[编辑][编Γ， ΔΓ，Δ Γ，ΔΓ，Δ[]Δ，[]Γ，， Δ[<$]Γ，<$ ΔΓ ⇒Δ,ψ[]，Γ，π Δ在下文中，我们将说序列Γ i <$Δ i（i = 1，.，n）是上述规则的条件（或先决条件），而Γ Δ是它的结论。像往常一样，公理被视为没有条件的推理规则，即， 它们是形式为Γ Δ的规则。在后面我们通常会假设底层逻辑有一个可靠而完备的证明演算，即一个基于序列的证明系统C，使得ΓiΓ在C中是可证明的。例2.7在本文中，我们通常使用经典逻辑（CL）来进行论证。GentzenFig. 1. 证明系统LK2.2.2作为消除规则的不同的攻击关系已经在文献中被考虑用于逻辑论证框架（参见，例如，[8、14、17]）。在我们的例子中，攻击允许消除（或释放）序列。我们将用Γ/ππ表示 π Γππ的消去。或者，s表示s的消除。现在，排除规则（或攻击规则）具有与推理规则类似的形式，除了它的结论是一个条件的解除，即，这是一项形式如下的规则（二）Γ 1 Δ 1，.，I n I n.nΔn攻击规则的先决条件通常包括三个要素。帮助O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2127击败：[Def]Γ 1⇒ ψ1ψ⇒¬Γ1强势击败：[S-Def]Γ⇒¬ Γ Γ2⇒ψ21Γ2 /2012年2Γ2⇒ψ22Γ2/γ2直接击败：[D-Def]<$11<$<$$><$2，φ2Γ2，φ/φ2间接击败：[I-Def]Γ 1⇒ ψ1ψ⇒¬Γ1Γ2， Γ′2/γ22Γ2， Γ ′2，Γ′2，Γ ′2，Γ ′2强势正面击败：[SD-Def]Γ1<$φΓ2，φ2Γ2，φ/φ2间接强势击败：[SI-Def]Γ⇒ ¬rr2，r ′ 2，r′2，r′212Γ2，Γ′2/2012年底切：[Ucut]Γ1⇒ψ1ψ⇒¬Γ12¬ΓΓ2，Γ′222 1Γ2， Γ′2/γ2强底切：[S-Ucut]Γ⇒ ¬rr2，r ′ 2，r′2，r′212直接底切：[D-Ucut]强直接底切：[SD-Ucut]Γ2， Γ′2/γ2Γ1⇒ψ1ψ1⇒ ¬γ2<$γ212，γ22Γ2，γ2/γ2Γ1γ2Γ2，γ2γ2Γ2，γ2π/ π2标准底切：[C-Ucut]Γ1⇒ψ1ψ⇒¬Γ12¬Γ ⇒ψ2 1Γ2π/π2Γ2⇒ψ2反驳：[Reb]Γ1⇒ψ1ψ1⇒ ¬ψ2¬ψ2⇒ ψ1Γ2⇒ψ2Γ2/γ2强烈反驳：[S-Reb]第1000章击败反驳：【D-瑞布】还原击败反驳：[RD-Reb]间接反驳：[I-Reb]Γ1⇒ ¬ψ2Γ2⇒ψ2Γ2/γ2Γ1⇒ψ1ψ1⇒ ¬ψ2Γ2⇒ψ2Γ2π/π2Γ1⇒ψ1ψ2⇒ ¬ψ1Γ2⇒ψ2Γ2/γ2Γ1⇒ψ1ψ1⇒ϕψ2⇒ ¬ϕΓ2⇒ψ2Γ2/γ2为了让读者区分这些成分，我们将以某种顺序来写它们：规则先决条件中的第一个条件是“攻击”条件，规则先决条件中的最后一个条件是“被攻击”条件，其他先决条件是攻击的条件。在这种观点下，排除规则的结论就是对被攻击论点的排除例2.8图2列出了逻辑推理系统中的一些消元规则（另见[4]）。道义逻辑和规范推理的类似规则可以在[22]中找到。在本文中，我们将只探讨这些规则中的一小部分。我们参考[4，8，14，22]以进一步证明它们的有用性。图二. 序贯淘汰规则28O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）212.2.3论证背景与归纳逻辑框架我们现在结合序列和消除规则来定义相应的论证框架。为此，我们需要以下定义。定义2.9论证设置（简称设置）是一个三重S=<$L，C，A <$L，其中L=<$L，<$L是一个命题逻辑，C是L的一个可靠的完备的微积分，A是一组用L-序列表示的攻击规则定义2.10设S=L，C，A是一个设定，S是一组公式，θanL-取代（即L中的原子被L中的化学式取代）。• （1）形式的推理规则R是ArgL（S）-可应用的（对于S，关于θ），如果对每个1≤i≤n，θ（Γi）<$θ（Δi）是C-可证的.• 如果θ（Γ1）<$θ（Δ1）和θ（Γn）<$θ（Δn）在ArgL（S）中，并且对于每个1（p <$p）.5.p）pp. . .6.q公理注意，qq在这里最终导出。事实上，ArgCL（S1）中唯一可能攻击q或p，的形式，其中 在逻辑上等价于<$q，但是这些序列被以下的p 8[8]值得注意的是，qq的Ucut-attackers仍然可以在D的扩展中导出。然而，如上所述，根据定义3.8（c）中的条件（ii），它们不能用于消除qq。O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2133因此，上面的推导不能扩展到q <$q被消除的推导，因此S1|我的天就普普而言，情况完全不同。这是因为上面的推导可以通过以下元组扩展，从而消除了pp：7.<$p<$p公理8.p/pUcut，7，7，7，1p反过来，这个推导可以进一步扩展，得到对p的攻击：9.好吧好吧10.我...11.Ucut，1，9，10，7pp在最后的推导中，pp不再被消除然而，pp可以被pp再次攻击。或者，pp可以被形式为<$p的任何一个重新攻击，其中等价于<$p（例如，n=<$2n+1p，即，一个公式，其中p前面有奇数个否定）。因此，在这个推导的扩展中重新引入了p/p，同样地，也可以重新引入<$p<$p。因此，这两个序列都不是最终导出的。以类似的方式，任何基于S1的动态推导总是可以以这样的方式扩展，即ArgL（S1）中的所有结论为p的序列（分别为，p）被消除，因此S1|S1（分别为|∼ ¬p).一个矩阵的这种状态直观地被这样一个事实所证明，即虽然q与S1中的不一致性无关，因此它可以安全地从S1中得出，但S1关于p是矛盾的，因此p和<$p都不能从S1可靠地推导出来。例4.2让我们考虑前面例子的以下变化。底层设置与之前相同：S=CL，LK，Ucut，但现在我们采用p和q的合取：S1J={p<$q，<$p}。再次，虽然bothofpqp和p和p都是LK可导出的，p和p都不能根据S从S1J导出，因为，例如，第一个节点Ucut-attack另一个节点，并被节点<$p <$$>（p<$q）Ucut-attack（细节与例4.1中的非常相似）。然而，这一次q不是S-可从S1J导出的，因为尽管序列p_q_q_q和<$p，p_q_q_q也被LK-可导出的序列p_q_q（p_q）Ucut-attacked，并且不能被Ar_g_CL（S1J）中的序列永久地防御。9注4：最后两个例子特别表明，|它对syn很敏感，前提的策略形式：虽然S1（例4.1）和S1J（例4.2）是一个CL-等价，它们的S-结论不一样.这可以通过以下事实直观地证明：在S1J中，与S1中的k不同，q对于前提集合的不一致性不是中性的也被上述对p的Ucut-attack所反映）。实际上，语法敏感性[9]注意，Ar gCL（S1′）-序列p_q_p并不通过Ar gCL（S1′）-序列p_q_p 这种情况与例4.1中的情况不同，在例4.1中，qpp“阻止”了对q q的任何潜在的Ucut-attack，因为在例4.1中，⇒34O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21这在非单调推理中并不罕见。 Darwiche和Pearl的迭代信念修正假设[ 10 ]也暗示了同样的现象，因此，例如，如果推理机1因此，推理者2仍然相信q，而推理者1没有q成立的迹象。当考虑前提的最大相容子集时，会发生类似的现象：q位于S1的最大相容子集的交集中，而交集的最大组成的子集的fS1J是empty（也见[19]）。10例4.3考虑一个带有否定连接词<$（sop<$$>p和<$p/<$p）的逻辑，它不考虑双重否定引入（即，p/<$p），并假设直接击败（D-Def; 见图2）是唯一的攻击规则。 让S2={p，<$p，<$$>p，<$$>p，<$$><$p}.我们把si（i∈N）记为<$$> ip <$$>ip（其中<$0p=p）。 注意，通过自反性，si在任何完备微积分中都可证明。 的基本逻辑。现在，考虑以下证明元组的序列D1. s0公理2. S1公理3. S2公理4. S1D-Def，3，3，2S25. S3公理6. s0D-Def，2，2，1S17. S2D-Def，5，5，3S38. S4公理很容易证明D是一个有效的推导。 只使用元组9扩展它。s3D-Def，8，8，5s4得到一个简单的推导DJ，其中攻击者（s4）不被反击通过一个可接受的矩阵，但 DJ是不相干的，因为 s1∈Attack（ DJ）<$Elim（DJ）。[11]然而，请注意，D可以扩展到包含元组9的相干推导，只要后者与以下消除元组一起引入：10. S1D-Def，3，3，2S2事实上，D的扩展序列为是一个有效的推导。这证明了在定义3.8中需要一次引入多个消除现在让我们检查一下从S2最终可以导出什么。首先，根据D-Def，仅通过右侧为<$5p的序列来攻击序列4，但是由于双重否定引入不成立，因此这样的序列不可能在ArgL（S2）中。[10]当S1（或S1′）一致时，系统税收概念不再成立。 这是下面的第5.2条建议的后续内容。[11]这特别表明，定义3.8（c）中的两个条件是不相关的。O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2135因此，s4最终由上述推导导出，因此S2|4便士。此外，s3不能最终导出，因为导出它的任何派生都可以由形式为i，s3，D-Def，s4的元组扩展，这导致s3的消除。 因此，S2|3便士。反过来，由于s2的攻击者（s3）被消除并且无法恢复，因此s2最终导出，因此S2|好吧 类似的考虑表明，在这种情况下，|而S2|好吧注5最后一个例子强调了这里介绍的推导过程和[3]中考虑的推导过程之间的基本区别。虽然[3]中的过程允许重新引入序列，而不管它们是否被攻击，但在这里，可以在证明中引入序列的方式受到限制，并且它取决于已经引入的因此，例如，虽然根据[3]中的方法，可以在例4.3的动态推导的扩展中重新引入pp，但根据本形式主义，这是不可能的。因此，根据[3]，在例4.3中只有s4是最终可导的，而在我们的例子中，s2和s0也是最终可导的，尽管它们被攻击了。这允许更好地被s4反击，所以s2被5的一些性质|∼在这一节中，我们考虑由定义3.12的动态证明系统导出的蕴涵关系的一些性质。我们仍然用|∼ an arbitrary entailment relation that is covered by this definition.由于缺乏空间证明在这一节中被省略，并将出现在本文的扩展版本。关系|和我们开始与一些结果之间的关系的基础后果关系和相应的论证设置引起的蕴涵。在这些命题中我们提到一个蕴涵|由论证设置S=L，C，A和基本逻辑L = L，L所引起的一个逻辑。(i) 塔斯基推论关系可以被看作是特殊的S-蕴涵：命题5.1如果A = 0，则|两者重合。(ii) 的另一情况|下面是一个例子：命题5.2如果S相对于S是无冲突的（也就是说，在ArgL（S）中的元素之间没有A -攻击），则S|我的天啊。(iii) 总的来说，|比命题5.3如果S|然后是S。36O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21(iv) 命题5.3的逆命题对定理和定理保持规则成立：定义5.4上面（2）形式的消去规则R是定理保持的（关于逻辑L），如果不存在通过替换θ使θ（Γ n）= θ的R的应用。直觉上，如果一条规则不能用于攻击底层（基础）逻辑的定理，那么它就是定理保持的。图2中的Undercut和Defeat的各种变体是关于任何逻辑的定理保持规则的示例。命题5.5如果A仅由定理保持规则组成，则定理保持意味着：|好吧推论5.6如果A仅由定理保持规则组成，则（i）|C是弱健全的和完全的，|（也就是说，|C是C-可导的）。我 们 还 注 意 到 ， 基 础 逻 辑 的 某 些 属 性 是 由 |- 是 的 其 中 之 一 是 -paraconsideration[9]：命题5.7如果p是<$-次协调的（也就是说，存在原子p，q使得p，<$p/q），则|- 是的谨慎的回复正如第4节中的例子所示，一般来说，|不是自反的：即使然而，下一个命题和推论表明，|他谨慎地回复。命题5.8如果S是无约束的，则S|对所有的S∈ S都是推论5.9(i) 对于每一个使得{}在S中无约束的公式，我们有|好吧(ii) 对于每一个原子p，|好吧注6最后一个命题和推论中的条件确实是必需的。例如，如果|是由S=|好吧好吧限制单调性很显然，|它不是单调的。例如，推论5.9 p|而例4.1示出了p，<$p，q|好吧像反射性一样，单调性可以在特定情况下得到例如，如下面的命题5.12所示，当使用Undercut将不相关的信息添加到框架时，这些信息不应该干扰先前的推断。对于这个命题，我们首先用精确的术语定义“不相关信息”的O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）2137定义5.10设S是一组公式，而A是语言L中的公式。我们用原子（S）表示出现在S中（在公式的某个子公式中）的原子公式的集合。我们说S与相关，如果Atoms（S）Atoms（{}）=意味着S=。 一个非空集合S与一个（非空）集合T无关，如果S与T中的任何公式都不相关，即： Atoms（S）Atoms（T）=。定义5.11设L=L，是一个命题逻辑。 L -公式集S如果存在一个L-公式，使得S/ε。我们说L是一致的，如果S1是一致的，当S1，S2是一致的，S2是相容的，并且与S1无关。注7根据L-os-Suzsko定理[15]，一个有限的命题逻辑L，如果它有一个单一的特征矩阵，则它是一致的（另见[23]）。因此，经典逻辑和许多其他逻辑是一致的。命题5.12设S=L，C，{Ucut} L是一个其基逻辑L是uni-form的集合，且设|这就是归纳蕴涵。如果s1|S1和S2是与S1无关的公式的一个相容集，则S1，S2|好吧注8命题5.12的一个重要性质是当被攻击序列的前提被削弱时，Ucut-attacks被保持：如果Γj被Ucut-attacked，那么只要ΓJ包含Γ，Γj就被Ucut-attacked（被同一个攻击者）注9最后一个命题也适用于直接下切。在S2与{n}无关的附加条件下，该命题对反驳也成立6结论和今后的工作我们已经介绍了一个演绎推理方法与序列为基础的argu- mentation系统。其推导的非单调性质类似于其他上下文中的其他动态证明系统，例如自适应逻辑[7，21]。在我们的设置，证明过程中的推导步骤可以被视为一个对话，阐述实际（动态）推理的论证框架。 这一点，以及其他的机会，使用动态推导模仿常识推理，以及确切的关系，相关的语义，如那些诱导的Dung风格的形式主义，还应该在未来的工作中探索引用[1] O.阿列利逻辑论证的一种基于序列的表示。在Proc. CLIMASpringer，2013.[2] O. Arieli，A. Avron和A.扎曼斯基三值语义学框架下的极大和预极大次协调。Studia Logica，97（1）：31[3] O. Arieli和C.斯特拉瑟基于顺序的逻辑论证的动态推导。在Proc. COMMAIOS Press，2014.[4] O. Arieli和C.斯特拉瑟基于顺序的逻辑论证。Journal of Argument and Computation，6（1）：7338O. 阿里埃利角Straßer/Electronic Notes in Theoretical Computer Science 323（2016）21[5] P. Baroni，M. Caminada和M. 贾科明论证语