| 研究概要 |
本年度は求解,証明,書換のインタラクションによる計算が本質的に重要である研究対象として,ソフトウェアの検証と幾何学的対象の制約問題を重点的に取り上げ,次の二つのサブプロジェクトに分けて研究を実施した.
(1)上記課題の問題解決における,求解,証明,書換のインタラクションの研究
(2)インタラクションの計算環境である記号計算グリッドの構築
また,問題によって,インタラクションの方法は異なるので,対象そのものに対する研究にも同時に着手した.本年度は特に,計算折り紙,定理証明系を用いたソフトウェアの検証およびソフトウェアの性質の自動証明を研究した.前者では,幾何制約を表現する高次多項式系の求解,折り方が仕様を満たしていることの証明を行った.我々のアプローチを適用し,Morleyの三角形として知られる幾何定理の自動証明の問題の解決を試み,ネットワークを介した16時間という計算時間を必要としたものの,自動定理証明に成功した.
後者では,ソフトエアの検証に取り組み,高階論理に基づく定理証明系Isabell/HOL でコンパイラーの検証に成功した.
計算グリッドの構築については,記号計算システムMathematicaを活用して,Mathematicaベースのシステム構築をGlobusツールキット,JavaServer Pageの技術を活用して推進している.すでに構築がすんだ部分については,webOrigamiサイトとして,一般に公開している(URL:weborigami.score.cs.tsukuba,ac.jp)
|
