问题标签 [theorem-proving]

大约 2-3 周前，我开始学习定理证明者 Isabelle。我仍然是一个绝对的初学者，到目前为止，我一直在学习“Isabelle/HOL 中的编程和证明”教程。

到目前为止，我发现的关于矩阵的唯一帮助是查看HOL 库中的源代码。

现在我想学习如何证明矩阵的性质。矩阵的 lambda 语法对我来说仍然是新的。有没有关于在 Isabelle 中使用矩阵的教程或基本/中级示例？

在我的伊莎贝尔理论中，我有一个具有常数因子的矩阵：

我可以计算转置矩阵：

在我看来，后者应该相当于

根据 的定义transpose。但是这是错误的。我的错误是什么？

顺便说一下，转置的定义是：

我面临以下引理的问题，我认为这应该是正确的。我可以通过小步骤使证明工作到某个点，但是我还没有找到证明整个引理的方法。

我是 Coq 的新手，但通过一些努力，我能够证明各种归纳引理。但是，我卡在所有使用以下归纳定义的练习中：

我得到的最远的是以下引理：

以下两个引理我无法通过第一步，因为我exists在使用intros.

任何帮助，将不胜感激！

很多时候我遇到的问题是sledgehammer找到一个证明，但是当我插入它时，它并没有终止。我想sledgehammer这是 Isabelle 最重要的部分之一，但如果证明失败，它会变得很烦人。

在Sledgehammer 教程中，有一个小章节是“为什么 Metis 无法重构证明？”。

它列出：

1. 尝试isar_proofs获取逐步 Isar 证明的选项，其中每一步都由metis. 由于步骤相当小， metis因此更有可能重播它们。
2. 尝试smt证明方法而不是metis. 它通常更强大，但您需要有 Z3 可用于重放证明、信任 SMT 求解器或使用证书。
3. 尝试blastor autoproof 方法，根据需要通过unfolding, using, intro:, elim:, dest:, 或传递必要的事实simp:。

问题是第一个选项使证明更加冗长，并且还涉及人工干预。第二个选项很少奏效。

那么第三个选项呢。我可以应用任何易于遵循的启发式方法吗？

unfolding和有什么区别using？还有关于如何使用intro:,elim:和dest:来自失败metis证明的最佳实践吗？

部分示例

我想去掉证明的第一行，因为这行似乎微不足道。如果我删除第一行，sledgehammer仍然会找到一个证明，但是这个找到的证明失败（不会终止）。

我为正在验证此表单的编译器定义了几种归纳类型

现在这很好并且简化了许多事情，直到我尝试证明一些定理，例如

现在我想进行简单的案例分析，destruct test因为只有 2 个案例，T并F考虑。但是如果我尝试这样做，我会收到一个错误，通知我该destruct策略会生成错误类型的术语。它确实如此。

是否有任何类似的策略destruct可以让我对输入正确的术语进行案例分析并自动发送那些输入错误的术语？我怀疑这是不可能的，在这种情况下，处理此类证明的正确方法是什么？

我最近开始使用伊莎贝尔定理证明器。因为我想证明另一个引理，所以我想使用与引理“det_linear_row_setsum”中使用的符号不同的符号，它可以在 HOL 库中找到。更具体地说，我想使用“χ ij notation”而不是“χ i”。一段时间以来，我一直在尝试制定一个等效的表达式，但还没有弄清楚。

..

我正在寻找一个自动定理证明系统，它可以证明这一点：

鳄鱼带走了男人的孩子。人要求鳄鱼不要吃他的孩子。但鳄鱼说：我会把你的孩子还给你，如果你告诉我，我要拿他怎么办。

他的解析解是这样的：

x - 鳄鱼会吃小孩 y - 男人的答案：鳄鱼会吃小孩

~ 表示平等，！表示不，-> 暗示，+ OR；

所以，答案是男人必须说：“你不会吃掉孩子”；

现在，这里列出了很多系统： http ://en.wikipedia.org/wiki/Automated_theorem_proving

我已经尝试了其中的 5-6 个，但无法真正理解我在这里做什么。如何在其中形式化这个定理，以便我可以进入它的第一部分：

((x~y)->!x) and ((x XOR y)->x)

并得到答案

y作为输出。

任何一次建议，哪个系统至少能够自动执行此操作，并给我更多提示？

问候，康斯坦丁。

我想在我的 C++ 程序中使用 z3 API。我想知道要包含哪些头文件以及如何运行包含 z3 函数等的程序。

我看到了example.cppz3 源代码附带的文件，为了运行这个文件，我必须make examples在内部执行命令的 build 目录中运行

现在，如果我创建任何程序，是否../src/api每次需要编译程序时都需要像这样编译它（包含并链接 lib 文件）？

请帮助我，我以前从未使用过z3。任何帮助是极大的赞赏。:)

我想学习用于 c++ 的 z3 API 以及如何在 c++ 程序中使用它们。我试图找到一个教程，但找不到。我可以从哪里学到这一点？有教程之类的吗？谢谢。