＞「思いつくのは大変だけど、証明を追うのは誰でもできる」

命題論理の命題の証明チェックは多項式時間でできるが
そもそも証明できるかどうかの判定はNP完全だから
P≠NPならば、多項式時間ではできない・・・

ついでにいうち
述語論理の場合証明チェックのアルゴリズムはあるが
そもそも証明可能かどうか判定するアルゴリズムは・・・ない

これ豆な