| 研究分担者 |
大谷 武 (株)富士通研究所, 研究員
竹内 泉 京都大学, 工学研究科, 助手 (20264583)
沢村 一 新潟大学, 工学部, 助教授 (40282991)
亀山 幸義 京都大学, 工学研究科, 助教授 (10195000)
龍田 真 京都大学, 理学研究科, 助教授 (80216994)
|
|---|
| 研究概要 |
本研究は構成的プログラミングの実用化へ向けて,構成的プログラミング支援ソフトウェアのプロトタイプを作成し,それを用いてプログラミングを行うことにより有用性を確認する研究を2年計画で行った.96年度は,(1)構成的プログラミング・システム作成の基礎となるプログラム言語Λの処理系の実装(2)直観主義一階述語論理に対する対話型定理証明システムの実装を行った.97年度は,(3)様相論理など多様な論理体系へ対応した対話型定理証明システムの実装,(4)古典論理を用いた構成的プログラミング・システムの実装を行った.
(1)は(2)〜(4)を実装するために新たに設計したプログラミング言語の実装である.(2):最も基本となる直観主義一階述語論理に対してグラフィカルユーザインターフェースを持つ対話型定理証明支援システムを実装した.実装の一部はJAVAを用いて,モジュール化による分散プログラミング(分散証明)を行える環境とした.(3):(2)を発展させて,各種の様相論理など多様な論理体系へ対応した対話型定理証明システムを実装した.個々の論理体系に依存しない共通した証明戦略の構築が可能なシステムとした.(4):古典論理の証明からのアルゴリズム抽出という新しい話題に関して,catch/throw機構と継続計算という2種類の異なる制御オペレータを用いた体系を実装しアルゴリズム抽出を行った.
(2)〜(4)の構成的プログラミングシステムを利用することにより,多数の例題を記述した.仕様を論理式として厳密に記述できる場合には,プログラム作成までスムーズに進むことが多く,例題を作成することができた.これらの研究成果およびソフトウェアにより,構成的プログラミングの適用範囲が従来より広がり,より実用的な構成的プログラミング・システムの実現へ向けての一歩とできた.
|
