| 研究概要 |
本研究では,ソフトウェアの検証,定理自動証明,プログラム解析等の複雑な論理構造を対象とする計算の本資を,求解,証明,書換という記号計算に求め,それらのインタラクションによる高次な計算の方法論を構築し,さらにこれを支援する記号計算ネットワークを構築することを目的とした.
研究成果は次の二つの分けられる.
1. ソフトウェアの検証と幾何学的対象の制約問題・定理証明における,求解,証明,書換のインタラクションの研究
2. インタラクションを可能とする記号計算ネットワークの構築
1. に関しては,計算折り紙,定理証明系を用いたソフトウェアの検証に関して,多くの成果を挙げ,論文として公刊することができた.特に,計算折り紙における求解系とグロブナ基底計算を用いた自動定理証明,オートマトン理論を援用したウェブソフトウェアの検証およびXML文書の処理と検証のための計算系の設計において顕著な研究成果を得ることができた. 2. に関しては, Google Web Toolkit (GWT)を用いて,ウェブサービスシステムScorum(Symbolic Computation Forum)を設計,実装した.研究当初はグリッドとしてシステムを構築する予定であったが,近年進歩が著しいウェブサービス技術のほうが本研究の目的に合致したシステムを構築するのに適切であるため, GWTの技術を用いた独自のウェブサービスシステムを開発した.また, Scorumを活用した,計算折り紙の計算環境をも構築した.
|
