本文介绍了基于图的解释Answer Set编程的离线和在线证明方法，并将其集成到计算模型中用于调试Answer Set程序。

Dec, 2008

本文提出了一种多值扩展的逻辑程序，基于可靠模型语义，其中模型中的每个真实原子都与一组证明关联，在一个证明树的集合中类似，我们将证明捕捉到一个真值的代数中，该代数具有三个内部操作：加号表示公式的替代证明，可交换乘积表示导致的联合交互以及非交换积表示证明构造器。使用这种多值语义，我们得到了标准（非因果）逻辑程序的语法证明树与模型中每个真实原子的解释之间的一一对应关系，并且由于这种代数特征，我们可以检测到获得的证明的冗余性和相关性。我们还确定了此代数的基于格的特征，定义了直接后果算子，证明了其连续性，并证明其最小修复点可以在有限次迭代后计算。最后，我们通过引入类似于Gelfond和Lifschitz的程序削减的变换来定义因果稳定模型的概念。

Dec, 2013

本文提出一种基于稳定模型语义的逻辑程序的多值扩展，其中每个模型中的真实原子都与一组证明相关联，这些证明是由规则标签形成的因果图表示它们的应用顺序而表达的。通过在因果值的格子上进行代数运算（乘积，和，应用），可以以纯粹语义的方式获得这种因果信息。对于带否定的程序，引入一种类似的转换来定义因果稳定模型。

Sep, 2014

本文介绍了如何使用论证理论来解释为什么某个文字是或不是包含在给定答案集中，并定义了两种基于论证的方法：攻击树和 ABA-Based 答案集证明。

Nov, 2014

本文提出了一种基于逻辑编程的新方法，其中每个派生自良基模型的默认文字都与一个代表证明的代数表达式相关联，并包含启用或禁用因果规则的条件，这些条件分别称为“激活剂”和“抑制剂”，并与默认否定有紧密关联，本文通过一些例子进行了探讨。此外本文还比较了两种最近的LP证明方法：为什么不证明（WnP）和因果图（CG），表明当前方法在良基语义下扩展了WnP和CG证明，并建立了这两种方法之间的形式关系。

Feb, 2016

本文正式比较了两种基于规则的论证形式，DeLP和ASPIC+的一些中心概念，特别关注直观的充分性和可相互转换性、一致性和闭合性质。与攻击和论据的定义不同，DeLP的定义更具吸引力，但可能不完全符合严格闭合和间接一致性的理性假设。 针对一些特殊情况，DeLP的定义被证明比ASPIC+更好。最后证明了如果将DeLP确认程序更改为基于grounded语义，那么DeLP的warrant概念和ASPIC +的justification的概念是相等的，并为三种攻击定义的情况证明了这一结果。

Sep, 2019

本文研究辩解论理论在计算机科学中的应用，探究其与博弈论的关系，并研究了两种不同方言的辩解论理论（以图形和树形解释），以及建立了一个精确的标准来证明由辩解论理论引起的语义产生一致的结果。

Aug, 2020

本文介绍了一个用于定义基于规则语言的语义的普遍框架，即“justification theory”，并讨论了“nested justification systems”的概念，这允许模块化地定义规则语言的语义，从而增强了说明理论的表达能力。另外，本文提供了一种替代的“nested justification systems”的语义表征方式，并证明其与原来的语义表征方式等价，同时还讨论了如何利用“nested justification systems”表示fixpoint定义。

May, 2022

本文研究了包括树状结构和图形结构的证明理论，解决了其中树状结构中的一致性问题，揭示了其抽象的统一形式主义。

Aug, 2022

通过对非平面ABA的扩展，我们建立了假设为LP中的不可行否定的稳定模型语义，以及在LP中的否定失效头部的集合稳定ABA语义之间的对应关系。

May, 2024