表記法で反復最大値を使用する正式な証明を Z3 に検証させようとしています。たとえば、fa 関数 (↑i: 0 ≤ i < N: f(i)) は、0 と N の間の値に適用されたときの f の最大値を指定します。次のようにうまく公理化できます。
(↑i: p(i): f(i)) ≤ x <=> (∀i: p(i): f(i) ≤ x)
i の型に対する pa 述語を使用します。Z3 でそのような量指定子を定義する方法はありますか?
証明を定式化するのに非常に便利なので、できるだけこの定義に近づけたいと思います。
ありがとう！
Z3 でそのようなバインダーを直接定義する方法はありません。Z3 は、古典的な単純に並べ替えられた一次論理に基づいており、唯一のバインダーは普遍的で出口的な量化です。特に、Z3 ではラムダ式を直接記述できません。ネストされた結合子を含む Z3 を使用して定理を証明するための 1 つのアプローチは、最初にラムダ リフティングを適用し、次に結果の一次定式化を証明しようとすることです。
あなたの例では、定数 max_p_f を定義したいと考えています。次のプロパティを使用します。
forall i: p(i) => max_p_f >= f(i)
(exists i: p(i) & max_p_f = f(i)) or (forall i . not p(i))
言う（ドメインで最高値が定義されていると仮定するなど）max関数を適用する各p、fの組み合わせに対して定数を作成する必要があります。
このような関数を定義することは、高階論理の証明アシスタントでは標準です。Isabelle の定理証明者は、証明義務を一次バックエンド (E、Vampire、Z3 など) にマッピングするときに、上記と同様の変換を適用します。