Oct, 2023

高级逻辑程序中等价性属性的自动验证 —— 学士论文

HTML
PDF
TL;DR使用Answer Set Programming的工业应用中，现对于关键应用来说，需求更多形式验证工具。本文提出的新版本的anthem工具能够扩展验证功能，通过强等价性来表示具有否定、简单选择和池的逻辑程序。
发现论文，激发创造
  • 关于Answer-Set Programming中强等价、一致等价和其它等价概念的共性视角

    本文提出一种参数化的等价概念，同时限制了规则头和规则体中允许出现的原子，该方法是用于逻辑编程中应对强等价和一般等价的一种新的实现方式。

    Dec, 2007

  • 具有命题连接词和聚合运算的逻辑程序

    提出了一种基于命题连词的比喻来定义aggregates的方法，可以在ASP范式下，对任意命题理论进行扩展，将aggregates定义为基础构造，并且结合了表达能力和简洁性。该定义还继承了关于具有嵌套表达式的程序的许多定理，例如强等价性和拆分定理。

    Dec, 2008

  • 发现强等价逻辑程序类

    本文应用计算机辅助定理发现技术，发现强等价逻辑程序在答案集语义下的定理，进而得到了新的程序化简规则。具体发现了关于规则和空集、两个规则、两个规则和其中一个规则、两个规则和另一个规则、以及三个规则和其中两个规则之间的强等价的确切条件。

    Oct, 2011

  • 关于Gringo语义学的研究

    该研究通过将答案集求解器转换为无穷命题公式的语言，解决了一些基于本质稳定模型定义的复杂结构，如局部变量、条件文字和聚合等，避免了纯手动的解释。

    Dec, 2013

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

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

    Jan, 2014

  • 逻辑程序之间的本质等价论证中的强等价和程序结构

    本文介绍了关于ASP中程序重写的正式结果，并提供了Projector系统的正确性证明，它可以对程序进行自动重写来提高效率。

    Jan, 2019

  • 使用Anthem和Vampire验证紧凑逻辑程序

    研究逻辑程序与一阶理论之间关系的论文，将程序完备性的定义扩展到具有一种程序翻译器中输入语言子集的输入和输出程序，研究了这种情况下稳定模型和完备性之间的关系，并描述了两个软件工具，anthem 和 vampire，用于验证具有输入和输出的程序的正确性。

    Aug, 2020

  • 本地紧凑程序的验证

    本文介绍了ANTHEM的应用，它是一种证明助手，可以用于验证答案集接口程序GRINGO的紧密性，并且与一阶公式的规范相关。它定义了局部紧密计划的概念，并证明了ANTHEM使用的验证过程可以在这更普遍的环境中应用。与紧密性不同，本地紧密条件允许某些递归形式，特别是描述动作效果的程序是局部紧密的。

    Apr, 2022

  • 有序析取逻辑程序的强等价性：一个逻辑角度

    本文在四价逻辑中提出了逻辑程序的强等价的纯逻辑特征，并证明了该等价性的coNP完备性。

    May, 2022

  • 关于逻辑编程与SETAF等价性的研究

    该论文将Normal Logic Programs（NLPs）和Sets of Attacking Arguments（SETAF）互相转换，并证明了它们在语义上的等价性，特别是L-stable和semi-stable semantics的等价性。此外，论文还证明了Redundancy-Free Atomic Logic Programs（RFALPs）是与NLPs等价的，并通过一系列已知的程序转换对任何NLP进行了等价的RFALP转换。这些结果进一步加深了我们对NLPs和SETAFs本质上是相同形式的理解。

    Jul, 2024