2

一阶逻辑的有效命题 (EPR) 片段通常被定义为形式为 的一组前置量化公式∃X.∀Y.Φ(X,Y)，其中X和Y是（可能为空的）变量序列。量化的顺序，即∃*∀*EPR 的可判定性是否重要？如果量化顺序被切换，我们会失去可判定性吗？

特别是，我对在可判定逻辑中捕获 set-monadic 绑定操作的语义感兴趣。给定一组S1类型的元素T1（即，S1具有类型T1 Set）和一个f类型的函数T1 -> T2 Set，set-monad 的绑定操作通过对 的每个元素应用并合并结果集来构造一个新S2的类型集。可以在以下 SMT-LIB 代码/公式中捕获此行为：T2 SetfS1

(declare-sort T1)
(declare-sort T2)
;; We encode T1 Set as a boolean function on T1
(declare-fun S1 (T1) Bool)
(declare-fun S2 (T2) Bool)
;; Thus, f becomes a binary predicate on (T1,T2)
(declare-fun f (T1 T2) Bool)
(assert (forall ((x T1)(y T2)) (=> (and (S1 x) (f x y)) 
                                   (S2 y))))
(assert (forall ((y T2)) (exists ((x T1)) (=> (S2 y) 
                                              (and (S1 x) (f x y)))) ))

观察到第二个断言语句有量化的形式∀*∃*，它不符合标准的 EPR 定义。然而，在 Z3 上使用此类公式时，我从未遇到过超时问题，我想知道我上面的公式是否确实在某个可判定的片段中（同时承认实践中的可解性并不意味着理论上的可判定性）。欢迎任何意见。

4

1 回答 1

4

如果量词的顺序不同，它就不再是 EPR。EPR 仅涵盖 EA Phi 形式的公式，其中 Phi 没有函数（仅对绑定变量和自由常量进行谓词）。有一些一阶逻辑的可判定片段不是 EPR，但 Z3 不是此类片段的判定过程。描述此类片段的综合资料来源是 Borger、Graedel、Gurevich，“经典决策问题”。

于 2017-09-13T07:07:33.690 回答