| Project/Area Number |
07804012
|
|---|
| 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 | Kyoto Sangyo University |
|---|
Principal Investigator |
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
|
|---|
| Project Period (FY) |
1995
|
| Project Status |
Completed (Fiscal Year 1995)
|
| Budget Amount *help |
¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 1995: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | 自然演繹 / 古典論理 / 正規性 / 計算機構 / 自然な証明 |
|---|
| Research Abstract |
研究実行計画にしたがって、下記のような結果を得た。
証明論の方法論としてのinfinite version of generalized Konig's lemmaとgeneralized bar inductionの数学的同値性の証明の概要。
自然演繹の新しい体系NDKの再定式化およびその2階論理への拡張。
NDKの正規証明からNKの(自然な)証明への変換アルゴリズムの構成。
NDKの計算機構を表現する項体系NDTRMの定義。
NDKとNDTRMの相互写像などいくつかの詳細は今後の課題として残ったが、方法論は明確なので、実行に問題はないと予想される。
これらの研究において、形式的体系と計算性の問題、計算機使用の援助などに関して、本学の辻井、中神、藤井、鷲原の各教授にも協力を依頼した。大学院生の笠さんは、NDKの最初の協力者であったが、さらにそのグラフィックな表現および論理的複雑度のスケールの研究を担当した。また、プログラミングにおいては学部生の協力も得た。
研究費は、研究連絡および研究会出席などの旅費、知識・技術提供の謝金、文房具、ソフトウエアなどの消耗品などに使用した。設備備品としては書籍以外に、プリンタを購入した。通信費およびコピー代を大学の研究費内でまかなうことができたので、その分を手持ちのパソコンにつなぐプリンタにまわした。実験的な入力を即カラーで見ることができて、大変便利になった。
科学基礎論学会、数理解析研究所短期共同研究集会、超準解析研究会、などで関連テーマの講演を行った。また、関連分野の談話会およびインフォーマルなセミナー講師として、R. Pollack, J-P. jouannaud, MaLi, 小川重義の諸氏を招いた。
|
