1995 Fiscal Year Annual Research Report
| Project/Area Number |
07640295
|
|---|
| Research Institution | Shizuoka University |
|---|
Principal Investigator |
古森 雄一 静岡大学, 理学部, 助教授 (10022302)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小崎 高太郎 静岡大学, 理学部, 助教授 (10028186)
板津 誠一 静岡大学, 理学部, 助教授 (20126767)
伊沢 達夫 静岡大学, 理学部, 助教授 (20021941)
白井 古希男 静岡大学, 理学部, 助教授 (70077915)
千葉 慶子 静岡大学, 理学部, 教授 (90022227)
|
|---|
| 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のλ-μ項との関連について新しい知見を得た.
|
-
[Publications] Yuichi Komori: "Syntactical Investigations into BI Logic and BB'I Logic" Studia Logica. 53. 397-416 (1994)
-
[Publications] Sachio Hirokawa: "A reduction rule for Peirce formula" Studia Logica.
-
[Publications] Keiko Chiba: "The weak covering numlev and O-tightness of v-products" Reports of the Faculty of Science, Shizuoka Univ.30. 13-23 (1996)
