| 研究分担者 |
小崎 高太郎 静岡大学, 理学部, 助教授 (10028186)
板津 誠一 静岡大学, 理学部, 助教授 (20126767)
伊沢 達夫 静岡大学, 理学部, 助教授 (20021941)
白井 古希男 静岡大学, 理学部, 助教授 (70077915)
千葉 慶子 静岡大学, 理学部, 教授 (90022227)
|
|---|
| 研究概要 |
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のλ-μ項との関連について新しい知見を得た.
|
