問題の決定可能性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/05/28 07:09 UTC 版)
使用する論理によって、論理式の妥当性の判定は自明なものから不可能なものまで様々である。命題論理の多くの問題では、定理は決定可能だがco-NP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、完全性定理より妥当な論理式は証明可能であり、その逆も成り立つから、妥当な論理式の全体は再帰的に枚挙可能である。したがって、妥当な論理式の証明を機械的に探索することはできる。 妥当でない文、すなわち与えられた定理から意味論的に導かれない式は認識可能とは限らない。さらにゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的不完全であり、本質的不完全な体系は本質的決定不可能であるから、とくに決定不可能である。そのような場合、一階述語論理の定理証明機は証明探索の完了に失敗する（停止しない）可能性がある。このような理論上の制限はあるが、実用的な定理証明機は様々な難しい問題の証明をすることができる。
※この「問題の決定可能性」の解説は、「自動定理証明」の解説の一部です。
「問題の決定可能性」を含む「自動定理証明」の記事については、「自動定理証明」の概要を参照ください。
ウィキペディア小見出し辞書の「問題の決定可能性」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 問題の決定可能性のページへのリンク
