我一直在研究各种SMT求解器，主要是Z3，CVC4和VeriT。他们对用量词解决SMT问题的能力都有模糊的描述。他们的文档主要基于示例(Z3)，或由学术论文组成，描述了可能会或可能不会实际实现的更改。
我知道一阶逻辑存在可确定的片段，例如:
我想知道的是，各种SMT求解器可以保证完成哪些FOL类(如果有)？我怎么知道我要解决的问题是在完整的片段中？
最佳答案
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最终都会回答“不满意”。
如果您对此功能感兴趣，则默认情况下，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