命题逻辑程序的连续分解
本文探讨了命题理论在答案集语义下的一个性质(称为 Equilibrium Logic),即任何理论都可以重新表述为一个具有强等价性的模态逻辑规划,可能具有头部否定。我们提供了两个不同的证明:一个涉及语法变换,另一个从中间逻辑的反例开始构建程序。
Jan, 2007
本文提出了一种多值扩展的逻辑程序,基于可靠模型语义,其中模型中的每个真实原子都与一组证明关联,在一个证明树的集合中类似,我们将证明捕捉到一个真值的代数中,该代数具有三个内部操作:加号表示公式的替代证明,可交换乘积表示导致的联合交互以及非交换积表示证明构造器。使用这种多值语义,我们得到了标准(非因果)逻辑程序的语法证明树与模型中每个真实原子的解释之间的一一对应关系,并且由于这种代数特征,我们可以检测到获得的证明的冗余性和相关性。我们还确定了此代数的基于格的特征,定义了直接后果算子,证明了其连续性,并证明其最小修复点可以在有限次迭代后计算。最后,我们通过引入类似于 Gelfond 和 Lifschitz 的程序削减的变换来定义因果稳定模型的概念。
Dec, 2013
我们提出了序列堆分离逻辑,将序列集成到堆操纵程序的逻辑推理中,该逻辑包括序列变量量词和存储序列的单例堆。我们研究了序列堆分离逻辑的两个片段的可满足性问题,并探讨了正前式正规形式的解释逻辑边界。
Jan, 2023
该研究将过渡系统用于计算命题公式的模型,证明了其适用于逻辑规划和 PC(ID)逻辑中,通过计算答案集表示的模型,提供了一种统一的视角,为不同命题形式开发的解决程序提供联系。
May, 2011
通过 Gaifman-Shapiro-style 模块架构和稳定模型语义来限制组合系统,提出一种正方案程序的模块化架构算法,并且取得了很好的效果,这也为实现程序性质讨论提供了理论基础和研究方法,对自动化组合和解析正规方案程序等方面都有非常重要的研究意义。
Sep, 2008
本文从不同角度探讨了非简洁逻辑规划的互补推理,通过稍微修改定义非简洁互补语义的一些方法,我们展示了一种直观的互补推理形式,并提供了一种自下而上的程序,从而阐明了不同方法之间的关系及其优缺点。
Jan, 2003
本文研究基于 Sato 分布语义的概率逻辑程序,分析了基于稳定和基于良基模型这两种语义,探讨了 credal 语义产生的概率模型集合是无限单调 Choquet 容量的结果产生的几个有用的结果,并研究了其推理和查询的复杂度。作者对此进行了详细说明,并对无环、分层、周期性的命题和关系程序,提出了推理和查询复杂度的结果,该复杂度达到各种计数层次和指数级别。
Jan, 2017
本文提出一种基于稳定模型语义的逻辑程序的多值扩展,其中每个模型中的真实原子都与一组证明相关联,这些证明是由规则标签形成的因果图表示它们的应用顺序而表达的。通过在因果值的格子上进行代数运算(乘积,和,应用),可以以纯粹语义的方式获得这种因果信息。对于带否定的程序,引入一种类似的转换来定义因果稳定模型。
Sep, 2014
本论文探讨否定作为失败的两种理论之间的关系:基于程序完成和基于稳定模型或答案集。研究表明,当一个逻辑程序满足一定的语法条件 (被称为 “紧密性”) 时,它的稳定模型可以被表征为其完成模型。本研究将 “紧密性” 的定义和 Fages 的定理扩展到规则体中包含嵌套表达式的程序,并研究包含谓词的传递闭包定义的紧致逻辑程序。
Feb, 2003