论文标题
验证本地紧密的程序
Verification of Locally Tight Programs
论文作者
论文摘要
程序完成是从逻辑程序的语言转换为一阶理论的语言。它的原始定义已扩展到包括整数算术，接受输入并区分输出谓词和辅助谓词的程序。对于紧密的程序，已知完成的概括可以匹配稳定的模型语义，这是答案集编程的基础。我们表明，该定理中的紧密条件可以被限制性较小的“本地紧密度”要求所取代。从这个事实中，我们得出的结论是，可以使用证明助手Anthem-P2P来验证本地紧密的程序之间的等价性。正在考虑逻辑编程理论和实践中的出版
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
