z3 证书是什么样子的？

Question

在 Extending Sledgehammer with SMT solvers 中，我找到了这句话：

Certificates make it possible to store Z3 proofs alongside Isabelle formalizations, allowing SMT proof replay without Z3. Only if the formalizations cahnge must the certificates be regenerated.

Z3 证书长什么样？它只是某种平衡树，其中存储了Z3中获得的推理步骤吗？

Answer 1

证书简单来说就是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 调用（无论你是手工编写还是使用 Sledgehammer 生成它），你都可以使用证书。但是，我不知道有人这样做。

z3 证书是什么样子的？

How does a z3 certificate look like?

z3

isabelle