Matitaという定理証明系のdockerイメージを作りました。 MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。 Leanの論文から参照されていたので知りました。 定理証明器の研究用途に作成されたようなので実用…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。