问题标签 [theorem-proving]

我是一名二年级学生，我的离散数学 2 任务是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序（假设证明始终存在）。到目前为止，我已经用谷歌搜索了，但那里的材料在 4 周内真的很难理解。谁能推荐我一些适合初学者的书籍/网站/开源代码或一些有用的提示？先感谢您。

因此？

我的问题发生的用例上下文

我定义了一个三角形的 3 个随机项。Microsoft Z3 应输出：

• 约束是否满足或是否有无效的输入值？
• 所有其他三角形项目的模型，其中所有变量都分配给具体值。

为了约束我需要assert三角形等式的项目 - 我想从勾股定理（(h_c² + p² = b²) ^ (h_c² + q² = a²)）开始。

问题

我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手动计算器也能够解决这样一个非常简化的版本：

问题

• 如果给出两个值，有没有办法让 Microsoft Z3 解决勾股定理？
• 或者：是否有另一个定理证明器能够处理这些非线性算术的情况？

感谢您对此的帮助 - 如果有任何不清楚的地方，请发表评论。

当我在Isabelle中陈述引理时，我经常输入nitpick，如果这没有给我一个反例。然后我键入sledgehammer以尝试自动查找证明。

我想知道：是否可以调用Nitpick和Sledgehammer以便它们同时运行？既然Sledgehammer已经将我的引理发送给了一堆自动证明者，那么这些证明者中的一个难道不能成为像Nitpick这样的反例发现者吗？

我的例子：方程组

我想要的信息

在方程组中，我想获得以下知识：

我可以用来从给定值（在约束基础中）计算变量值（解决方案）的抽象公式。

（就像在高中，老师不仅想要看到结果，还想要这样一个转换的抽象公式。）

我的问题

如何使用Z3Py从 Z3 约束方程系统中检索此信息？

谢谢。- 如果有任何不清楚的地方，请评论什么是错的。

我有一个简单的定理，我想用案例证明来证明。下面给出一个例子。

我将如何解决这个问题。而且，我将如何使用相等的两个可能值（真或假）来定义证明？

任何帮助，将不胜感激。谢谢，

我有以下目标：

我想将此目标分解为六个子目标P 0，P 1，P 2，P 3和。这很容易做到。但是用于执行此操作的相关规则是什么？我问是因为我的实际目标看起来更像这样：P 4P 5apply autoauto

并且apply auto不会以同样的方式打破这个目标（它给了我

反而）。

我已经定义了自己的布尔值，称为booleanSMT2，以及boolean_and它们的 AND 函数。我的猜想是 AND 是可交换的：

然而，z3 在一段时间后报告了这个问题的未知数，尽管我认为它应该能够对 skolemised 变量sk_x和sk_y.

奇怪的是，如果我删除我的布尔公理化并将其替换为 declare-datatypes，z3 将报告unsat：

我究竟做错了什么？如何使用我的公理化让 z3 进行案例拆分？

我的情况

我正在做一个需要：

• 证明涉及矩阵运算的3D 矩阵变换公式的正确性
• 找到具有未知矩阵条目值的模型。

我的问题

• 使用矩阵运算来表达公式以便它们可以解决的最佳方法是z3什么？（Z3Py 的 Sudoku 示例中使用的方式不是很优雅，似乎不适合更复杂的矩阵运算。）

谢谢。- 如果有任何不清楚的地方，请留下问题评论。

I've defined a module signature in Coq that defines several notations. When I try to use these notations outside of the signature however, Coq fails. A simplified version of my code is given below. Any help would be appreciated.

我想证明我的一些程序的正确性，但我不知道从哪里开始。假设我有以下程序，我该如何证明它的正确性或缺乏。我怎样才能从下面的源代码中将它们插入定理证明器。Coq 或 ACL2 或几乎任何东西。

下面的代码只计算它从标准输入中读取的字节数。它有 2 个版本，一个逐字节计数，另一个尽可能以无符号整数大小的块读取它们。我知道它既不便携也不漂亮，这只是一个可以让我入门的例子。在一些帮助下。

代码有效，我知道它是正确的，我知道如何为它编写单元测试，但我不知道如何证明它。