z3 - 如何使用 Z3 证明单参数组的定理

Question

使用 Z3 可以证明

形成一个单参数组。

使用以下 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

请在此处在线运行代码。

其他例子：证明

形成一个单参数组。

使用以下 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

请在此处在线运行此代码

其他例子：证明

形成一个单参数组。

证明在这里在线给出，四维扩展在这里在线给出

最后几个例子：证明

形成一个单参数组。

证明在这里在线给出。

证明

形成一个单参数组。

证明在这里在线给出。

更一般地，证明

形成一个单参数组。

证明在这里在线给出。

一个三维扩展：证明

形成一个单参数组。

证明在这里在线给出。

双曲函数的一个例子：证明

形成一个单参数组。

证明是在网上给出的 here

我的问题是：

1. 可以使用数组来证明更高维度吗？

2. 我声称 Z3 是唯一能够执行这些证明的系统。你同意吗？