我是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)的含义呢？
任何提示都值得赞赏
应该指出的是，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 用于未解释的排序、量词和基本建模。如果您有具体问题，请随时进一步提问。