定理証明手習い の商品レビュー

ダニエル・P.フリードマン(著者),カール・イーストルンド(著者),中野圭介(著者)

2018/03/27

定理証明系がどういうものかはなんとなくわかった。
自明の積み重ねで大きなことを証明していくイメージを持った。
対話形式は疑問を生んで解消できず、私にとって苦手なことがわかった

2018/01/08

（あとがきによれば画期的な）定理証明ツールとして J-Bob なるものが使われていて、実際にそれで動かしながら読むことが勧められているが、これがあまりにも使いづらいツールであることはすぐに気づくと思う。実際、定理とは式の書き換えでしかないので、目で追っていっても問題ないし、本の説明も、「最後は定理Aと定理Bを用いて終了です」とかいう端折った書き方をしてるし。

訂正。ツール名を J-Bob であるのに誤って ACL2 と書いていました (https://twitter.com/ksknac/status/946744439891927041)