満を持して ACL2 をやろうと思い立った。
しかし殆ど解説記事が無い...
環境
- Windows ではうまくいかなかった。
- Racket もうまくいかなかった。
- Jupyter のやつは未確認です。
- Eclipse でできた。これの正式名称は ACL2s というらしい。
Install ACL2 Sedan
Ubuntu でおこなった。
解凍すると、Eclipse も内蔵されている。
画像
.lisp ファイルで命題を書いて、.a2s ファイル上で REPL をおこなう。
はじめの一歩
1=1
を証明した。
(defthm one (equal 1 1) :rule-classes nil)
意味としては、1=1
を書いて、後は自動定理証明器にまかせるかんじだ。
ACL2 の自動定理証明器にばんばん命題を投げていくやり方は、
Lean とも Isabelle とも違うなと思った。
参考記事
TojoQK の投稿
とても分かり易いです。