z3 - SMT 究竟针对哪些量词完成？

Question

我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们都对自己用量词解决 SMT 问题的能力有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述可能会或可能不会实际实现的可能更改。

我知道有一阶逻辑的可判定片段，例如:

有界量词

Monadic 一阶逻辑

我想知道的是，各种 SMT 求解器保证完成哪些(如果有)FOL 类？我如何知道我正在查看的问题是否在它们完成的片段中？

Answer 1

CVC4 完成了两类量化公式。

(1) 具有有限域的量化公式。

CVC4 在未解释的排序上的量词上是有限模型完备的，这意味着如果存在一个模型，其中所有未解释的排序都被解释为有限的，那么 CVC4 最终会找到它。有关详细信息，您可以查看这篇论文:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
这里总结了 session 论文:
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
它建立在早期的 session 论文之上:
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