anthem 1

國歌

將答案集程式翻譯為一階定理證明語言

該項目的現狀

筆記

您目前正在查看anthem的版本 1，該版本由 Patrick Lühne 構建，不再開發。不會對該儲存庫進行進一步的提交。

如果您對最新版本的國歌感興趣，請查看新的儲存庫。

概述

anthem將 ASP 程式（使用clingo的輸入語言）翻譯為一階定理證明器的語言，例如 Prover9。

用法

若要驗證程式是否實作了規範，請使用verify-program指令呼叫anthem ：

 $ anthem verify-program <程式文件> <規格文件>...

請注意，可以指定多個規範文件。這對於將引理和公理與假設和規範分開非常有用。

計算數字平方根下限的範例可以重現如下：

 $ 國歌驗證程式範例/example-2.{lp,spec,lemmas}

大括號表示法是 Bash 的簡寫

$ 國歌驗證程式範例/example-2.lp 範例/example-2.spec 範例/example-2.lemmas

預設情況下， anthem對翻譯後的公式執行 Clark 補全，偵測哪些變數是整數，並透過應用幾個基本轉換規則來簡化輸出。

可以使用選項--no-complete 、 --no-simplify和--no-detect-integers關閉這些處理步驟。

大樓

anthem是使用 Rust 的cargo工具鏈建構的。安裝 Rust 後，可以如下建造anthem ：

 $ git 克隆 https://github.com/potassco/anthem.git
$ CD國歌
$ 貨物建構--發布

然後， anthem二進位檔案將在target/release/目錄中可用。或者，可以使用cargo調用anthem ，如下所示：

 $ Cargo run -- verify-program <程式檔案> <規格檔>...

貢獻者

• 派崔克·呂內