• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

1992 年度 研究成果報告書概要

プログラム基礎理論の総合的研究

研究課題

研究課題/領域番号 02302009
研究種目

総合研究(A)

配分区分補助金
研究分野 数学一般
研究機関東北大学

研究代表者

佐藤 雅彦  東北大学, 電気通信研究所, 教授 (20027387)

研究分担者 亀山 幸義  東北大学, 電気通信研究所, 助手 (10195000)
龍田 真  東北大学, 電気通信研究所, 助手 (80216994)
研究期間 (年度) 1990 – 1992
キーワードプログラム理論 / 構成的論理 / 型理論 / グラフ理論
研究概要

(1)基礎数理、(2)応用数理、(3)プログラミングの3つの主題について、プログラミングの基礎となる理論の構築、理論に基づくプログラム開発方式の研究、実際の応用プログラムの開発を行った。プログラムの基礎的諸理論について考察し、相互の関連を検討するこにより、各理論を深化させることができた。特に、本研究により次のような研究成果を得た。
佐藤は、証明を内的対象としてもつ論理体系RPTを構成し、プログラム理論の基礎を与えた。龍田は、構成的プログラミングのための帰納的定義の実現可能性解釈について研究した。亀山は、構成的プログラミングシステムの作成および研究活動の基盤となる計算機ネットワークに関する研究を行った。伊藤は、並列プロセスの構造化モでルと項書換え計算モデルについて研究を行い、それらに基づくソフトウェアの試作をした。林は、Singleton,union,intersectionによる型理論の新しい枠組を提唱し、これが、constructive programmingのためには、従来の型理論の枠組より強力な表現力をもつことを示した。萩谷は、形式的な証明を記述するための計算機環境を構築するために必要と考えられる基礎的な技術、特に、例による証明、例を用いた証明、証明の視覚化等を含む証明チェッカのユーザ・インターフェースに関する研究を行った。小野は、構造規則を欠いた論理のセマンティクス、決定問題、有限モデル性について、いくつかの結果を得た。野下は、ゲーム木の高速探索技法を開発し,詰将棋を解くプログラムに応用した。牛島は、並行処理プログラムのテスト法およびデバッグ法の基礎と実際について研究した。

  • 研究成果

    (24件)

すべて その他

すべて 文献書誌 (24件)

  • [文献書誌] M.Sato: "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Proceedings of Theoretical Aspects of Computer Software. 53-87 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Tatsuta: "Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams" Theoretical Computer Science.

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Tatsuta: "Uniqueness of normal proofs of minimal formulas" Journal of Symbolic Logic.

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 亀山 幸義: "構成的数学体系RPTに基づく超数学定理の形式化" 情報処理学会第42回全国大学. 1. 47-48 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 有川 節夫,西野 哲朗: "学習における計算論的アプローチ" 情報処理学会誌. 32-3. 217-225 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] J.Cheng and K.Ushijima: "Analyzing Ada Tasking Deadlocks and Livelocks Using Extended Petri Nets" Lecture Notes in Computer Science. 499. 125-146 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Noshita and Y.Nakatani: "A note on deleting the maximum element in nested s-heaps" Trans.ofIECEJ. E73,10. 1725-1726 (1990)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] E.Kiriyama and H.Ono: "The contraction rule and decision problems for logics without structural rules" Studia Logica. 50. 299-319 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 萩谷 昌己: "高階単一化と証明の一般化" 人工知能学会誌. 6,3. 388-396 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Hagiya: "Synthesis of rewrite programs by higher-order and semantic unification" New Generation Computing. 8,4. 403-420 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Hagiya: "Higher-order unification as a theorem proving procedure" Eighth International Conference on Logic Programming. 270-284 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 佐藤 雅彦,桜井 貴文: "プログラムの基礎理論" 岩波書店, 348 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] I.Ito and A.R.Meyer: "Proceedings of Theoretical Aspects of Computer Software" Springer, 770 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 林 晋,小林 聡: "構成的プログラミングの基礎" 遊星社, 254 (1991)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 龍田 真: "型理論" 近代科学社, 82 (1992)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Sato: "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Proceedings of Theoretical Aspects of Computer Software. 53-87 (1991)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Tatsuta: "Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams" Theoretical Computer Science.

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Tatsuta: "Uniqueness of normal proofs of minimal formulas" Journal of Symbolic Logic.

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] J.Cheng and K.Ushijima: "Analyzing Ada Tasking Deadlocks and Livelocks Using Extended Petri Nets" Lecture Notes in Computer Science. 499. 125-146 (1991)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K.Noshita and Y.Nakatani: "A note on deleting the maximum element in nested s-heaps" Trans. of IECEJ E73. 10. 1725-1726 (1990)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] E.Kiriyama and H.Ono: "The contraction rule and decision problems for logics without structural rules" Studia Logica. 50. 299-319 (1991)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Hagiya: "Synthesis of rewrite programs by higher-order and semantic unification" New Generation Computing 8,4. 403-420 (1991)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Hagiya: "Higher-order unification as a theorem proving procedure" Eighth International Conference on Logic Programming. 270-284 (1991)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] I.Ito and A.R.Meyer: "Proceedings of Theoretical Aspects of Computer Software" Springer. (1991)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 1994-03-24  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi