1998 Fiscal Year Annual Research Report

部分構造論理の研究

Research Project

Project/Area Number	10640103
Research Institution	Chiba University
Principal Investigator	古森雄一千葉大学, 理学部, 教授 (10022302)
Co-Investigator(Kenkyū-buntansha)	藤田憲悦九州工業大学, 情報工学部, 講師 (30228994) 廣川佐千男九州大学, 大型計算機センター, 教授 (40126785) 金沢誠千葉大学, 文学部, 助教授 (20261886) 山本光晴千葉大学, 理学部, 助手 (00291295) 桜井貴文千葉大学, 理学部, 助教授 (60183373)
Keywords	部分構造論理 / 古典論理 / 直観主義論理 / BCK論理 / ラムダ計算 / 型理論
Research Abstract	1. 三つの論理式B((β→γ)→(α→β)→α→γ),B′((α→β)→(β→γ)→α→γ),I(α→α)を公理型とし推論規則 modus ponensを持つ含意論理の体系をP-Wという。P-WはBCK論理より弱い部分構造論理である。体系P-Wでα→βとβ→αの両方が証明できればαとβは全く同じ論理式であるか,というのが有名なP-W問題である。歴史的には,P-W問題は意味論的に1982年にE.P.Martinにより肯定的に解かれたが構文論的な解決を求めてその後も研究が続けられた。廣川によって始められたラムダ計算によるP-W問題への取り組みが古森と永山の協力により最終的に解決したものである。我々の方法では,まずP-W問題が体系P-Wでα→αの証明が唯一かという問題と同値であることを示し,α→αの証明が唯一であることを証明した。このことは我々の研究課題である証明図の唯一性の広がりと重要性を示している。 2. 上記の結果は部分構造論理において,証明図が唯一であることの面白い御利益を示している。 3. 複数の結論を持つ自然演鐸体系とλμ計算の関係の研究は,藤田により活発に行なわれ本報告書の研究発表の欄にある三つの論文を生んでいる。 4. BB'IW論理の決定問題はrelevant論理最大の未解決問題であるので,研究代表者,分担者全員で解決にあたっているが問題が難しくみるべく成果は得られていない。 5. 金沢はカテゴリー文法について,それらの構文論的性質や意味論的性質をより明らかにするよう研究を進めている。 6. 桜井は,ラムダ計算のカテゴリーモデルについての研究を進め,構文論的な性質を証明するためのモデルの構成法について成果を得ている。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] 桜井貴文: "Categorical Model Construction for Proving Syntactic Properties" Proceedings of Third Fuji International Symposium. 187-206 (1998)
[Publications] 山本光晴: "Formalization of Graph Search Algorithms and Its Applications" Lecture Notes in Computer Science. 1479. 479-496 (1998)
[Publications] 廣川佐千男: "Infiniteness of proof(α)is polynomial-space complete" Theoretical Computer Science. 206. 331-339 (1998)
[Publications] 藤田憲悦: "On Proof Terms and Embeddings of Classical Substructural Logics" Studia Logica. 61・2. 199-221 (1998)
[Publications] 藤田憲悦: "Calculus of Classical Proofs II" Transactions of Information Processing Society of Japan. 39・12. 3269-3281 (1998)
[Publications] 藤田憲悦: "Polymorphic Call-by-Value Calculus based on Classical Proofs" Lecture Notes in Artificial Intelligence. 1476. 170-182 (1998)

1998 Fiscal Year Annual Research Report

部分構造論理の研究

Principal Investigator

古森 雄一 千葉大学, 理学部, 教授 (10022302)

Research Products

[Publications] 桜井 貴文: "Categorical Model Construction for Proving Syntactic Properties" Proceedings of Third Fuji International Symposium. 187-206 (1998)

[Publications] 山本 光晴: "Formalization of Graph Search Algorithms and Its Applications" Lecture Notes in Computer Science. 1479. 479-496 (1998)

[Publications] 廣川 佐千男: "Infiniteness of proof(α)is polynomial-space complete" Theoretical Computer Science. 206. 331-339 (1998)

[Publications] 藤田 憲悦: "On Proof Terms and Embeddings of Classical Substructural Logics" Studia Logica. 61・2. 199-221 (1998)

[Publications] 藤田 憲悦: "Calculus of Classical Proofs II" Transactions of Information Processing Society of Japan. 39・12. 3269-3281 (1998)

[Publications] 藤田 憲悦: "Polymorphic Call-by-Value Calculus based on Classical Proofs" Lecture Notes in Artificial Intelligence. 1476. 170-182 (1998)

古森雄一千葉大学, 理学部, 教授 (10022302)

[Publications] 桜井貴文: "Categorical Model Construction for Proving Syntactic Properties" Proceedings of Third Fuji International Symposium. 187-206 (1998)

[Publications] 山本光晴: "Formalization of Graph Search Algorithms and Its Applications" Lecture Notes in Computer Science. 1479. 479-496 (1998)

[Publications] 廣川佐千男: "Infiniteness of proof(α)is polynomial-space complete" Theoretical Computer Science. 206. 331-339 (1998)

[Publications] 藤田憲悦: "On Proof Terms and Embeddings of Classical Substructural Logics" Studia Logica. 61・2. 199-221 (1998)

[Publications] 藤田憲悦: "Calculus of Classical Proofs II" Transactions of Information Processing Society of Japan. 39・12. 3269-3281 (1998)

[Publications] 藤田憲悦: "Polymorphic Call-by-Value Calculus based on Classical Proofs" Lecture Notes in Artificial Intelligence. 1476. 170-182 (1998)