z3 - Z3 の証明: 仮説と補題の規則は常にきれいに入れ子になっていますか?

Question

簡単な質問: Z3 の証明 (例: 4.3.2) では、「仮説」規則によって局所的な仮定が導入され、最終的に「補題」規則によって解放されます。「仮説」と「補題」の規則は常にきれいにネストされていますか?つまり、Z3 証明をネストされた証明ブロックを持つ言語にマッピングできるか、シーケンスを持つことができますか?

hypothesis 1
hypothesis 2
lemma 1
lemma 2

? ありがとう。

Answer 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.