定理自動証明技術の計算論的研究

閲覧数: 4
ダウンロード数: 0
このエントリーをはてなブックマークに追加

定理自動証明技術の計算論的研究

フォーマット:
助成・補助金
Kyushu Univ. Production 九州大学成果文献
タイトル(他言語):
Computational Complexity of Automated Theorem Proving
責任表示:
岩間 一雄(京都大学・工学研究科・教授)
IWAMA Kazuo(京都大学・工学研究科・教授)
本文言語:
日本語
研究期間:
1996-1997
概要(最新報告):
人工知能分野の基本的テーマである定理の自動証明は,多くの研究者の興味を引いて来たが,基礎的な解析が進んでいないため未だ実用化の目度が立っていない.本研究では定理証明系の複雑さの解析を行なうことを目的とし,導出原理の複雑さに関する研究を行なった.導出原理とは,和積形論理式が恒偽であることを証明する証明系である.本テーマに関して,以下結果を得た. (1)導出原理による証明を見つける問題は盛んに議論されており,証明を見つけるための高速なアルゴリズムも近年発見されている.本研究では,本問題を最適化の面から議論した.すなわち,できるだけ短い証明を見つける問題の複雑さを議論した.その結果,n変数の論理式の最短の証明の長さをSとしたとき,任意の定数dに対し,長さS+O(n^d)以下の証明を見つける問題がNP困難であるという結果を得た. (2)導出原理とバックトラック法の関係について論じた.バックトラック法とは,CNF論理式の充足可能性問題(SAT)に対する深さ優先探索アルゴリズムである.本研究では,導出原理の証明木からバックトラック法の探索木が,また逆にバックトラック法の探索木から導出原理の証明木が,サイズを増やさずに得られることが分かった. (3)冗長度を増すことにより,証明時間を極端に減らすことができる例を発見した.あるグラフ問題をSATに変換して得られた論理式に対し,そのままでは証明に指数ステップを要する(ことが予想される)が,冗長な項を少数追加することによって,多項式時間で証明することができる.他の問題をSATに変換して解く場合,式のサイズを小さくすることが効率の上昇に継ると考えられているが,本結果は,ある程度の冗長度を含ませることも重要である場合があることを示唆している. 続きを見る
本文を見る

類似資料:

4
定理証明系PCMGTPのFPGA上の実装について by 藤田, 博; Fujita, Hiroshi; 河野, 真史; Kawano, Atsushi; 長谷川, 隆三; Hasegawa, Ryuzo
10
畳込みと分岐補題を統合したモデル生成 by 松下, 慎; Matsushita, Makoto; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, 博; Fujita, Hiroshi; 越村, 三幸; Koshimura, Miyuki
11
GASH: An improved algorithm for maximizing the number of equivalent residues between two protein structures by Standley, Daron M; Toh, Hiroyuki; 藤, 博幸; Nakamura, Haruki; 中村, 春木
6
カテゴリー論的計算機数学の総合的研究 by 河原 康雄; KAWAHARA Yasuo
12
陽電子消滅、X線回折、レーザラマン分光によるグラファイトの結晶性評価 by 蔵元, 英一; 佃, 昇; 竹中, 稔; 長谷川, 雅幸; 田辺, 哲朗; Kuramoro, Eiichi; Tsukuda, Noboru; Takenaka, …
4.
定理証明系PCMGTPのFPGA上の実装について by 藤田, 博; Fujita, Hiroshi; 河野, 真史; Kawano, Atsushi; 長谷川, 隆三; Hasegawa, Ryuzo
6.
カテゴリー論的計算機数学の総合的研究 by 河原 康雄; KAWAHARA Yasuo
10.
畳込みと分岐補題を統合したモデル生成 by 松下, 慎; Matsushita, Makoto; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, 博; Fujita, Hiroshi; 越村, 三幸; Koshimura, Miyuki
11.
GASH: An improved algorithm for maximizing the number of equivalent residues between two protein structures by Standley, Daron M; Toh, Hiroyuki; 藤, 博幸; Nakamura, Haruki; 中村, 春木
12.
陽電子消滅、X線回折、レーザラマン分光によるグラファイトの結晶性評価 by 蔵元, 英一; 佃, 昇; 竹中, 稔; 長谷川, 雅幸; 田辺, 哲朗; Kuramoro, Eiichi; Tsukuda, Noboru; Takenaka, …