Conversation

@tacumi ラムダノートさんの本って古本屋に出回ってるもんなんですかね……。

下記の本で著者は完全に ACL2 へと誘導しているのですが訳者の方は Coq へと誘導しているのがつらいところです(涙)。この本を読んでも ACL2 の詳細な使い方は結局学べないのですが、ACL2 を使うに当たって前提として知っておくべきことは学べるという感じなんで良いんですよね(ACL2 だと簡単な定理は自動証明するのでまずその仕組みが謎だし、簡単な定理であば自動証明され自動証明できない場合はどう対処すればいいか分からなくて詰むためいきなり ACL2 を使っても練習にならない)。なので、もしも ACL2 をやるのであればとてもおすすめです。

訳者の方が Coq を勧めているようなのでおそらく他の定理証明支援系に進むにしても役立つ基礎的な内容なのだと思います。

『定理証明手習い』 – 技術書出版と販売のラムダノートhttps://www.lambdanote.com/collections/littleprover