Rocq Prover
Rocq Prover
软件描述
一个可信的、工业级的交互式定理证明器及依赖类型编程语言，用于数学、计算机科学等领域的机械化推理。
官方网站
访问软件的官方网站了解更多信息
官方认证
rocq-prover.org
安全链接HTTPS
什么是 Rocq Prover?
Rocq证明器是一个交互式定理证明器，或称证明助手。它提供了一种形式化语言，用于编写数学定义、可执行算法和定理，并配备了一个半交互式的环境，用于开发机器可检查的证明。
主要功能
🔄 替代方案
4 个选择
Lean Prover
Lean 是一种基于依赖类型理论的函数式编程语言和交互式定理证明器。依赖类型理论将程序与证明的世界统一起来，因此 Lean 也是一种编程语言。
F*
F* 是一种类似 ML 的函数式编程语言，旨在实现程序验证。F* 可以表达程序的精确规范，包括功能正确性性质。用 F* 编写的程序可被转换为 OCaml 或 F# 以供执行。
Isabelle
Isabelle 是一个用于通过计算机编写和检查数学证明的证明助手。
Agda
Agda 是一种依赖类型函数式编程语言。它具有归纳族，即依赖于值的数据类型，例如指定长度的向量类型。它还支持参数化模块、混合运算符、Unicode 字符以及交互式 Emacs...
