| 研究分担者 |
藤田 憲悦 九州工業大学, 情報工学部, 講師 (30228994)
廣川 佐千男 九州大学, 大型計算機センター, 教授 (40126785)
金沢 誠 千葉大学, 文学部, 助教授 (20261886)
山本 光晴 千葉大学, 理学部, 助手 (00291295)
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| 研究概要 |
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. 桜井は,ラムダ計算のカテゴリーモデルについての研究を進め,構文論的な性質を証明するためのモデルの構成法について成果を得ている。
|
