z3 - SMT 上下文中的“无量词逻辑”是什么意思？

Answer 1

Answer 2

帕特里克给出了一个很好的答案，但这里还有一些想法。（我会将此作为评论，但 StackOverflow 认为它太长了！）

• 请注意，您不能总是玩“否定并检查相反”的把戏。这只有效，因为如果一个属性的否定是不可满足的，那么该属性对于所有输入都必须为真。但它并没有反过来：一个属性可以是可满足的，它的否定也可以是可满足的。简单的例子：x < 10. 这显然是可以满足的，它的否定也是如此x >= 10。所以，你不能总是通过玩这个把戏来摆脱量词。它仅在您想证明某事时才有效：然后您可以否定它并查看该否定是否不可满足。如果您担心找到公式的模型，则该方法不适用。

• 您始终可以对公式进行 sklemize 并通过用未解释的函数替换它们来消除所有存在量词。然后你最终得到的是一个具有所有前缀普遍性的等值公式。显然，这不是免费的量词，但这是大多数工具自动为您执行的一个非常常见的技巧。

• 所有这些伤害的地方是交替量词。不管 skolemization，如果你有交替量词，那么你的问题已经很难处理了。关于量词消除的维基百科页面相当简洁，但它给出了很好的介绍：https ://en.wikipedia.org/wiki/Quantifier_elimination底线：并非每个理论都承认量词消除，甚至那些可能需要指数算法的理论摆脱它们；导致性能问题。