本文主要研究非单调逻辑编程中的强等价性,包括程序在加入其他语句后仍具有相同的答案集的重复强等价性,以及更自由的强等价性概念,其中实际的语句可以受到限制,同时考虑规则的相对概念和可满足性的计算复杂性。
Feb, 2005
本文提出了一个关于逻辑程序强等价的简化及直接的表征方法,并证明了该方法同样适用于 Niemela 和 Simons 的权重约束程序。同时,提供了一个可以自动推理逻辑程序强等价的编码方式。
Dec, 2003
本文介绍了关于 ASP 中程序重写的正式结果,并提供了 Projector 系统的正确性证明,它可以对程序进行自动重写来提高效率。
Jan, 2019
本文应用计算机辅助定理发现技术,发现强等价逻辑程序在答案集语义下的定理,进而得到了新的程序化简规则。具体发现了关于规则和空集、两个规则、两个规则和其中一个规则、两个规则和另一个规则、以及三个规则和其中两个规则之间的强等价的确切条件。
Oct, 2011
Answer Set Programming (ASP) 是一种基于规则的语言,用于知识表示和推理,研究了忘记、简化和相关概念的关联以及引入了一种新的相对等效概念,提供了相对简化的必要和充分条件,并介绍了结合投影和适度遗忘来获得相对简化的操作符。
Dec, 2023
本文探讨了命题理论在答案集语义下的一个性质(称为 Equilibrium Logic),即任何理论都可以重新表述为一个具有强等价性的模态逻辑规划,可能具有头部否定。我们提供了两个不同的证明:一个涉及语法变换,另一个从中间逻辑的反例开始构建程序。
Jan, 2007
本文提出了两种方法来定义任意类型抽像限制原子(c-atoms)的逻辑程序的答案集,这些定义泛化了正常逻辑程序的修正点和级别映射基础的答案集语义,其中包括四种不同的答案集定义,这四种在应用于正常逻辑程序时是相等的。
研究 ELP 模块的等价性以及如何使用一种新的特征来直接应用于最先进的 ELP 求解器,证明判定两个 ELP 的一致性在计算复杂性的多项式层级中是可行的。
Jul, 2019
该研究使用 Bartholomew 和 Lee 的函数稳定模型语义,提供了关于强否定的另一种描述方式,并表明非布尔内涵函数可以用强否定表示以计算函数稳定模型语义。
Dec, 2013
使用 Answer Set Programming 的工业应用中,现对于关键应用来说,需求更多形式验证工具。本文提出的新版本的 anthem 工具能够扩展验证功能,通过强等价性来表示具有否定、简单选择和池的逻辑程序。
Oct, 2023