1996 Fiscal Year Annual Research Report
Project/Area Number |
08780297
|
Research Institution | Kyushu Institute of Technology |
Principal Investigator |
藤田 憲悦 九州工業大学, 情報工学部, 講師 (30228994)
|
Keywords | シーケント計算 / 自然演繹体系 / 古典的証明 / 排中律 / グリベンコの定理 / カリ-・ハ-ワード同型 / 例外処理プログラム |
Research Abstract |
論理式を型と解釈する原理(カリ-・ハ-ワード同型)により,μ冠頭形証明に計算的意味(プログラム)を割当てるための基礎的研究として以下のことが明らかになった. (1)シーケントの右側に高々2種類の論理式しか出現することのないμ冠頭形証明の基本的性質について(発表論文2): 1-1)古典命題論理における定理に対しては,必ずμ冠頭形証明が存在する; 1-2)μ冠頭形証明におけるシーケントの右側に対しては,直観主義的証明の特徴であるdisjunction propertyがある意味で成立している; 1-3)古典的証明であるμ冠頭形証明から直観主義的証明への埋め込みは容易に与えることができ,これはグリベンコの定理の拡張となっている. (2)μ冠頭形証明のプログラミングへの応用について(発表論文1): 2-1)μ冠頭形証明は,型付き関数型言語であるMLの例外処理プログラムに自然に対応付け可能である; 2-2)μ冠頭形証明では,シーケントの右側に高々2種類の論理式しか出現することのない.その2種類のうちで,証明図全体に出現している論理式は不変論理式と呼ばれる.その不変論理式は,与えられた定理の構文のみから,“含意"と"かつ"に関してstrictly positiveな部分論理式として特徴付けられる.したがって,シーケント計算における右減規則の適用方法がこの不変論理式により規定できることがわかった.そしてこの不変論理式は,例外処理で外に脱出する値の型に対応していることが解明された.
|
Research Products
(6 results)
-
[Publications] 藤田 憲悦: "μ冠頭形証明とそのプログラミングへの応用に関する一考察" コンピュータソフトウエア. 14・2. 71-75 (1997)
-
[Publications] Ken-etsu Fujita: "μ-Herd Form Proofs with Two Formulas in Succedent" 情報処理学会論文誌. (採録).
-
[Publications] Ken-etsu Fujita: "On Proof Terms and Embeddings of Classical Substructurah Logics" Studia Logica. (採録).
-
[Publications] 藤田 憲悦: "μ冠頭形証明とそのプログラミングへの応用に関する一考察" 日本ソフトウエア科学会第13回大会論文集. 417-420 (1996)
-
[Publications] 縄田 和裕 他: "Martin-Lofの型理論に基づくプログラム生成支援システムの構築" 情報処理学会研究報告書. 97・25. 1-8 (1997)
-
[Publications] 縄田 和裕 他: "Martin-Lofの型理論に基づくプログラム支援システムの構築" 情報処理学会九州支部研究会報告. 1-10 (1997)