Z3 is not able to prove the equivalence between two simple programs using Kleene algebras with test but Mathematica and Reduce are able

Question

Our problem here is to show that

using Kleene algebras with test.

In the case when the value of b is preserved by p, we have the commutativity 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 preserved by p, we have the commutativity 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 am obtaining timeout; it is to say Z3 is not able to hand the commutativity condition bp = pb. Please run this example online here.

Z3 is not able to prove these equations but Mathematica and Reduce are able. Z3 is not so powerful as a theorem prover. Do you agree?

Answer 1

The first equation is proved 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)")

The output is

sat
sat
unsat
Proved: bpq + b`pr = p(bq + b`r)

Please run this proof online here

Answer 2

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

Please run this example online here

Z3 is not able to prove the second equation directly but Mathematica and Reduce ane able.