z3 - Z3 を使用して 1 パラメーター グループの定理を証明する方法

Question

Z3 を使用すると、次のことを証明できます。

1 パラメータ グループを形成します。

証明は、次の Z3 コードを使用して実行されます。

(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)

対応する出力は次のとおりです。

sat
unsat
unsat
unsat
unsat

ここでコードをオンラインで実行してください。

その他の例: 証明する

1 パラメータ グループを形成します。

証明は、次の Z3 コードを使用して実行されます。

(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)

対応する出力は次のとおりです。

sat
unsat
unsat
unsat
unsat

ここでこのコードをオンラインで実行してください

その他の例：それを証明するために

1 パラメータ グループを形成します。

証明はここでオンラインで与えられ、4 次元拡張はここでオンラインで与えられます。

最後のいくつかの例:

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

証明してください

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

より一般的に、

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

1 つの 3 次元拡張: 証明する

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

双曲線関数を使用した例:

1 パラメータ グループを形成します。

証拠は ここでオンラインで提供されます

私の質問は次のとおりです。

1. 配列を使用して高次元の証明を作成することは可能ですか?

2. Z3 は、これらの証明を実行できる唯一のシステムであると主張します。同意しますか？