"lemma"函数的一般类型应该如何理解？
也许这是一个愚蠢的问题。以下是来自《Hasochism》论文的一句话： One approach to resolving this issue is to encode lemmas, given by parameterised equations, as Haskell func...
Coq中的非空列表追加定理
我正在尝试在Coq中证明以下引理：Require Import Lists.List. Import ListNotations. Lemma not_empty : forall (A : Type) (a b : list A), (a <> [] \/ b <&...
使用定理证明器查找攻击
我听说过使用自动定理证明器来尝试证明软件系统中不存在安全漏洞。一般来说，这是非常困难的。 我的问题是，是否有人在使用类似的工具来发现现有或提议的系统中的漏洞？ 编辑：我不是在询问如何证明软件系统的安全性。我是在询问如何发现（理想情况下是以前未知的）漏洞（甚至是漏洞类别）。我像黑客那样思...
使用Coq证明可逆列表是回文。
这是我关于回文的归纳定义：Inductive pal { X : Type } : list X -> Prop := | pal0 : pal [] | pal1 : forall ( x : X ), pal [x] | pal2 : forall ( x : X ) (...
当使用rewrite策略时，Coq无法找到子项
我正在尝试修改Certified Programming with Dependent Types第一章中栈机器章节的compile_correct证明。在我的版本中，我试图利用progDenote是一个fold的事实，并在主引理的证明中使用更弱的归纳假设来证明compile_correct。...
避免在Z3中使用量词
我正在尝试使用Z3，将算术、量词和相等理论结合起来。但是这似乎并不是很有效，实际上，当可能时，用所有已实例化的基础实例替换量词似乎更加高效。考虑以下示例，在其中我已经对函数 f 进行了唯一命名公理的编码，该函数需要两个类型为Obj的参数，并返回解释类型S。此公理指出，每个唯一的参数列表都将返回...
伊莎贝尔: Sledgehammer 找到了一个证明，但是它失败了。
经常出现这样的问题，sledgehammer 找到了一个证明，但插入后无法终止。我猜测 sledgehammer 是 Isabelle 中最重要的部分之一，但如果证明失败，它就会变得非常恼人。 在 Sledgehammer 教程 中，有一个关于“为什么 Metis 无法重构证明？”的小章节。...
在Agda中，显示 (head . init) = head 是什么意思？
我正在尝试在Agda中证明一个简单的引理，我认为它是正确的。 如果一个向量有两个以上的元素，则在取init后再取head与直接取head相同。 我已经将其表述如下： lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l))) ...
交互式数学证明系统
我正在寻找一个工具（最好是GUI，但CLI也可以），允许我输入数学表达式并对其进行操作，但限制我只能使用数学上有效的操作。此外，该工具必须能够保存会话，并在以后证明给定的一组保存的操作是有效的。 注意：我不是在寻找一个系统来生成证明，只是检查我手动指定的步骤是否有效。 我已经使用ACL2执...
逻辑编程和自动定理证明的区别
逻辑编程和自动定理证明（ATP）（如E-Prover、Spass或Princess）有什么区别？ 我搜索了很多资料，唯一找到的信息是ATP是逻辑编程的前身。但我并不看出两者之间的区别。但我猜想它应该不止于语法上的差异。