使用分辨率定理证明 Z3

Question

我是 Z3 的新手，但之前有一些使用 Prolog 的经验。

我已经设法解决了以下“难题”，即使用 Prolog 证明女孩是，但我不知道如何在 Z3 中实现它（在 C++ 或 Python): https://www.netfunny.com/rhf/jokes/90q4/burnher.html

我是否需要为像这样的断言声明 Function() BURNS(x) /\ WOMAN(x) 和 WOMAN(GIRL) \forall x, ISMADEOFWOOD(x) => BURNS(x) 的含义如何？

如有任何提示，我们将不胜感激

Answer 1

应该指出的是，SMT 求解器（即 Z3）一般不擅长用量词进行推理，但这种特殊情况很简单，可以毫不费力地处理。（这很容易，因为您所拥有的只是未解释的排序和布尔值；没有整数、实数、数据类型等会使逻辑复杂化。）此外，与 Prolog 的推导策略相比，使用 SMT 求解器时存在一些建模差异，因此建模会有点不同。

关键在于Prolog使用了所谓的封闭世界假设观点。也就是说，如果它不能显示暗示，它将决定它不是暗示的。 SMT 求解器不会这样做：它将证明含义；但是如果你查询一个没有被适当约束的变量（即，如果根据断言它可以是 True 或 False），那么它可以自由选择任何解释。因此，建模必须考虑到这一点。

这对当前的问题意味着什么？我们必须证明这些陈述暗示女孩是。如果他们不这样做，我们就不知道她是不是。为此，我们断言我们想要的结论是否定的，并检查结果系统是否不可满足。如果是这样的话，那么我们可以得出结论，我们的结论一定是有效的。如果结果是可满足的，那么我们就有了一个可以进一步研究的反例模型。在这种情况下，这意味着没有足够的证据表明该女孩是。（请注意，添加我们要证明的结论的否定是非常典型的分辨率证明，我们在这里遵循相同的策略。）

鉴于所有这些，下面是我将如何使用 Python API 对其进行建模，您应该能够将其转换为 C++（或具有适当绑定的任何其他语言）舒适。这些条款几乎是直译：

from z3 import *

Thing = DeclareSort('Thing')
GIRL  = Const('GIRL', Thing)
DUCK  = Const('DUCK', Thing)

BURNS        = Function('BURNS',        Thing,        BoolSort())
FLOATS       = Function('FLOATS',       Thing,        BoolSort())
WOMAN        = Function('WOMAN',        Thing,        BoolSort())
WITCH        = Function('WITCH',        Thing,        BoolSort())
SAMEWEIGHT   = Function('SAMEWEIGHT',   Thing, Thing, BoolSort())
ISMADEOFWOOD = Function('ISMADEOFWOOD', Thing,        BoolSort())

s = Solver()
x = Const('x', Thing)
y = Const('y', Thing)

s.add(ForAll([x], Implies(And(BURNS(x), WOMAN(x)), WITCH(x))))
s.add(WOMAN(GIRL))
s.add(ForAll([x], Implies(ISMADEOFWOOD(x), BURNS(x))))
s.add(ForAll([x], Implies(FLOATS(x), ISMADEOFWOOD(x))))
s.add(FLOATS(DUCK))
s.add(ForAll([x, y], Implies(And(FLOATS(x), SAMEWEIGHT(x, y)), FLOATS(y))))
s.add(SAMEWEIGHT(DUCK, GIRL))

# To prove the girl is a witch, we assert the negation,
# and check if it is unsatisfiable.
s.add(Not(WITCH(GIRL)))

res = s.check()

if res == sat:
    print("Nope, it doesn't follow that she's a witch!")
elif res == unsat:
    print("Yes, she is a witch!")
else:
    print("Hmm, solver said: ", res)

当我运行这个时，我得到：

Yes, she is a witch!

对她来说太可惜了！

您可以通过注释掉一些断言来进行试验，您会看到 z3 会说系统是 sat，即它不能断定女孩是。然后您可以详细查看模型本身以找出分配的内容。

您可以通读 https://ericpony.github.io/z3py-tutorial/advanced-examples.htm 以了解如何使用基本 Python API 进行未解释的排序、量词和基本建模。如果您有具体问题，请随时进一步询问..

使用分辨率定理证明 Z3

Using Resolution theorem proving with Z3

c++

z3