关于带变量的环式公式

Jul, 2023

On Loop Formulas with Variables

Joohyung Lee, Yunsong Meng

TL;DR稳定模型与变量的循环公式的关系，广义化循环公式至包括非零多项联结程序和任意一阶句子，并通过扩展逻辑程序的语法允许明确量词，将其语义定义为 Ferraris 等人提出的新稳定模型语言的子类，能在不依赖唯一名字和域封闭性假设的情况下处理非单调推理，同时由于受限的语法而产生更简洁的循环公式。此外，我们还展示了某些句法条件，使得扩展程序的查询回答可以简化为一阶逻辑的蕴涵检查，为使用一阶定理证明器推理非 Herbrand 稳定模型提供了一种途径。

Abstract

Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding, which applies to the syntax of arbitrary first-order sentences. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang, and generalize their loop formulas to →

stable models loop formulas disjunctive programs quantifiers nonmonotonic reasoning

发现论文，激发创造

一阶稳定模型语义与一阶环公式

研究了一阶稳定模型语义与一阶循环公式之间的精确关系，探讨了扩展一阶循环公式定于来便于比较，给出一个带显式量化符号的逻辑程序扩展语法，这允许我们使用一阶推理器进行涉及非 - Herbrand 稳定模型的推理。

Jan, 2014

稳定模型与一种替代逻辑编程范式

通过稳定模型语义重新审视逻辑编程在约束满足问题中的角色定义，提出一种函数符号被消除的新型逻辑编程系统，基于约束来描述问题的解决方案。该方法具有良好的应用范围、有力的计算算法和新型编程方法。

Sep, 1998

非分层逻辑程序的稳定模型存在性

该论文介绍了一个基础性的结果，给出了一种稳定模型的存在条件的句法特征表示，利用引入新的规范形式和循环依赖来定义稳定模型元语，从而保证了稳定模型存在的确定性。

Dec, 2004

具有外延原子的无限公式的稳定模型

该论文通过将内涵和外延原子区分，并将一阶公式的对称分裂定理推广到无穷公式，增强了无穷析取和合取命题的稳定模型定义，并用于推理。

Aug, 2016

关于逻辑程序的基本环路

本文研究了基本环的性质，特别是针对极大基本环与最小未建立集之间的关系。其中基于基本环定义，我们讨论了 Head-Elementary-loop-Free 程序的性质，该程序可以被转换成多项式时间的等价非不相交程序。在此基础上，我们讨论了基本环的识别问题在不同类型程序中的复杂度。

Dec, 2010

具有内涵函数的一阶稳定模型语义

通过引入引伸函数，扩展一阶稳定模型语义，并将其用作定义 Answer Set Programming Modulo Theories (ASPMT) 的基础，从而实现类似 SMT 的有效一阶推理，解决包含实数的领域中的接地问题。

Jul, 2023

带广义量词的逻辑程序稳定模型的两种新定义

本文提出了关于第一阶稳定模型语义及其通过引用重新定义泛化量词概念的替代定义，并将 FLP 稳定模型语义扩展到通过引用类似于 SM 运算符的运算符来允许使用广义量词。对于一定的逻辑程序语法类，本文证明了这两个广义量词的稳定模型语义是可交换的。

Jan, 2013

稳定模型的一般理论中的安全公式

在设计答案集求解器中，安全的一阶公式泛化了安全规则的概念。我们展示了任何安全的句子在某种意义上等价于其推理结果 - 通过将所有量词替换为多个合取和析取而得到的无变量句子。由此可知，安全句子以及其推理结果具有相同的稳定模型，并且可以通过一个简单的句法形式的公式来描述安全句子的稳定模型。

Jul, 2023

扩展和实现稳定模型语义

提出了一种用于计算逻辑程序稳定模型语义的算法，强调使用有效的实现技术，特别地，提出了一种展望的实现和一种通过最小化搜索空间来产生良好的启发式方法。结果表明，稳定模型语义的逻辑程序具有更紧凑的逻辑程序表示，因此在某些问题上比命题逻辑优越。

May, 2000

逻辑编程的基本集合

提出了循环和循环公式的概念，证明了非不相交逻辑程序的答案集恰好是满足所有循环的 Clark 完成模型。简化和概括了基本循环的概念，并阐明了其作用。提出了基本集合的概念，对于非不相交程序几乎等价于基本循环的概念，但更简单，并且可以扩展到包含分离项的程序而不产生令人费解的结果。证明了 “相关” 部分的最大无根基本集合正好是非空的最小无根集合。提出了用于非不相交程序的基本集合的图论刻画，相对于 (Gebser & Schaub 2005) 提出的刻画更为简单。同时，对于分离项程序，决定一个基本集合的问题是 coNP 完备的。

Jul, 2023