Automated Verification of Equivalence Properties in Advanced Logic Programs — Bachelor Thesis

要約

アンサーセット プログラミングを使用する産業用アプリケーションの増加に伴い、特に重要なアプリケーションに対する正式な検証ツールの必要性も高まっています。
プログラムの最適化プロセス中に、最適化されたサブプログラムが元のサブプログラムを置き換えることができるかどうかを自動的に検証できるツールがあることが望ましいでしょう。
形式的には、これは 2 つのプログラムの強い等価性を検証する問題に対応します。
そうするために、翻訳ツール anthem が開発されました。
これを古典論理の自動定理証明器と組み合わせて使用​​すると、2 つのプログラムが強く同等であることを検証できます。
現在のバージョンの国歌では、入力言語が制限されている肯定的なプログラムの強い同等性のみを検証できます。
これは、anthem に実装されている変換 $\tau^*$ の結果であり、here and there の論理で式を生成します。これは、ポジティブなプログラムの場合にのみ古典的な論理と一致します。
この論文は、これらの制限を克服するために国歌を拡張します。
まず、変換 $\sigma^*$ が提示されます。これは、式をあちこちの論理から古典論理に変換します。
定理は、古典論理におけるあちこちの論理における等価性を表現するために $\sigma^*$ をどのように使用できるかを形式化します。
第 2 に、変換 $\tau^*$ はプールを含むプログラムに拡張されます。
別の定理は、古典論理における 2 つのプログラムの強い等価性を表現するために $\sigma^*$ を $\tau^*$ とどのように組み合わせることができるかを示しています。
$\sigma^*$ と拡張 $\tau^*$ を使用すると、否定、単純な選択、プールを含む論理プログラムの強い等価性を表現できます。
拡張された $\tau^*$ と $\sigma^*$ は両方とも、新しいバージョンの anthem に実装されています。
プール、否定、単純な選択ルールを含む論理プログラムの例がいくつか示されており、新しいバージョンの国歌は古典論理に変換できます。
いくつかの…

要約(オリジナル)

With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. Formally this corresponds to the problem of verifying the strong equivalence of two programs. In order to do so, the translation tool anthem was developed. It can be used in conjunction with an automated theorem prover for classical logic to verify that two programs are strongly equivalent. With the current version of anthem, only the strong equivalence of positive programs with a restricted input language can be verified. This is a result of the translation $\tau^*$ implemented in anthem that produces formulas in the logic of here-and-there, which coincides with classical logic only for positive programs. This thesis extends anthem in order to overcome these limitations. First, the transformation $\sigma^*$ is presented, which transforms formulas from the logic of here-and-there to classical logic. A theorem formalises how $\sigma^*$ can be used to express equivalence in the logic of here-and-there in classical logic. Second, the translation $\tau^*$ is extended to programs containing pools. Another theorem shows how $\sigma^*$ can be combined with $\tau^*$ to express the strong equivalence of two programs in classical logic. With $\sigma^*$ and the extended $\tau^*$, it is possible to express the strong equivalence of logic programs containing negation, simple choices, and pools. Both the extended $\tau^*$ and $\sigma^*$ are implemented in a new version of anthem. Several examples of logic programs containing pools, negation, and simple choice rules, which the new version of anthem can translate to classical logic, are presented. Some a…

arxiv情報

提供元, 利用サービス

arxiv.jp, Google