>>785
>自動定理証明

全くの脱線ですが、この言葉を聞いた素人は
「任意の命題について、それが証明可能か否か
 判定できるアルゴリズムが原理的に存在するんだ!」
と誤解する

正しくは
「任意の命題について、それがトートロジー(恒真命題)であるとき
 その証明を返すような手続きが存在する」

ついでにいうと全然難しい手続きではありません
よく知られてるのはタブロー法というものです
某私大の文系学部のシラバスでこれ教えてるの見ました
まあ、そういうレベルのことですがなぜか東大では教えないですね
私が見つけられなかっただけかもしれんし、
東大の学生はそんなん大学で教わらんでも
勝手に本読んで勉強して理解するからええ
ということかもしれんけど
(後者ならええですけどね)