theorem-proving
-
HOL 中 THEN 之后 ACCEPT_TAC 的异常
-
使用 SML 和 HOL 推理规则从第一原理证明定理
-
通过一个简单的定理证明理解 Coq
-
Idris 中的定理证明
-
“!=<”之类的错误在 agda 中意味着什么以及如何修复
-
Coq：在编写证明脚本期间查看证明术语
-
Coq 中相互递归类型的“决定相等性”？
-
证明Agda中的爆炸原理
-
Z3 中的全面评估结果？
-
Z3：表达线性代数性质
-
伊莎贝尔有加法版的"Power.thy"吗？
-
Agda：使用 Stack 安装时找不到 std-lib
-
Idris - 证明两个数相等
-
难以在 Idris 中应用证明
-
如何在 Isabelle/HOL 中使用 tactics/Isar 进行归纳？
-
是否可以描述一个不可能实现的功能？
-
Z3：用量词建模
-
从集合包含到精益中的集合平等
-
如何在精益中使用 Pi 类型编写非依赖产品的定义？
-
精益 : eq.subst h 窒息:(n=0)