用z3表示推理规则

Question

我一直在阅读和研究几篇文档，我仍然不清楚如何用z3表示我的推理规则。

假设我有以下2条推理规则：

​

​

我的z3规则是否如此简单：

a. (a ^ b) => c

b. (a ^ b) => c

或者，我认为更正确的是，我是否需要声明数据类型(记录、标量等)。

从那里开始，java实现在阅读文档时显得相当直接。

这仅仅是从一个类型系统的推理规则到命题逻辑的初始转换，这让我感到很困扰。

我认为我的推理规则(a和b)与在z3中表示它们之间缺少某种联系；当我继续阅读文档时，对于如何显示这些规则仍然不太清楚。

Answer 1

对于这个任务，Z3将是一个很好的选择，尽管很难确切地理解您的问题是什么。(你拥有的要点a和b完全相同，是故意的吗？)但从本质上说，推理规则是隐含的，因此，从命题和它们之间的含义来考虑它们是很好的。

此外，您的规则可能会有一个角结构(如Prolog中的角子句，参见这里的：clause)，而Z3有一个数据模拟引擎，它可以使这样的问题更容易编码。

请参见这里的很好的介绍：http://rise4fun.com/z3/tutorialcontent/fixedpoints，我认为它可以相对容易地应用到您的用例中。