Z3 证明中的命名断言 [英] Naming assertions in Z3 proofs

问题描述

是否可以在 Z3(版本 4.8.9)证明中获取断言名称?作为一个最小的例子:

Is it possible to get assertion names inside Z3 (version 4.8.9) proofs? As a minimal example:

(set-option :produce-proofs true)
(assert (! false :named name))
(check-sat)
(get-proof)

我想要以下输出:

unsat
((proof (asserted name)))

然而，这是实际输出:

unsat
((proof (asserted false)))

是否可以参考断言名称而不是实际公式来证明?

Is it possible to have the proof refering to the assertion names instead of the actual formula?

通过实验，我发现可以添加(set-option :unsat-core true).然而，这使得证明更加复杂.设置选项后，输出为:

Via experimenting, I found out that it is possible to add (set-option :unsat-core true). However, this makes the proof more complicated. With the option set, the output is:

unsat
((proof
(let (($x27 (not name)))
(let ((@x30 (mp (asserted (=> name false)) (rewrite (= (=> name false) $x27)) $x27)))
(unit-resolution @x30 (asserted name) false)))))

此外，我不确定是否允许同时启用证明和 unsat-core 生成，在 https://github.com/Z3Prover/z3/issues/189#issuecomment-129786093 NikolajBjorner 指出:

Also I am not sure if enabling proof and unsat-core generation simultaneously is allowed, in https://github.com/Z3Prover/z3/issues/189#issuecomment-129786093 NikolajBjorner states:

Z3 并不真正支持同步证明和核心生成，...

Z3 doesn't really support simultaneous proof and core generation, ...

推荐答案

这极不可能.名称几乎只用于 unsat-core 生成.z3 中的证明对象或多或少仍然是一个黑盒.但是，如果您将自己限制为仅使用位向量，它可能会更好地工作.请参阅:https://link.springer.com/chapter/10.1007/978-3-642-25379-9_15

This is extremely unlikely. Names are pretty much only used in unsat-core generation. Proof objects in z3 remain more or less a black-box. However, if you restrict yourself to only bit-vectors, it might work better. See: https://link.springer.com/chapter/10.1007/978-3-642-25379-9_15

这篇论文在这方面也很相关:http://homepage.divms.uiowa.edu/~ajreynol/lpar15.pdf.简而言之，BV 求解器通常将问题简化为命题推理，因此可以轻松地由外部工具检查的解析式证明更容易构建.但对于其他逻辑，尤其是当涉及到量词时，证明步骤可能相当不透明，重放将更加困难.

This paper is also quite relevant in this context: http://homepage.divms.uiowa.edu/~ajreynol/lpar15.pdf. In short, BV-solvers usually reduce the problem to propositional reasoning, and thus resolution-style proofs that can be easily checked by external tools are much easier to construct. But for other logics, and especially when quantifiers are involved, the proof steps can be rather opaque and replay will be much more difficult.

这篇关于Z3 证明中的命名断言的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！