c++ - 使用 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)通常不擅长使用量词进行推理，但这种特殊情况很容易处理，可以毫不费力地处理。 (这很容易，因为您所拥有的只是未解释的排序和 bool 值；没有整数、实数、数据类型等使逻辑复杂化。)此外，与 Prolog 的推导策略相比，使用 SMT 求解器时存在一些建模差异，所以建模会有点不同。
关键是Prolog使用了所谓的封闭世界假设观点。也就是说，如果它不能显示隐含，它将决定它不是隐含的。 SMT 求解器不会这样做:它将证明含义；但是，如果您查询的变量没有受到适当的约束(即，根据断言，如果它可以是 True 或 False)，则可以自由选择任何解释。因此，建模必须考虑到这一点。
这对当前的问题意味着什么？我们必须证明这些陈述暗示女孩是女巫。如果他们不这样做，我们不知道她是不是。为此，我们断言我们想要的结论的否定，并检查结果系统是否不可满足。如果是这样，那么我们可以得出结论，我们的结论一定是有效的。如果结果令人满意，那么我们就有了一个反例模型，可以进一步研究。在这种情况下，这意味着没有足够的证据证明这个女孩是女巫。 (请注意，添加我们要证明的结论的否定是非常典型的解决证明，我们在这里遵循相同的策略。)
鉴于这一切，这就是我将如何使用 Python API 对其进行建模，您应该能够相对轻松地将其转换为 C++(或任何其他具有适当绑定(bind)的语言)。这些条款几乎按字面翻译:

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 进行未解释的排序、量词和基本建模。如果您有具体问题，请随时进一步询问..