22/12/02 07:15:17.51 fZZ7hap7.net
>>294-296
笑えるな
> 1は劣等感に苛まれてる中卒だから火ィつけるとあっちゅー間に燃えるなｗｗｗ
別にぃ～ｗ
守備範囲に近い事項だから書いただけ
de Bruijn、Automathは、知らなかったが
高山信毅 神戸大とMizarは、名前だけは知っていた
それを書いただけ
>URLﾘﾝｸ(ja.wikipedia.org)
>ただ、述語論理の場合、証明が存在しない式で実施すると止まらない
>「決定不能」というのはそういうこと
>証明が存在するなら、必ず終わる
正確に引用した方が良いぞｗｗ
「決定可能性
タブローの方法は命題論理や一引数の一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、二引数以上の一階述語論理において決定不可能である。つまり充足可能な場合(例えば∀x∃yR(x,y))、有限ステップで終了せず、延々と手続きが続く状況に陥ることがあるからである。」
つまり、二引数以上 例えば∀x∃yR(x,y) で、すでに決定不可能であるｗｗ
あと、下記 有限時間に終わるとしても、”P≠NP”問題のような計算複雑性がからむ
いま、ある証明検証のプログラムを走らせてまだ終わらないとする
人は、あと何日か続けて終わるのか？ それとも永遠に終わらないのか？ その判断ができない
これが、計算複雑性の話
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
P≠NP予想
P≠NP予想（P≠NPよそう、英: P is not NP）は、計算複雑性理論（計算量理論）における予想 (未解決問題) の1つで、「クラスPとクラスNPが等しくない」というものである。
理論計算機科学と現代数学上の未解決問題の中でも最も重要な問題の一つであり、2000年にクレイ数学研究所のミレニアム懸賞問題の一つとして、この問題に対して100万ドルの懸賞金がかけられた。
概要
クラスPとは、決定性チューリングマシンにおいて、多項式時間で判定可能な問題のクラスであり、クラスNPは、Yesとなる証拠（Witnessという）が与えられたとき、多項式時間でWitnessの正当性の判定（これを検証という）が可能な問題のクラスである。