在z3中使用公理推理

我是Z3的新用户，希望它使用一些公理，并且只有那些公理才能将公式简化为一阶逻辑中的另一个等价公式。例：仅使用在z3中使用公理推理

1.（p或q）和（p或r）< => p或（r和Q）

2.not（p或q）< =>不（ p）和不（q）

3.P且p = <>点

证明

不（p或（q和r））< =>（未（p）和不（q））或（不是（p）而不是（r））

我使用C＃API。我想它必须使用未解释的函数，但我不知道如何去做。

Plzz Help。

来源

2012-05-17 Dynamite

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

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

p和< =>点

与

没有（没有（P））< =>点

备注：上述脚本中的编码使用未解释的排序B而不是Bool。因此，Z3也不会尝试通过案例分析进行证明，也不会尝试使用仅包含两个元素的事实。

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

在下面的例子中，我们使用Z3Py来构造一个满足您提供的3个公理的模型，但是这个猜想并不成立。

http://rise4fun.com/Z3Py/7H7

来源

2012-05-17 15:25:20

感谢莱昂纳多！ – Dynamite

我之前使用context.ParseSmtLib（Args）将用户以SMT-LIB格式输入的逻辑公式转换为字符串，以将其转换为有效Term，然后声明公式。我仍然希望用户输入公式作为字符串或以任何其他可能的方式。我如何处理它以获得有效期限，这是新创建的排序中的公式。 P.S.我使用C＃API。谢谢。 – Dynamite

Z3 4.0中的.NET API具有名为'ParseSMTLIB2String'和'ParseSMTLIB2String'的方法。它们都允许我们用各种“绑定”符号（排序名称）。也就是说，我们可以使用使用API创建的排序来初始化解析器符号表。 Z3 4.0发行版包含一个示例（文件'test_managed。cs'，方法'assert_comm_axiom'），显示了如何做到这一点。这个例子使用'ParseSMTLIBString'。函数'ParseSMTLIB2String'类似，但期望SMT 2.0语法，而不是SMT 1.0。 –

在z3中使用公理推理

回答

相关问题