Open Provable Foundation

2022年6月9日 (四) 07:14的版本

Open Provable Foundation（开放可证明基础）

Provably Awesome
ML 语言家族适用于形式语言、计算机辅助定理证明、证明助理、逻辑语言、一阶逻辑、论证软件、代码验证等形式化领域。
Haskell, Agda, Idris, Liquid Haskell 具有“证明即程序、命题为类型”的特征。
F*
ACL2
proof assistant
Coq
Isabelle
HOL = functional programming + logic HOL Interactive Theorem Prover 文档 HOL Theory Hierarchy (Theory Graph)
seL4 The world's most highly assured OS kernel, specification and proofs with isabelle. The seL4 Haskell Model Haskell
Trustworthy Systems Formal methods
Hardware description language for Formal verification

@@ 第10行： / 第10行： @@
 *分析哲学
 *形式科学是指主要研究对象为抽象形态的科学，如逻辑、数学、数理逻辑、信息论、统计学（数理统计学）、理论计算机科学（计算理论）、经济学（博弈论）等。
+==SMT==
+*[http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisfiability Modulo Theories (SMT)]
+*[https://smtlib.cs.uiowa.edu/ SMT-LIB]
+*[https://smt-comp.github.io/ International Satisfiability Modulo Theories Competition (SMT-COMP)] 国际可满足性模理论竞赛
 ==项目==