z3证书的外观如何？

问题描述

在带有SMT求解器的扩展大锤中，我找到了这句话：

证书使存储Z3证明和Isabelle形式化成为可能，从而允许在没有Z3的情况下重播SMT证明。仅在形式化更改时才必须重新生成证书。

Z3证书的外观如何？是否只是某种平衡树，用于存储在Z3中获得的推理步骤？

解决方法

证书只是Z3产生的证明。这是一个示例（取自文件SMT_Examples.certs you can find in the Isabelle distribution）：

23f5eb3b530a4577da2f8947333286ff70ed557f 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x29 (exists ((?v0 A$) )(! (g$ ?v0) :qid k!7))
))
(let (($x30 (f$ $x29)))
(let (($x31 (=> $x30 true)))
(let (($x32 (not $x31)))
(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
(mp (asserted $x32) @x42 false))))))))

从本质上讲，Z3证明是结论为假的证明树，而不是平衡树。 paper by Sascha Böhme中描述了重构和证明格式。

请注意，Sledgehammer与证书无关。只要有smt呼叫（无论您是手工编写还是使用大锤制作），都可以使用证书。但是，我不知道有人这样做。

isabelle z3