形式论证中的抽象解释：关于抽象辩证框架与May-Must论证的伽罗瓦连接（首次报告）
计算机科学中的逻辑
2020-07-27 v1 人工智能
摘要
基于标记的形式论证依赖于标记函数，这些函数通常为每个论证分配3个标签之一，以表示接受、拒绝或未定。虽然经典的基于标记的方法对如何标记一个论证施加全局统一的条件，但这些条件可以更局部地针对每个论证来确定。抽象辩证框架（ADF）是一种属于此范畴的著名论证形式化方法，提供了更大的标记灵活性。然而，随着论证在论证数量和论证间关系上的规模增大，检查一个标记函数是否满足那些局部条件，甚至这些条件是否符合指定者的意图，其成本变得越来越高。因此，对更大规模的论证进行推理需要某种折衷。在此背景下，最近提出了一种称为may-must论证（MMA）的形式化方法，它强制执行仍然局部但更抽象的标记条件。我们在这项工作中确定了它们之间的联系。我们证明了它们之间存在一个伽罗瓦连接，其中ADF是MMA的具体化，而MMA是ADF的抽象。我们探索了在形式论证中起作用的抽象解释的后果，展示了从MMA内部对ADF中可接受性/可拒绝性判断的可靠推理。据我们所知，文献中很少有将抽象解释纳入形式论证的工作，并且，在上述背景下，这项工作是首次展示其用途和相关性。
引用
@article{arxiv.2007.12474,
title = {Abstract Interpretation in Formal Argumentation: with a Galois Connection for Abstract Dialectical Frameworks and May-Must Argumentation (First Report)},
author = {Ryuta Arisaka and Takayuki Ito},
journal= {arXiv preprint arXiv:2007.12474},
year = {2020}
}