anthem 1

国歌

解答セット プログラムを一次定理証明言語に翻訳する

このプロジェクトの状況

注記

現在、 anthemのバージョン 1 を参照していますが、これは Patrick Lühne によって構築され、現在は開発されていません。このリポジトリへのこれ以上のコミットは行われません。

Anthem の最新バージョンに興味がある場合は、新しいリポジトリをご覧ください。

概要

anthem ASP プログラム ( clingoの入力言語) を Prover9 などの一次定理証明者の言語に翻訳します。

使用法

プログラムが仕様を実装していることを検証するには、 verify-programコマンドを使用してanthemを呼び出します。

 $ anthem verify-program <プログラム ファイル> <仕様ファイル>...

なお、指定ファイルは複数指定することも可能です。これは、補題や公理を仮定や仕様から分離するのに役立ちます。

数値の平方根の下限を計算する例は、次のように再現できます。

 $ anthem verify-program example/example-2.{lp,spec,lemmas}

中括弧表記は Bash の短縮形です。

 $ anthem verify-program 例/example-2.lp 例/example-2.spec 例/example-2.lemmas

デフォルトでは、 anthem翻訳された数式に対してクラーク補完を実行し、どの変数が整数であるかを検出し、いくつかの基本的な変換ルールを適用することで出力を簡素化します。

これらの処理ステップは、オプション--no-complete 、 --no-simplify 、および--no-detect-integersを使用してオフにできます。

建物

anthem Rust のcargoツールチェーンを使用して構築されています。 Rust をインストールした後、次のようにanthem構築できます。

 $ git clone https://github.com/potassco/anthem.git
$CDアンセム
$ カーゴビルド --リリース

anthemバイナリはtarget/release/ディレクトリで利用できるようになります。あるいは、次のようにcargoを使用してanthemを呼び出すこともできます。

 $ Cargo run -- verify-program <プログラム ファイル> <仕様ファイル>...

貢献者

• パトリック・リューネ