1996 Fiscal Year Annual Research Report
| Project/Area Number |
08558023
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Section | 試験 |
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 工学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
大谷 武 富士通研究所, 研究員
亀山 幸義 京都大学, 工学研究科, 助教授 (10195000)
龍田 真 京都大学, 理学研究科, 助教授 (80216994)
沢村 一 新潟大学, 工学部, 助教授 (40282991)
|
|---|
| Keywords | 構成的プログラミング / 証明支援システム / グラフィカルユーザインターフェース / 証明エンジン |
|---|
| Research Abstract |
今年度の研究では,構成的プログラミング・システムの作成の基礎となるプログラム言語,および,証明支援システムの2点について検討を行い,プロトタイプシステムを作成した.
まず,関数型プログラム言語Aの処理系の作成を行った.Aは手続き型プログラム言語の特徴である代入文を持ちながら,関数型プログラム言語としての良い性質(参照透明性など)を持つというユニークな言語である.本年度の処理系は,インタープリンタであるが,Aのフルセットが動作し,次年度の構成的プログラミング・システム作成の基礎となるものである.
証明支援システムの作成については,グラフィカルユーザインターフェースを含めた対話型証明作成支援環境を実装した.大規模プログラムの開発を構成的プログラミングの手法で行うためには,証明作成が容易であることともに,モジュール化による分散プログラミング(分散証明)が可能でなければならないという考察をおこない,前者のためにSTk(Scheme+Tkツールキット)およびJAVAにより独立に対話型証明作成支援環境を実装した.
今年度は,証明作成エンジンとして直感主義一階述語論理のものを作成して利用したが,次年度には本格的な証明エンジンにいれかえて大規模プログラミングが可能な構成的プログラミングシステムを作成する予定である.
|
Research Products
(6 results)
-
[Publications] Masahiko Sato: "Intutionistic and Classical Natural Deduction Systems with the catch and the throw rules" Theoretical Computer Science. (発表予定).
-
[Publications] 山中淳彦: "参照透明な代入をもつ純関数型言語" コンピュータ・ソフトウェア. (発表予定).
-
[Publications] Hajime Sawamura: "Intuitionistic Logic of Music and its Mechanization with the Hol Theorem Prover" Proc.Int'l Conf.on Comp.Music and Music Science. 68-83 (1996)
-
[Publications] 大谷武: "汎用論証システムEUODHILOS-IIの設計と実装" 情報処理学会論文誌. 38・1. 9-22 (1997)
-
[Publications] Mitsuru Tada: "The Function [a/m] in Sharply Bounded Arithmetic" Archive for Mathematical Logic. (発表予定).
-
[Publications] Yukiyoshi Kameyama: "A New Formulation of the Catch/throw Mechanism" Proc.Int'l Workshop on Func.and Logic Programming. 56-64 (1996)
