我想知道有没有人能告诉我Z3和coq之间的区别？ 在我看来，coq是一种证明助手，因为它要求用户填写证明步骤，而Z3则没有这个要求。 但似乎coq也具有类似于Z3的自动策略吗？ 或者说coq中的证明搜索能力不如Z3强大？

我正在尝试使用Z3，由Microsoft Research开发的SMT求解器，检索某些一阶理论的所有可能模型。以下是一个最小工作示例：(declare-const f Bool) (assert (or (= f true) (= f false))) 在这个命题案例中，有两种令人满意的赋值：...

我正在尝试学习Agda，但遇到了问题。我在Agda维基上找到的所有教程都对我来说过于复杂，并涵盖了不同方面的编程。在阅读三个Agda教程的同时，我能够写一些简单的证明，但我仍然没有足够的知识将其用于实际算法正确性。 你可以推荐一些关于这个主题的教程给我吗？类似于Learn Yourself ...

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

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

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

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

我正在用Idris编写一个基本的单子解析器，以熟悉其语法和与Haskell的差异。我已经成功掌握了解析器的基础知识，但我在尝试为解析器创建VerifiedSemigroup和VerifiedMonoid实例时遇到了困难。 以下是解析器类型、Semigroup和Monoid实例，以及Verif...

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

有没有类似于策略simpl用于程序不动点的东西？ 特别地，如何证明以下平凡语句？ Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n' => S (bla n') end. Lemma...