Z3無法在羣論中證明權利取消的屬性？

Question

我想證明一些在羣論中的一般性質。

例如左取消屬性：（XY = XZ）=>（Y = Z）它證明用下面的代碼

(declare-sort S) 
(declare-fun e() S) 
(declare-fun mult (S S) S) 
(declare-fun inv (S) S) 
(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 (inv x) x) e))) 
(assert (forall ((x S)) (= (mult x e) x))) 
(assert (forall ((x S)) (= (mult x (inv x)) e))) 
(check-sat) 
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult x y) (mult x z)) (= y z))))) 
(check-sat) 

和相應的輸出是：

sat 
unsat 

現在當我嘗試使用以下代碼證明右對消性質：（yx = zx）=>（y = z）

(declare-sort S) 
(declare-fun e() S) 
(declare-fun mult (S S) S) 
(declare-fun inv (S) S) 
(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 (inv x) x) e))) 
(assert (forall ((x S)) (= (mult x e) x))) 
(assert (forall ((x S)) (= (mult x (inv x)) e))) 

(check-sat) 
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult y x) (mult z x)) (= y z))))) 
(check-sat) 

我獲得

timeout 

請讓我知道如何證明右取消財產或者使用Z3是不可能的？

Answer 1

據我所知，這種風格的定理更好地由超位置推理引擎處理。 老版本的Z3包含一個疊加引擎，但是它從新版本 中刪除，因爲我們在整體解決通用代數問題時看到了很少的用途。有幾個專門研究超位置推理的定理證明，比如吸血鬼，E，SPASS，你可以使用www.TPTP.org提供的工具來試用這些引擎。

Answer 2

使用Z3的權利取消屬性的​​可能證明如下。

(declare-sort S) 
(declare-fun e() S) 
(declare-fun mult (S S) S) 
(declare-fun inv (S) S) 
(assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z))))) 
(assert (forall ((x S) (y S) (z S)) (= (mult x (mult y z)) (mult (mult x y) z)))) 
(assert (forall ((x S)) (= (mult e x) x))) 
(assert (forall ((x S)) (= (mult (inv x) x) e))) 
(assert (forall ((x S)) (= (mult x e) x))) 
(assert (forall ((x S)) (= (mult x (inv x)) e))) 
(check-sat) 

(push) 
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult (mult y x) (inv x)) 
               (mult (mult z x) (inv x))) (= y z))))) 
(check-sat) 
(pop) 

和相應的輸出是

sat 
unsat