论文标题
用国歌和吸血鬼验证紧密的逻辑程序
Verifying Tight Logic Programs with anthem and Vampire
论文作者
论文摘要
本文继续进行研究旨在研究逻辑程序与一阶理论之间的关系。我们将程序完成的定义扩展到具有输入和输出的程序的定义，其中ASP接地器Gringo的输入语言子集，研究稳定模型与在这种情况下完成之间的关系，并通过使用两种软件工具（Anthem和Vampire）来描述初步实验，以验证具有输入和输出的程序的正确性。定理的证明是基于将本文研究的程序语义与稳定模型的一阶公式模型相关联的引理。正在考虑在TPLP中接受。
This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Under consideration for acceptance in TPLP.
