Z3的反例输出

Question

当 Z3 中的公式不满足并且指定了 (get-proof) 时，会有一个输出，我找不到任何关于它是什么的信息。我在哪里可以找到有关这方面的任何文档？

在我看来很难理解，是否有任何工具可以将此作为输入？

干杯， 马特

Answer 1

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

1. Isabelle 交互式定理证明器：Z3 证明是在 Isabelle 内部使用可信核心重建的。你可以在Sascha Bohme's homepage找到几篇描述这项工作和 Z3 证明格式的论文

2. Generation of interpolants

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