去年から作ってた自作の定理証明支援系、実用的な状態にまで持っていくのが絶望的に難しいということで放置してたんだけど、『定理証明手習い』(ラムダノート社)を読むときに限って有用な可能性があるのでしばらくしたら記事を作ろうと思ってる。 

本の中では J-Bob っていう定理証明支援系を使うように促されるんだけど J-Bob のインターフェースは結構つらかった(ミスがあると全部 `nil` って返ってくる)し、環境構築もなんか大変だった。

少し試してたところ Jupyter Notebook との相性が凄くいい、あとはエラーメッセージを親切にして環境構築をしやすいようにすれば普通に使ってもらえる気がする。

定理証明支援系 Vikalpa のテストコードはこんな感じ:
git.tojo.tokyo/vikalpa.git/tre

Follow

今の状態だと「 Guix を使ってれば超簡単にインストールできるよ!まずは Guix をインストールしてね!」って感じになっちゃうのでなんか用意しないといけない。

· · Web · 0 · 0 · 0
Sign in to participate in the conversation
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!