Z3 cannot prove equivalence between two simple programs using Klein algebras with test, but Mathematica and Reduce are capable
Our task here is to show that
using Klein algebras with test.
In the case when the value of b is stored on p, we have the commutation condition bp = pb; and the equivalence between the two programs is reduced to the equation
In the case when the value of b is not stored on p, we have the commutation condition pc = cp; and the equivalence between the two programs is reduced to the equation
I am trying to prove the first equation using the following SMT-LIB code
(declare-sort S)
(declare-fun sum (S S) S)
(declare-fun mult (S S) S)
(declare-fun neg (S) S)
(assert (forall ((x S) (y S) (z S)) (= (mult x (sum y z)) (sum (mult x y) (mult y z))) ) )
(assert (forall ((x S) (y S) (z S)) (= (mult (sum y z) x) (sum (mult y x) (mult z x))) ) )
(assert (forall ((x S) (y S) (z S)) (= (mult x (mult y z)) (mult (mult x y) z)) ))
(check-sat)
(push)
(declare-fun b () S)
(declare-fun p () S)
(declare-fun q () S)
(declare-fun r () S)
(assert (= (mult b p) (mult p b)) )
(check-sat)
(pop)
but i get timeout
; this means that Z3 cannot transmit the commutation condition bp = pb. Please run this example online here .
Z3 cannot prove these equations, but Mathematica and Reduce can. Z3 is not as strong as the proof of the theorem. Do you agree?
source to share
First equation is proven using Z3 with the following SMT-LIB code
(declare-sort S)
(declare-fun e () S)
(declare-fun O () S)
(declare-fun mult (S S) S)
(declare-fun sum (S S) S)
(declare-fun leq (S S) Bool)
(declare-fun negation (S) S)
(declare-fun test (S) Bool)
(assert (forall ((x S) (y S)) (= (sum x y) (sum y x ))))
(assert (forall ((x S) (y S) (z S)) (= (sum (sum x y) z) (sum x (sum y z)))))
(assert (forall ((x S)) (= (sum O x) x)))
(assert (forall ((x S)) (= (sum x x) x)))
(assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
(assert (forall ((x S)) (= (mult e x) x)))
(assert (forall ((x S)) (= (mult x e) x)))
(assert (forall ((x S) (y S) (z S)) (= (mult x (sum y z) ) (sum (mult x y) (mult x z)))))
(assert (forall ((x S) (y S) (z S)) (= (mult (sum x y) z ) (sum (mult x z) (mult y z)))))
(assert (forall ((x S)) (= (mult x O) O)))
(assert (forall ((x S)) (= (mult O x) O)))
(assert (forall ((x S) (y S)) (= (leq x y) (= (sum x y) y))))
(assert (forall ((x S) (y S)) (=> (and (test x) (test y) ) (= (mult x y) (mult y x))) ) )
(assert (forall ((x S)) (=> (test x) (= (sum x (negation x)) e) )))
(assert (forall ((x S)) (=> (test x) (= (mult x (negation x)) O) )))
(check-sat)
(push)
;; bpq + b`pr = p(bq + b`r)
(declare-fun b () S)
(declare-fun p () S)
(declare-fun q () S)
(declare-fun r () S)
(assert (=> (test b) (= (mult p b) (mult b p)) ))
(assert (=> (test b) (= (mult p (negation b)) (mult (negation b) p))))
(check-sat)
(assert (not (=> (test b) (= (sum (mult b (mult p q)) (mult (negation b) (mult p r) ))
(mult p (sum (mult b q) (mult (negation b) r))))) ) )
(check-sat)
(pop)
(echo "Proved: bpq + b`pr = p(bq + b`r)")
Output signal
sat
sat
unsat
Proved: bpq + b`pr = p(bq + b`r)
Run this proof online here
source to share
The second equation is indirectly proved using Z3 with the following procedure
This indirect procedure is implemented with the following SMT-LIB code
(declare-sort S)
(declare-fun e () S)
(declare-fun O () S)
(declare-fun mult (S S) S)
(declare-fun sum (S S) S)
(declare-fun leq (S S) Bool)
(declare-fun negation (S) S)
(declare-fun test (S) Bool)
(assert (forall ((x S) (y S)) (= (sum x y) (sum y x ))))
(assert (forall ((x S) (y S) (z S)) (= (sum (sum x y) z) (sum x (sum y z)))))
(assert (forall ((x S)) (= (sum O x) x)))
(assert (forall ((x S)) (= (sum x x) x)))
(assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
(assert (forall ((x S)) (= (mult e x) x)))
(assert (forall ((x S)) (= (mult x e) x)))
(assert (forall ((x S) (y S) (z S)) (= (mult x (sum y z) ) (sum (mult x y) (mult x z)))))
(assert (forall ((x S) (y S) (z S)) (= (mult (sum x y) z ) (sum (mult x z) (mult y z)))))
(assert (forall ((x S)) (= (mult x O) O)))
(assert (forall ((x S)) (= (mult O x) O)))
(assert (forall ((x S) (y S)) (= (leq x y) (= (sum x y) y))))
(assert (forall ((x S) (y S)) (=> (and (test x) (test y) ) (= (mult x y) (mult y x))) ) )
(assert (forall ((x S)) (=> (test x) (= (sum x (negation x)) e) )))
(assert (forall ((x S)) (=> (test x) (= (mult x (negation x)) O) )))
(assert (forall ((x S)) (=> (test x) (test (negation x)) )) )
(assert (forall ((x S)) (=> (test x) (= (mult x x) x) )) )
(check-sat)
(push)
(declare-fun c () S)
(declare-fun b () S)
(declare-fun p () S)
(declare-fun q () S)
(declare-fun r () S)
(check-sat)
(assert (not (=> (and (test b) (test c))
(= (mult (sum (mult b c) (mult (negation b) (negation c)))
(sum (mult b (mult p q)) (mult (negation b) (mult p r) ) ))
(sum (mult b (mult c (mult p q)))
(mult (negation b) (mult (negation c) (mult p r) ) ) ))) ) )
(check-sat)
(pop)
(echo "Proved: part 1")
(push)
;;
(assert (=> (test c) (= (mult p c) (mult c p)) ))
(assert (=> (test c) (= (mult p (negation c)) (mult (negation c) p))))
(check-sat)
(assert (not (=> (test c)
(= (mult (sum (mult b c) (mult (negation b) (negation c)))
(mult p (sum (mult c q) (mult (negation c) r))))
(sum (mult b (mult c (mult p q)))
(mult (negation b) (mult (negation c) (mult p r) ) ) ))) ) )
(check-sat)
(pop)
(echo "Proved: part 2")
and the corresponding output is
sat
sat
unsat
Proved: part 1
sat
unsat
Proved: part 2
This output is obtained locally. When the code is executed online, the output is
sat
sat
unsat
Proved: part 1
sat
timeout
Run this example online here
Z3 cannot prove the second equation directly, but Mathematica and reduce ane.
source to share