我已经阅读并研究了几篇文档，但我仍然不清楚如何在 z3 中表示我的推理规则。
假设我有以下 2 个推理规则:
是否如此简单，我的 z3 规则将是:
a. (a ^ b) => c
b. (a ^ b) => c
或者，我认为更正确的是，我是否必须声明数据类型(记录、标量等)。
从这里开始，通过阅读文档，java 实现显得相当简单。
这只是从类型系统的推理规则到命题逻辑的最初转换，这让我很困惑。
我认为我缺少推理规则(a 和 b)和在 z3 中表示它们之间的某些联系；当我继续阅读文档时，对于如何体现这些规则仍然不清楚。
最佳答案
Z3 对于这项任务来说是一个不错的选择，尽管很难准确理解你的问题是什么。 (你的要点 a 和 b 是完全相同的，这是故意的吗？)但本质上推理规则是蕴涵，所以从命题和蕴涵的角度来思考它们他们之间就好了。
此外，您的规则可能会有 Horn 结构(如 Prolog 中的 Horn 子句，请参阅此处: https://en.wikipedia.org/wiki/Horn_clause )，并且 Z3 有一个数据记录引擎，可以使编码此类问题变得更加容易。
请参阅此处，了解非常好的介绍:http://rise4fun.com/z3/tutorialcontent/fixedpoints我认为它可以相对轻松地应用于您的用例。
关于java - 在 z3 中表示推理规则，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/45020081/