Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs. Under consideration for publication in Theory and Practice of Logic Programming

翻译：程序完备化是将逻辑程序语言翻译为一阶理论语言的一种方法。其原始定义已被扩展至包含整数算术、接受输入，并区分输出谓词与辅助谓词的程序。对于紧程序，该完备化推广已知与稳定模型语义（即回答集编程的基础）相匹配。本文证明，该定理中的紧性条件可被更宽松的"局部紧性"要求替代。由此我们得出结论：证明助手anthem-p2p可用于验证局部紧程序之间的等价性。本文正在考虑发表于《逻辑编程理论与实践》。