1998 Fiscal Year Annual Research Report
| Project/Area Number |
10740053
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
菊池 誠 神戸大学, 自然科学研究科, 助手 (60273801)
|
|---|
| Keywords | 証明論 / 計算量理論 / 算術 / resolution |
|---|
| Research Abstract |
1. 概要
本研究は命題論理の証明図の長さの下限について,特に resolution での(弱い)PHP の証明図の長さの下限を求めることを中心に,算術の公理系との関係,PHP の証明図の構造の分析,代数的手法との関連の三つの視点から研究を進めるものである.本年度は特に算術の公理系との関係,PHP の証明図の構造の分析について研究をおこなった.
2. 算術の公理系との関係.
命題論理の証明図の長さとの対応を持つ弱い算術の体系そのもについての分析を中心に行っている.そうした弱い体系での不完全性定理の成立の分析によって体系の分離の可能性を調べることは,計算量のクラスの分離とも関係を持つ重要な研究課題である.最近 Adamowicz によって,強い算術の体系についての新しい不完全性定理の証明が発見さているが,本研究ではその新しい証明を分析し,弱い算術の体系での不完全性定理の成立に関する Wilkie Paris の結果への応用を試みている。なお,この研究について CUNY Logic Workshop において講演と研究討議がなされた.
3. PHP の証明図の構造の分析.
本年度の研究から resolution を regular な場合に限定した場合とそうでない場合の証明図の下限の違いは,PHP によっては分離できないという予想が得られた.PHP の証明図の長さの下限は regular な場合に限定したとしてもまだ解決されていないが,この予想が正しければ研究対象を regular なものに限定することが可能になる.
|
