コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

ACL2 をやってみた

ACL2(Lisp系)

満を持して 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 の投稿
とても分かり易いです。