c# - 在 z3 中使用公理进行演绎

Question

我是 Z3 的新用户，希望它使用一些公理，并且只使用这些公理将一个公式简化为一阶逻辑中的另一个等效公式。例如：仅使用

1.(p or q) and (p or r) <=> p or (r and q)

2.not(p or q) <=> not(p) and not(q)

3.p 和 p <=> p

证明

not(p or (q and r)) <=> (not(p)and not(q)) or (not(p)and not(r))

我使用 C# API。我想它必须使用未解释的功能，但我不知道该怎么做。

请帮助。

score 1 · Accepted Answer

你是对的，这个想法是使用未解释的函数和排序。这是 Z3 中编码的问题： http ://rise4fun.com/Z3/Vzns

Z3 找不到使用您提供的 3 个公理的证明。实际上，结论并不能从他们那里得出。但是，如果我们替换公理，它可以找到一个证明

p 和 p <=> p

和

不是（不是（p））<=> p

备注：上面脚本中的编码使用未解释的排序B而不是Bool. 因此，Z3 也不会尝试逐案证明，也不会尝试使用Bool仅包含两个元素的事实。

备注：它使用=而不是<=>.

在下面的示例中，我们使用 Z3Py 构建了一个满足您提供的 3 个公理的模型，但猜想不成立。

1 回答 1