本文研究了具有(抽象的)约束原子的逻辑程序的稳定模型语义及其性质,并提出了简洁的抽象表示方法,该方法可以将稳定模型泛化到任意的约束原子逻辑程序中。我们还展示了如何通过这个抽象表示方法来推广现有的方法,并进一步扩展了用于普通原子逻辑程序的标准特征和性质。
Apr, 2009
通过扩展正常逻辑编程的概念和结果,我们研究了具有单调和凸约束条件的程序的性质,这些结果为一些最近扩展的逻辑编程提供了抽象的概述,并应用这些结果进一步提出了通过伪布尔约束的通用求解器计算lparse程序稳定模型的方法,这种方法通常比smodels系统更快。
Sep, 2011
研究答案集编程中的模块化问题,定义DLP函数和模块定理,介绍了DLP函数的分解方法和模块等价性概念。
Jan, 2014
研究了一阶稳定模型语义与一阶循环公式之间的精确关系,探讨了扩展一阶循环公式定于来便于比较,给出一个带显式量化符号的逻辑程序扩展语法,这允许我们使用一阶推理器进行涉及非-Herbrand稳定模型的推理。
本研究提出了一种新的、基于模型理论的方法来确定 Logic Programs with Ordered Disjunction (LPODs) 中最受欢迎的模型,从而克服了现有语义的不足。而且,新的方法可以用来定义一个包含有序和经典析取的自然类别的逻辑程序的语义,这使得程序不仅可以表达严格的优先级,还可以表达同样优先级的选择。
Aug, 2021
本文介绍了ANTHEM的应用,它是一种证明助手,可以用于验证答案集接口程序GRINGO的紧密性,并且与一阶公式的规范相关。它定义了局部紧密计划的概念,并证明了ANTHEM使用的验证过程可以在这更普遍的环境中应用。与紧密性不同,本地紧密条件允许某些递归形式,特别是描述动作效果的程序是局部紧密的。
Apr, 2022
稳定模型与变量的循环公式的关系,广义化循环公式至包括非零多项联结程序和任意一阶句子,并通过扩展逻辑程序的语法允许明确量词,将其语义定义为Ferraris等人提出的新稳定模型语言的子类,能在不依赖唯一名字和域封闭性假设的情况下处理非单调推理,同时由于受限的语法而产生更简洁的循环公式。此外,我们还展示了某些句法条件,使得扩展程序的查询回答可以简化为一阶逻辑的蕴涵检查,为使用一阶定理证明器推理非Herbrand稳定模型提供了一种途径。
Jul, 2023
本文通过使用大语言模型,探索了在自动程序验证中找到归纳循环不变量的新方法,并证明了其可以改进目前的技术水平。
Nov, 2023
通过对非平面ABA的扩展,我们建立了假设为LP中的不可行否定的稳定模型语义,以及在LP中的否定失效头部的集合稳定ABA语义之间的对应关系。
May, 2024
通过对逻辑编程领域中的回答集编程(ASP)进行分析,我们提出了一种精细化的方法,描述了ASP程序的特征,以及在一些情况下决策问题的半决策解法和用于生成有限扩展的基础步骤。