数理論理学と関連分野の研究

Research Project

Project/Area Number	07640295
Research Category	Grant-in-Aid for General Scientific Research (C)
Allocation Type	Single-year Grants
Research Field	General mathematics (including Probability theory/Statistical mathematics)
Research Institution	Shizuoka University
Principal Investigator	古森雄一静岡大学, 理学部, 助教授 (10022302)
Co-Investigator(Kenkyū-buntansha)	小崎高太郎静岡大学, 理学部, 助教授 (10028186) 板津誠一静岡大学, 理学部, 助教授 (20126767) 伊沢達夫静岡大学, 理学部, 助教授 (20021941) 白井古希男静岡大学, 理学部, 助教授 (70077915) 千葉慶子静岡大学, 理学部, 教授 (90022227)
Project Period (FY)	1995
Project Status	Completed (Fiscal Year 1995)
Budget Amount *help	¥2,100,000 (Direct Cost: ¥2,100,000) Fiscal Year 1995: ¥2,100,000 (Direct Cost: ¥2,100,000)
Keywords	古典論理 / 直観主義論理 / BCK論理 / ラムダ計算 / 型理論
Research Abstract	1.relevance論理の有名な未解決問題のP-W問題(BB'I論理でA→BとB→Aが証明できればA≡Bである)は,MartinとMeyerにより意味論的に,Kronにより複雑ではあるが構文論的に解かれていた。古森と永山は,構文論的なより簡明な証明を与えた。 2.日本でP-W問題が知られるようになったのは,Meyerが来日し,自分たちが行なった意味論的な方法では満足できないので,ラムダ計算を使う証明を試みて欲しいと,広川に伝えたことによる。広川は試みたのであるが,うまくいかなかった。しかし,最近,古森-永山の方法を取り入れることにより,うまくいくことが分かった。しかも,その方法が最も簡明な証明を与える。 3.定理自動証明プログラムotterを使って,非古典命題論理の自動証明はKalmanにより行なわれていた。古森と広川はKalmanの方法を使って,種々のコンビネーターに対応する論理式を公理とする非古典論理について自動証明を試みた. 4.古森は複数の結論をもつ古典論理の自然推論体系を考案し,それとParigotのλ-μ項との関連について新しい知見を得た.