我一直在寻找各种SMT求解器,主要是Z3,CVC4和VeriT.他们都有模糊描述他们用量词解决SMT问题的能力.他们的文档主要是基于示例的(Z3),或由学术论文组成,描述可能或可能不实际实现的可能变更.
我知道有一阶逻辑的可判定片段,例如:
我想知道的是,哪些(如果有的话)FOL类是保证完整的各种SMT求解器？我怎么知道我正在看的问题是否在他们完成的片段中？
无论这是否可判,我都在苦苦挣扎:
A = {x是自然数|的集合的元素 对于大于x的每个y,2y是两个素数之和}
我倾向于认为这是可判定的,因为当它被送入图灵机时,它将永远不会达到接受状态并且无限循环,除非它拒绝.但是,我也知道,对于一种可判定的语言,必须只有一种算法来决定它; 我们不一定要知道它是如何完成的.有了这个,我认为它是可判定的吗？有谁知道如何证明？
一阶逻辑的有效命题 (EPR) 片段通常被定义为以下形式的 prenex 量化公式集\xe2\x88\x83X.\xe2\x88\x80Y.\xce\xa6(X,Y)，其中X和Y是（可能为空）变量序列。量化的顺序（即 ）\xe2\x88\x83*\xe2\x88\x80*对于 EPR 的可判定性重要吗？如果改变量化顺序，我们会失去可判定性吗？
特别是，我对捕获可判定逻辑中的 set-monadic 绑定操作的语义感兴趣。给定S1类型的元素集T1（即S1具有类型）和类型的T1 Set函数，set-monad 的绑定操作通过应用于每个元素来构造一个新的类型集fT1 -> T2 SetS2T2 SetfS1并联合结果集可以在以下 SMT-LIB 代码/公式中捕获此行为：
(declare-sort T1)\n(declare-sort T2)\n;; We encode T1 Set as a boolean function on T1\n(declare-fun S1 (T1) Bool)\n(declare-fun S2 (T2) Bool)\n;; Thus, f becomes a binary predicate on (T1,T2)\n(declare-fun f (T1 T2) Bool)\n(assert (forall ((x T1)(y T2)) (=> …在 Coq 标准库中，“小于”关系对于自然数 ( lt_dec) 和整数 ( Z_lt_dec) 是可判定的。然而，当我搜索 ( Search ({ _ _ _ } + {~ _ _ _ })) 时，我找不到 aQ_le_dec或Qle_dec的有理数，只能Qeq_dec找到可判定的相等性。
这是因为“小于”关系对于 Coq 中的有理数来说是不可判定的吗？或者它是可以决定的，但决策过程没有在标准库中实现？