theorem-proving
-
如何定义精益中的互感命题？
-
如何阅读 Coq 对 proj1_sig 的定义？
-
替换 Idris 等式证明中的子表达式
-
精益中的有效类型是什么？
-
coq 中列表 nat 的子集
-
伊莎贝尔的不等式推理
-
归纳 Coq 定义中存在量词和全称量词之间的关系
-
SMT-LIB 中的 QF_NRA 逻辑是否可判定？
-
QF_NRA 中是否包含被零除？
-
Coq 中的简单恒等式
-
带有列表的 Idris 简单证明
-
为什么 simp "fail to apply initial proof method" where blast 用同样的事实成功？
-
当 x 和 xs 静态已知时证明不是 (Elem x xs)
-
Z3 为所有公式提供意外的 UNSAT
-
关于依赖于替代项顺序的函数的证明
-
在 Idris 中与重写策略作斗争
-
精益证明助手中交换环的幂等性
-
Z3 的搜索时间对公式顺序敏感吗？
-
有没有办法使用 SMT 求解器找出如何组合函数？
-
如何在位向量中显示负数？