z3 - Z3的反例输出

Question

当Z3中的公式不符合条件并且指定了(get-proof)时，会有一个输出，我找不到关于它的任何信息。在哪里可以找到有关此文件的任何文档？

在我看来，这是非常难以理解的，是否有任何工具可以将其作为输入？

干杯，
马特

Answer 1

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

Isabelle交互式定理证明:Z3证明是使用受信任核心在Isabelle内部重构的。您可以在Sascha Bohme's homepage上找到几篇描述此工作的论文和Z3证明格式。

Generation of interpolants
正如pad所言，unsat-cores更加易于使用。