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可用于验证局部紧程序之间的等价性。本文投稿于《逻辑编程理论与实践》期刊审议中。