Z3的反例输出

Question

当Z3中的公式不饱和并且(防止出现)时,有一个输出,我找不到任何关于它是什么的信息.我在哪里可以找到有关它的任何文件？

在我看来相当难以理解,是否有可能将此作为输入的工具？

干杯,马特

Answer 1

Z3产生的"证据"不适合人类消费.该文件描述了该格式的过时版本:Proofs and Refutations和Z3.该z3_api.h文件对每个证明规则都有很长的描述.证明规则标识符以Z3_OP_PR.开头.我知道有两个使用Z3校对对象的应用程序.以下论文包含大量示例,并描述了如何使用证明对象.

1. Isabelle Interactive Theorem Prover:使用可靠的核心在Isabelle内部重建Z3样张.您可以在Sascha Bohme的主页上找到几篇描述这项工作和Z3证明格式的论文

2. 生成插值

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