定理証明支援系 matita のdockerイメージを作った - ::Eldesh a b = LEFT a

Matitaという定理証明系のdockerイメージを作りました。

MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。
Leanの論文から参照されていたので知りました。
定理証明器の研究用途に作成されたようなので実用するものでは無さそうですが*1、検証器の実装に興味がある人には面白そうです。

最新版にはパッケージが無いようですし、ビルドも面倒なのでdockerイメージを作りました。 > eldesh/matita

$ docker pull eldesh/matita:0.99.3

IDEとして使用するため環境変数DISPLAYを指定して起動します。
# /usr/local/matita/matitacというのがCLIを提供するようですがよく分かりません*2。

$ docker run -it --rm -e DISPLAY=192.168.1.2:0 eldesh/matita:0.99.3

使い方を知るには/usr/local/matita/lib/tutorialにチュートリアルがあるのでこれを読むと良さそうです。

私自身もまだ全く理解してませんが、ちょっとだけGUIの様子を紹介します。

左のペインがソースコードです。右下はmatitaのログのようです。
CoqIDEのように上から行毎にチェックを進め、右上のペインに現在の証明ゴールと前提が表示されています。
面白いのは[?3120][?3119]と表示されているタブで、これは各タブが各サブゴール毎の画面になっています。

分岐した後に各枝がどういった証明図(?)になっているのか簡単に分かるというのは便利そうです。

*1:実用とは？

*2:-extract_ocamlというオプションもあるので気になりますね