问题标签 [theorem-proving]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
matrix - 伊莎贝尔:如何使用矩阵
大约 2-3 周前,我开始学习定理证明者 Isabelle。我仍然是一个绝对的初学者,到目前为止,我一直在学习“Isabelle/HOL 中的编程和证明”教程。
到目前为止,我发现的关于矩阵的唯一帮助是查看HOL 库中的源代码。
现在我想学习如何证明矩阵的性质。矩阵的 lambda 语法对我来说仍然是新的。有没有关于在 Isabelle 中使用矩阵的教程或基本/中级示例?
matrix - Isabelle:转置包含常数因子的矩阵
在我的伊莎贝尔理论中,我有一个具有常数因子的矩阵:
我可以计算转置矩阵:
在我看来,后者应该相当于
根据 的定义transpose
。但是这是错误的。我的错误是什么?
顺便说一下,转置的定义是:
matrix - Isabelle:证明具有常数因子的转置矩阵等式
我面临以下引理的问题,我认为这应该是正确的。我可以通过小步骤使证明工作到某个点,但是我还没有找到证明整个引理的方法。
coq - Coq:归纳中的列表问题
我是 Coq 的新手,但通过一些努力,我能够证明各种归纳引理。但是,我卡在所有使用以下归纳定义的练习中:
我得到的最远的是以下引理:
以下两个引理我无法通过第一步,因为我exists
在使用intros
.
任何帮助,将不胜感激!
isabelle - 伊莎贝尔:大锤找到了证据,但失败了
很多时候我遇到的问题是sledgehammer
找到一个证明,但是当我插入它时,它并没有终止。我想sledgehammer
这是 Isabelle 最重要的部分之一,但如果证明失败,它会变得很烦人。
在Sledgehammer 教程中,有一个小章节是“为什么 Metis 无法重构证明?”。
它列出:
- 尝试
isar_proofs
获取逐步 Isar 证明的选项,其中每一步都由metis
. 由于步骤相当小,metis
因此更有可能重播它们。 - 尝试
smt
证明方法而不是metis
. 它通常更强大,但您需要有 Z3 可用于重放证明、信任 SMT 求解器或使用证书。 - 尝试
blast
orauto
proof 方法,根据需要通过unfolding
,using
,intro:
,elim:
,dest:
, 或传递必要的事实simp:
。
问题是第一个选项使证明更加冗长,并且还涉及人工干预。第二个选项很少奏效。
那么第三个选项呢。我可以应用任何易于遵循的启发式方法吗?
unfolding
和有什么区别using
?还有关于如何使用intro:
,elim:
和dest:
来自失败metis
证明的最佳实践吗?
部分示例
我想去掉证明的第一行,因为这行似乎微不足道。如果我删除第一行,sledgehammer
仍然会找到一个证明,但是这个找到的证明失败(不会终止)。
coq - 使用依赖类型进行破坏
我为正在验证此表单的编译器定义了几种归纳类型
现在这很好并且简化了许多事情,直到我尝试证明一些定理,例如
现在我想进行简单的案例分析,destruct test
因为只有 2 个案例,T
并F
考虑。但是如果我尝试这样做,我会收到一个错误,通知我该destruct
策略会生成错误类型的术语。它确实如此。
是否有任何类似的策略destruct
可以让我对输入正确的术语进行案例分析并自动发送那些输入错误的术语?我怀疑这是不可能的,在这种情况下,处理此类证明的正确方法是什么?
matrix - Isabelle 矩阵算术:库中的 det_linear_row_setsum 具有不同的符号
我最近开始使用伊莎贝尔定理证明器。因为我想证明另一个引理,所以我想使用与引理“det_linear_row_setsum”中使用的符号不同的符号,它可以在 HOL 库中找到。更具体地说,我想使用“χ ij notation”而不是“χ i”。一段时间以来,我一直在尝试制定一个等效的表达式,但还没有弄清楚。
..
prolog - 自动定理证明
我正在寻找一个自动定理证明系统,它可以证明这一点:
鳄鱼带走了男人的孩子。人要求鳄鱼不要吃他的孩子。但鳄鱼说:我会把你的孩子还给你,如果你告诉我,我要拿他怎么办。
他的解析解是这样的:
x - 鳄鱼会吃小孩 y - 男人的答案:鳄鱼会吃小孩
~ 表示平等,!表示不,-> 暗示,+ OR;
所以,答案是男人必须说:“你不会吃掉孩子”;
现在,这里列出了很多系统: http ://en.wikipedia.org/wiki/Automated_theorem_proving
我已经尝试了其中的 5-6 个,但无法真正理解我在这里做什么。如何在其中形式化这个定理,以便我可以进入它的第一部分:
((x~y)->!x) and ((x XOR y)->x)
并得到答案
y
作为输出。
任何一次建议,哪个系统至少能够自动执行此操作,并给我更多提示?
问候,康斯坦丁。
compilation - 在 c++ 程序中使用 z3 API 时需要帮助
我想在我的 C++ 程序中使用 z3 API。我想知道要包含哪些头文件以及如何运行包含 z3 函数等的程序。
我看到了example.cpp
z3 源代码附带的文件,为了运行这个文件,我必须make examples
在内部执行命令的 build 目录中运行
现在,如果我创建任何程序,是否../src/api
每次需要编译程序时都需要像这样编译它(包含并链接 lib 文件)?
请帮助我,我以前从未使用过z3。任何帮助是极大的赞赏。:)
c++ - 在哪里可以了解用于 c++ 的 z3 定理证明器 API?
我想学习用于 c++ 的 z3 API 以及如何在 c++ 程序中使用它们。我试图找到一个教程,但找不到。我可以从哪里学到这一点?有教程之类的吗?谢谢。