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.

翻译：本文延续了旨在研究逻辑程序与一阶理论之间关系的研究路线。我们将程序完备性定义扩展至ASP基层器gringo输入语言子集中具有输入和输出的程序，研究该语境下稳定模型与完备性之间的关系，并描述使用anthem和vampire这两个软件工具验证带有输入输出程序正确性的初步实验。定理证明基于一个引理，该引理将本文研究的程序语义与一阶公式的稳定模型联系起来。本文正在考虑被TPLP接收。