2

我正在尝试使用以下代码证明群论中的右取消属性

(set-option :macro-finder true)

(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)

但我得到

sat
(error: "out of memory")

请让我知道会发生什么。非常感谢。

4

2 回答 2

2

Z3 并不是特别适合证明通用代数中的定理。具有叠加位置的定理证明器，例如 E、Spass、Vampire，传统上非常适合此类定理。

也就是说，不稳定分支中的Z3版本没有问题。这是我得到的：

z3.exe ua.smt2 /v:10
(simplifier :num-exprs 23 :num-asts 196 :time 0.00 :before-memory 2.61 :after-memory 2.61)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
sat
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
(smt.simplifier-done)
(smt.searching) 
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.mbqi :failed k!6)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!7)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!8)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!9)
(smt.restarting :propagations 0 :decisions 0 :conflicts 0 :restart 100 :restart-outer 100 :agility 0.00)
unsat

您可以从 z3.codeplex.com > 下载 > “计划中”下载 Z3 所谓“不稳定”分支的最新版本

于 2014-04-17T13:13:48.277 回答
1

对于 Z3 的 master 分支版本，这只是一个难题，并且在运行第二个check-sat. 当前版本（不稳定的分支）很快就解决了。（请注意，该macro-finder选项已重命名为smt.macro_finder，但这对该文件没有太大影响。）

于 2014-04-17T13:15:14.420 回答