>>785
＞自動定理証明

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

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

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