问题标签 [proof-system]

我正在寻找一种工具（首选 GUI，但 CLI 可以），它允许我输入数学表达式，然后对它们执行操作，但将我限制为仅在数学上有效的操作。此外，该工具必须能够保存会话并稍后证明给定的一组已保存操作是有效的。

注意：我不是在寻找生成证明的系统，只是检查我手动指定的步骤是否有效。

我已经将ACL2用于类似的操作，并且在某些情况下效果很好，但在其他所有情况下都很难使用。

这个小项目是我的动力。它是一种 D 模板类型，允许求解方程。给定这个等式：

任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。它的工作原理是将表达式树构建到类型中，然后使用重写规则将其转换为可以为未知类型触发的东西。

我需要的是某种方法来验证重写规则。它们可以通过测试一个断言来验证，即给定一些关系是真的，另一个也是真的。

......他们是否在我有能力阅读的地方发布了结果？

我有定义的归纳类型：

现在我必须证明该归纳类型的一系列属性，但我一直卡住。

有人可以帮助我前进。

自动证明两个一阶公式 F 和 G 等价的最佳方法是什么？

与“完整”一阶公式相比，这些公式有一些限制：

1. 无量词
2. 无功能
3. 隐含的普遍量化的

我可以将这些公式转换为子句范式，并且我有统一文字的例程。但是，我不确定如何继续以及是否可以确定此问题。

在 COQ 中，类型 prod（具有一个构造函数对）对应于笛卡尔积，类型 sig（具有一个构造函数）对应于依赖求和，但是如何描述笛卡尔乘积是依赖求和的特例这一事实？我想知道 prod 和 sig 之间是否存在联系，例如一些定义相等，但我在参考手册中没有明确找到它。

我试图解决以下问题，但我无法检查它....或者 wolfram 会这样做吗？我不知道我对运算符（范围）的处理是否是 occrect...你知道吗？对于所有 x：颠倒的 A 运算符（通用性）

证明：

快速复审：

• 推理规则=结论+规则+前提
• 证明树 = 结论 + 规则 + 子树
• 后向证明搜索：给定一个输入目标，尝试通过自下而上的方式应用推理规则构建证明树（例如目标是最终结论，应用规则后会生成新的子目标列表现场）

问题：
给定一个输入目标（例如A AND B,C），假设我们首先在 上应用规则 AND A AND B，然后得到两个新的子目标，第一个是A,C，第二个是B,C。
问题是A和B是无用的，这意味着我们可以只使用C. 但是，我们有两个子目标，那么我们要证明C两次，所以效率很低。

问题：
例如，我们有A AND B,C AND D,E AND F,G,H AND I. 在这种情况下，我们只需要 D 和 G 来构建完整的证明树。那么如何选择正确的规则来应用呢？

这是 Ocaml 中的示例代码：