jmi*_*ite 5 first-order-logic decidable smt z3 cvc4
我一直在寻找各种SMT求解器,主要是Z3,CVC4和VeriT.他们都有模糊描述他们用量词解决SMT问题的能力.他们的文档主要是基于示例的(Z3),或由学术论文组成,描述可能或可能不实际实现的可能变更.
我知道有一阶逻辑的可判定片段,例如:
我想知道的是,哪些(如果有的话)FOL类是保证完整的各种SMT求解器？我怎么知道我正在看的问题是否在他们完成的片段中？
小智 4
CVC4 已完成两类量化公式。
(1) 有限域的量化公式。
CVC4 在未解释排序上的量词上是有限模型完备的，这意味着如果存在一个模型，其中所有未解释排序都被解释为有限，那么 CVC4 最终会找到它。有关详细信息，您可以参阅这篇论文：
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
，其中总结了会议论文： http:
//homepage.divms.uiowa.edu/~ajreynol/cav13 .pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
请注意，这些技术与 CVC4 支持的任何理论相结合。假设理论是可判定的并且量化不涉及（无限）解释排序，则有限模型完整性保证仍然存在。
该方法对于某些片段也是反驳完全的，例如 Bernays-Schoenfinkel-Ramsey 片段（EPR），这意味着对于该片段中的任何不可满足的问题，CVC4 最终都会回答“unsat”。
如果您对此功能感兴趣，CVC4 默认情况下不会对输入问题使用有限模型查找。命令行选项“--finite-model-find”将启用这些技术。
(2) 一些理论中的量化公式会产生量词消除。
例如，CVC4 对于（纯）量化线性算术来说是完整的。有关详细信息，您可以参阅这篇论文：
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
，该论文基于早期的会议论文： http:
//homepage.divms.uiowa.edu/~ajreynol /cav15a.pdf
这在本质上与其他方法类似，例如在 Z3 中： https:
//www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf