3

我试图证明群论中的一些一般性质。

例如左取消属性： ( 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 是不可能的？

4

2 回答 2

4

据我所知，这种类型的定理最好由叠加推理引擎处理。旧版本的 Z3 包含一个叠加引擎，但它已从新版本中删除，因为我们很少看到整体用于解决通用代数问题。有几个专门研究叠加位置推断的定理证明器，例如 Vampire、E、SPASS，您可以使用 www.TPTP.org 提供的工具来试用这些引擎。

于 2014-01-23T07:40:00.490 回答
0

使用 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
于 2014-03-31T01:43:28.470 回答