Conversation

@tacumi ラムダ計算は勉強しなくても大丈夫ですね。学ぶ必要があるのは高校レベルの数学的帰納法の知識と、定理証明の基本的なところ(公理や既存の定理を使って式を変形する)です(場合によっては順序数とかも必要になるのですが……)。あと再は帰関数が書けるのは前提として必要なくらいですね。これらについては『定理証明手習い』という本で学べます。

これだけならまだしも ACL2 になると自動定理証明なので、 自動証明できない定理については、ACL2 に補助定理を教えたりヒントを与えたりしないといけないわけなんですが、補助定理の書き方には細かいルールがあって書き方によって ACL2 の挙動は変わるんですよね……。これを学ぶ学習コストに耐えないと ACL2 は全く使えないといっても過言ではないところが痛いんです。