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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google