| 研究概要 |
本研究では,ソフトウェアの検証,定理自動証明,プログラム解析等の複雑な論理構造を対象とする計算の本質を,求解,証明,書換という記号計算に求め,それらのインタラクションによる高次な計算の方法論を構築し,さらにこれを支援する記号計算ネットワークを構築することを目的とする.本年度は求解,証明,書換のインタラクションによる計算が本質的に重要であるソフトウェアの検証と幾何学的対象の制約問題・定理証明を深く掘り下げた.研究は次の二つのサブプロジェクトに分けて推進した.
(1) 上記ドメインにおける,求解,証明,書換のインタラクションの研究
(2) インタラクションを可能とする記号計算ネットワークの構築
(1)に関しては,計算折り紙,定理証明系を用いたソフトウェアの検証を行った.この一連の研究により,一階述語論理で記述された論理式を多項式に変換し,自動定理証明系へと接続する手法の健全性を明らかにし,この手法を実現するソフトウェアを完成させた.このソフトウェアは我々が構築したE-Origami System(EOS)と呼ぶシステムと統合して作動している.(2)に関しては,Google Web Toolkit(GWT)を用いて,独自のWebサービスシステムを構築した.当初はGlobus Toolkitを用いて,グリッドとして構築する予定であったが,Webサービスのほうが,本研究の目的により合致するため,GWTの技術を用いたWebサービスシステムを構築した.Scorumと呼ぶ我々のシステムは定理自動証明系をWebサービスとして利用でき,(1)で構築したEOSとも結合して運用することができる.
海外共同研究者のBruno Buchbergerとはグレブナ基底を用いた幾何学定理証明の高速化について,共同して考察した.
|
