Formative System Engineering 項書換え系を用いた多重文脈型定理証明の高速化 多重文脈型定理証明 等式で表現された定理が、あるデータ構造上で成り立つかどうかの検証 公理とデータ構造は項書換え系で表す 項書換え系は等式に向きをつけた書換え規則の集合 研究目的 マルチコアを使い、項書換え系を用いた多重文脈型定理証明の効率を大きく上げる 等式 項書換え系 公理と データ構造 停止性チェッカーは計算時間の 大部分を占める 多重文脈型定理 証明 停止性 チェッカー 仕様変更可能な ツール 等式が成 り立つか どうか 基本のやり方は項書換え系の ルールを各コアに割り当てて、 タスクを並列に実行する 停止性検査のステップごとに違う設計 順序関係などの潜在バグを排除 現在は様々な並列化手法を試しています
© Copyright 2024 ExpyDoc