| 研究概要 |
本研究は,ソフトウェア検証,定理証明,プログラム解析等の複雑な論理構造をもつ計算の本質を,求解,証明,書換という記号計算に求め,これら三つの記号計算の特質を究明し,それらのインタラクションによる計算の方法論を構築するとともに,インタラクションを可能にする記号計算グリッド(ウェブサービスシステム)を構築することを目的としている.
本年度はソフトウェアの検証と幾何学的対象の制約問題を重点的に取り上げ,次の二つのサブプロジェクトに分けて研究を推進した.
●上記課題の問題解決における,求解,証明,書換のインタラクションの研究
●インタラクションの計算環境である記号計算グリッドの構築
問題によって,インタラクションの方法は異なるので,対象そのものに対する研究として,計算折紙,定理証明系を用いたソフトウェアの検証およびソフトウェアの性質の自動証明の研究を並行して推進した.具体的にはプログラム検査器で利用される形式言語の包含関係の検査アルゴリズムを証明支援系Isabelle/HOLで形式化し,その正しさを検証した.また,等式と不等式が必要とされる幾何学的問題の自動定理証明を行った.
ウェブサービスネットワークの構築については,記号計算システムMathematicaを対象として,Mathematica,グーグルツールキット,JAVA技術を活用して行った.記号計算ウェブサービスシステムは全体の設計が完成し,実装を行ってしる.一部はすでにできあがっており,グレブナー基底計算をこのシステムを介して行えるようになっている.
海外共同研究者Bruno Buchbergerとは,科学技術のための記号・数値計算シンポジウムにおいて,打ち合わせを行った.特に,Buchbergerが考案したグレブナー基底計算アルゴリズムの幾何定理証明への応用と定理証明系Theoremaとウェブサービスとの連携について討議し,その結果をウェブサービスネットワークの構築に反映させた.
|
