Z3 证明：假设和引理规则总是干净嵌套吗？答案

【问题标题】：Z3 proofs: Are hypothesis and lemma rules always cleanly nested?Z3 证明：假设和引理规则总是干净嵌套吗？
【发布时间】：2015-04-28 18:47:24
【问题描述】：

快速问题：在 Z3 证明（例如 4.3.2）中，“假设”规则引入了局部假设，最终由“引理”规则解除。 “假设”和“引理”规则是否总是干净嵌套，这意味着可以将 Z3 证明映射到具有嵌套证明块的语言，或者可以有一个序列

hypothesis 1
hypothesis 2
lemma 1
lemma 2

？谢谢。

【问题讨论】：

4.3.2 在哪里？在 Z3 文档中？
@gsnedders：可能 4.3.2 是使用的 Z3 的版本号。
相关：stackoverflow.com/a/9115446/1959808

标签： z3 proofs

【解决方案1】：

您是对的，文档对此并不清楚。我将其更新为：

  \nicebox{
      T1: false
      [lemma T1]: (or (not l_1) ... (not l_n))
      }
      This proof object has one antecedent: a hypothetical proof for false.
      It converts the proof in a proof for (or (not l_1) ... (not l_n)),
      when T1 contains the open hypotheses: l_1, ..., l_n.
      The hypotheses are closed after an application of a lemma.
      Furthermore, there are no other open hypotheses in the subtree covered by
      the lemma.

【讨论】：