我尝试通过形式化推理来证明我熟悉的数学定理：停机问题的不可判定性，以及其他计算理论中的各种定理。由于我对计算模型（如图灵机、寄存器机、λ演算等）的细节不感兴趣，因此我试图通过假设 "Axiom" 来表述Coq认为可计算的函数（即类型为“nat -> nat”的可定义函数）的性质。 例如...

我正在学习陶哲轩的实分析教材，该教材从自然数开始构建基本的数学概念。通过尽可能多地形式化证明，我希望熟悉Idris和依赖类型。 我定义了如下数据类型： data GE: Nat -> Nat -> Type where Ge : (n: Nat) -> (m: N...

传统上，计算逻辑的大部分工作要么是命题逻辑，此时使用 SAT（布尔可满足性）求解器；要么是一阶逻辑，此时使用一阶定理证明器。 近年来，SMT（可满足性模理论）求解器取得了很多进展，基本上将命题逻辑与算术等理论结合起来；SRI国际公司的约翰•拉什比甚至称它们是一种颠覆性技术。 在一阶逻辑中可...

当我编写算法时，我通常会在注释中写下不变量。 例如，一个函数可能返回一个有序列表，而另一个函数期望列表是有序的。 我知道存在定理证明器，但我没有使用它们的经验。 我还相信聪明的编译器可以利用它们来优化程序。 因此，是否可以编写不变量并让编译器检查它们？

当我在Isabelle中声明引理时，我通常会输入nitpick，如果这不能给我一个反例，那么我会输入sledgehammer来尝试自动找到证明。 我想知道：是否可能调用Nitpick和Sledgehammer以便它们同时运行？既然Sledgehammer已经将我的引理发送给许多自动证明器，难...

有人尝试过使用Z3来证明Z3吗？ 甚至有可能使用Z3来证明Z3的正确性吗？ 更理论的问题是，是否可能使用工具X本身来证明工具X的正确性？

在 Coq 中，sig 被定义为： Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. 我的理解是： "sig P" 是一种类型，其中 P 是一个函数，接收...

逻辑编程和自动定理证明（ATP）（如E-Prover、Spass或Princess）有什么区别？ 我搜索了很多资料，唯一找到的信息是ATP是逻辑编程的前身。但我并不看出两者之间的区别。但我猜想它应该不止于语法上的差异。

我听说过使用自动定理证明器来尝试证明软件系统中不存在安全漏洞。一般来说，这是非常困难的。 我的问题是，是否有人在使用类似的工具来发现现有或提议的系统中的漏洞？ 编辑：我不是在询问如何证明软件系统的安全性。我是在询问如何发现（理想情况下是以前未知的）漏洞（甚至是漏洞类别）。我像黑客那样思...

我正在尝试在 Hilbert 风格的系统中证明 ~(a->~b) => a 这个命题。不幸的是，似乎无法想出一般性算法来找到证明，但我正在寻找一种暴力策略。欢迎任何攻击这个问题的想法。