为什么引入这个存在量词会导致不终止？答案

【问题标题】：Why does introducing this existential quantifier cause non-termination?为什么引入这个存在量词会导致不终止？
【发布时间】：2019-11-17 17:43:04
【问题描述】：

我刚开始自己玩 Z3，我认为一个有趣的实验是构建一个 3 元素字段。

所以我声明我的域 S 是三个元素 A、B、C 的标量枚举，并开始逐渐添加域公理，在每一步之后要求 Z3 提供一个模型，只是为了看看发生了什么。一切顺利，直到我断言减法的可能性，∀ab.(∃x.a+x=b):

(declare-datatypes () ((S A B C)))

; there exist three distinct elements in S
(declare-const someA S)
(declare-const someB S)
(declare-const someC S)
(assert (distinct someA someB someC))

(declare-fun ADD (S S) S)
(declare-fun MUL (S S) S)

; commutative
(assert (forall ((x S) (y S)) (= (ADD x y) (ADD y x))))
(assert (forall ((x S) (y S)) (= (MUL x y) (MUL y x))))

; associative
(assert (forall ((x S) (y S) (z S)) (= (ADD x (ADD y z)) (ADD (ADD x y) z))))
(assert (forall ((x S) (y S) (z S)) (= (MUL x (MUL y z)) (MUL (MUL x y) z))))

; subtractivity
(assert (forall ((a S) (b S)) (exists ((x S)) (= (ADD a x) b))))

(check-sat)
(get-model)

这会导致 Z3 永远循环。我很惊讶。我的意思是，我理解为什么 FOL 通常是无法确定的，但我认为这将是那些“简单”的情况之一，因为 a、b 和 ADD 的所有可能值的空间是有限的（在这种情况下甚至非常小的）？为什么会循环？什么是表达可减性公理的正确方法，最好以一种不会失去可感知性作为其预期的直观含义的方式？

【问题讨论】：

量词很难，交替量词更难。虽然您有一个有限（且很小）的域，但 z3 无法识别这一点，并且很可能会陷入电子匹配器的内部。这类问题不适合 SMT 求解：我建议使用适当的定理证明器（如 Isabelle、Coq、Agda、HOL、Lean 等）来处理这类公理化。

标签： z3 smt theorem-proving

【解决方案1】：

虽然@alias 对他的建议总体上是正确的，但如果您愿意削弱您的公理化，您仍然可以使用 Z3。例如：

...
; subtractivity
(declare-fun SUB (S S) S)
(assert (forall ((a S) (b S) (x S)) (iff (= (ADD a x) b) (= (SUB b x) a))))

(check-sat)
(get-model)

【讨论】：