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 <程序文件> <规范文件>...

贡献者

• 帕特里克·吕内