在Z3中使用归结定理证明
我是Z3的新手，但有一些使用Prolog的经验。
我已经设法解决了以下“难题”，即使用Prolog证明这个女孩是个巫师，但我不知道如何用Z3 (用C++或Python)实现它：https://www.netfunny.com/rhf/jokes/90q4/burnher.html
我需要为像BURNS(x) /\ WOMAN(x)和WOMAN(GIRL)这样的断言声明\forall x, ISMADEOFWOOD(x) => BURNS(x) ()吗？
任何建议都值得感谢。
回答 1
Stack Overflow用户
发布于 2020-07-04 02:50:09
应该指出的是，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，了解如何使用basic Python API进行未解释的排序、量词和基本建模。如果您有具体的问题，请随时提出进一步的问题。
https://stackoverflow.com/questions/62720552
复制相似问题
腾讯云开发者
