>>963
Coqは難しいです。私は挫折しました。
私はもう少し分かりやすいシステムを開発していて、自然演繹ベースです。
多分よく知られている論理体系の中では自然演繹が最も初学者でも分かりやすいです。
たとえば、命題論理で有名なPeirceの法則は私のシステムで証明すると↓の画像のようになります。
https://i.imgur.com/WMRbwRt.png
上の方にある図のようなものが証明の内容を図的に表したもの（証明図）で
下の方にあるコマンドがこの証明を行うのに必要なコマンド列です。
今のところ私のシステムでは論理式の作成から証明まで全部コマンドを実行することで行います。
これは人間が手動で証明する場合には面倒なのですが（なので今後改善が必要）
人工知能に証明させる場合はコマンドを覚えさせるだけなので楽かもしれませんね。

＞まだ先になるかもしれません
はい、私は私で自分のシステムの開発を続けます。
お互い開発頑張りましょうね！a4さんは大学院進学も。