氏名: 白井 基裕 (l0481636)

論文題目: MRCによるTRS処理プログラミングのための基本ライブラリ開発


論文概要

TRS(項書換え系)は定理の自動証明やソフトウェアの代数的仕様記述などに広く 利用され、 これまでに多くの理論的成果が得られている。MRC(メタ項書換え計算)はTRSの記 述・実行 ばかりでなく、TRSの処理の記述・実行のようなTRSのメタ計算を表現するための 計算モデ ルである。TRSのメタ計算の例としてはTRSの合流性や停止性といった性質の判定 などが上 げられるが、これらのTRSを処理するMRCプログラムの開発には、項の代入、マッ チング、 単一化などのように多くの共通する項の処理プログラムが必要である。本研究で は、この ようにTRSの処理や解析をMRCを用いて行なう際に必要となる様々な基本的処理に ついて調 査し、それを実際にMRCプログラムとして実現して、今後のMRCプログラミングに 有用な基 本ライブラリの開発を行う。


目次に戻る


asakura@nuie.nagoya-u.ac.jp