Isabelle
https://gyazo.com/324694485316c333cf5be3bc47563b4d
高階論理に基づく汎用定理証明系言語
自動証明能力が高い
ホーア論理のためのライブラリがある
HOLの後続システム
website
github
Scala実装, Standard ML実装
入門記事
https://qiita.com/myuon_myon/items/11bb5bfc2e274fdaea7c
プログラムを書いてapply(vcg)を実行すると論理式に変換される
これは人間にも読めるので、数式で見ることでデバッグができる
数学的な記述をそっくりそのままの形で形式検証できるようにしようという Isabelle の野心的な挑戦が数学界隈で全然知られていないのが悲しすぎる ref
型クラス
https://caeruiro.hatenadiary.org/entry/20100516/1274018433
事例
ケプラー予想
中心極限定理
https://link.springer.com/article/10.1007/s10817-017-9404-x?wt_mc=alerts.TOCjournals
https://blog.kuniwak.com/entry/2020/12/19/111404
https://m-hiyama.hatenablog.com/entry/20160609/1465433202
https://swet.dena.com/entry/2022/08/04/181425
OCamlから変換できるんだ
Isar
https://isabelle.in.tum.de/doc/tutorial.pdf
#プログラミング言語