• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2004 年度 実績報告書

近似プログララムの計算論-古典論理の証明のテストにむけて-

研究課題

研究課題/領域番号 15700001
研究機関東北大学

研究代表者

赤間 陽二  東北大学, 大学院・理学研究科, 助教授 (30272454)

キーワードmonotone modified 実現可能性解釈 / 構成的論理 / lesser limited principle of omniscience / プログラム抽出 / Lifsitz' 実現可能性解釈 / Markov principle / 冠頭標準形定理 / 無限カット除去定理
研究概要

数学対象の構成的存在証明からは有意な情報を得られることが多いが、どのような構成的推論原理からどのような手法によりそれら有意な情報が抽出できるかが問題となるであろう。
我々は構成的推論原理としてMarkov Principle、弱 Koenig補題,単純全称(存在)量化式に対する排中律、Postの定理、に着目したが、それらの推論原理に現れる論理式を一般の冠頭標準形に拡張することにより、構成的推論原理の階層を考えた:
Σi冠頭標準形に対する二重否定除去原理(Σi-LEM)、
Σi冠頭標準形に対するLesser Limited Principle of Omniscience(Σi-LLPO)、
Σi冠頭標準形に対する排中律(Σi-LEM)
Pi^O_i冠頭標準形に対する排中律(Σi-LEM)
Δi式に対する排中律(Δi-LEM)。
そして、冠頭標準形定理(全ての論理式は同値な冠頭標準形を持つ)との関係をまず考察した。
次に全ての正整数iに対して以下を証明した:Heyting Arithmeticにおいて、
(1)Σi-LEM,Πi-LEM,Σi-LLPO,Δi-LEM Σ(i-i)-LEMの順に真に強い.またΣi-LEM,Σi-DNE,Δi-LEMの順に真に強い。
(2)Πi-LEMとΣi-DNEからΣi-LEMが証明できる。
逆向きがいえないことの示すために、形式証明からプログラムを抽出するための手法を用いた。具体的には、実現可能性解釈、無限カット除去定理、Kohlenbachのmonotone modified実現可能解釈,van OostenのLifschitz'実現可能解釈である。

  • 研究成果

    (1件)

すべて 2004

すべて 雑誌論文 (1件)

  • [雑誌論文] An arithmetical hierarchy of the law of excluded middle and related principles2004

    • 著者名/発表者名
      Y.Akama, S.Berardi, U.Kohlenbach, S.Hayashi
    • 雑誌名

      Proceedings of 19^<th> annual IEEE symposium on logic in computer science

      ページ: 192-201

URL: 

公開日: 2006-07-12   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi