Z3证明中的命名断言

Question

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

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

我想要以下输出：

unsat
((proof (asserted name)))

然而，这是实际输出：

unsat
((proof (asserted false)))

有可能让证明引用断言名称而不是实际公式吗？

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

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

此外，我不确定是否允许在https://github.com/Z3Prover/z3/issues/189#issuecomment-129786093 NikolayBjorner州：

Z3并不真正支持同时证明和核心生成。。。

Answer 1

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

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