使用分辨率定理证明 Z3 [英] Using Resolution theorem proving with Z3

问题描述

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

I am new to Z3 but have some prior experience using Prolog.

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

I have managed to solve the following "puzzle", i.e. to prove that the girl is a witch using Prolog, but am at a loss how to implement it in Z3 (in C++ or Python): https://www.netfunny.com/rhf/jokes/90q4/burnher.html

我是否需要为诸如此类的断言声明 Function()BURNS(x)/\ WOMAN(x) 和 WOMAN(GIRL)排序 \forall x, ISMADEOFWOOD(x) => 的含义如何?烧伤(x)?

Do I need to declare Function() for assertions like BURNS(x) /\ WOMAN(x) and WOMAN(GIRL) What about implications of the sort \forall x, ISMADEOFWOOD(x) => BURNS(x)?

感谢任何提示

推荐答案

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

It should be pointed out that SMT solvers (i.e., Z3) aren't usually good at reasoning with quantifiers in general, but this particular case is easy enough that it can handle without a sweat. (It's easy because all you have are uninterpreted sorts and booleans; there are no integers, reals, datatypes etc., to complicate the logic.) Also, there are some modeling differences when you use an SMT solver compared to Prolog's deduction strategy, so the modeling will be a bit different.

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

The crucial point is that Prolog uses the so-called closed-world-assumption viewpoint. That is, if it cannot show an implication, it'll decide that it isn't implied. An SMT solver does not do that: It will prove implications; but if you query a variable that isn't properly constrained (i.e., if it can be both True or False according to the assertions), then it's free to pick any interpretation. So, the modeling has to take that into account.

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

What does that mean for the current problem? We have to prove that the statements imply the girl is a witch. If they don't, we don't know whether she is or not. To do so, we assert the negation of the conclusion we want and check if the resulting system is unsatisfiable. If that's the case, then we can conclude our conclusion must be valid. If the result is satisfiable, then we have a counter-example model that we can investigate further. In this case, it'll mean there is insufficient evidence that the girl is a witch. (Note that adding the negation of the conclusion we want to prove is very typical of resolution proofs, and we're following the same strategy here.)

考虑到所有这些，下面是我将如何使用 Python API 对其进行建模，您应该能够相对轻松地将其转换为 C++(或具有适当绑定的任何其他语言).这些条款几乎可以按字面意思翻译:

Given all this, here's how I would go about modeling it using the Python API, you should be able to translate this to C++ (or any other language with proper bindings) with relative ease. The clauses almost translate literally:

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)

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

When I run this, I get:

Yes, she is a witch!

对她来说太糟糕了！

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

You can experiment by commenting out some of the assertions, and you'll see that z3 will say the system is sat, i.e., it cannot conclude the girl is a witch. You can then look at the model itself in detail to find out what the assignments are.

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

You can read through https://ericpony.github.io/z3py-tutorial/advanced-examples.htm to see how to use basic Python API for uninterpreted sorts, quantifiers, and basic modeling. If you've specific questions, feel free to ask further..

这篇关于使用分辨率定理证明 Z3的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！