6

当 Z3 中的公式未满足并指定(get-proof)时,会出现一个输出,我找不到任何关于它是什么的信息。我在哪里可以找到有关此的任何文档?

在我看来,这很不可读,是否有任何工具可以将此作为输入?

干杯,马特

4

1 回答 1

8

Z3制作的“证明”不供人食用。论文中描述了该格式的过时版本:Proofs and Refutations 和 Z3。该z3_api.h文件对每个证明规则都有详细的描述。证明规则标识符以Z3_OP_PR. 我知道两个使用 Z3 证明对象的应用程序。以下论文包含大量示例,并描述了如何使用证明对象。

  1. Isabelle 交互式定理证明器:Z3 证明在 Isabelle 内部使用可信核心重建。您可以在Sascha Bohme 的主页上找到几篇描述这项工作和 Z3 证明格式的论文

  2. 插值的生成

    正如pad所说,unsat-cores使用起来要简单得多。

于 2012-02-02T15:57:02.027 回答