|
定理証明支援系を用いた形式化によって、機械的に検査された正しい証明が得られるだけでなく、一旦完了した証明に対する試行錯誤や適切な抽象化の検討がしやすくなる。本研究の成果の一部である状態付きベクトル加算系からベクトル加算系への変換の形式化においても、適切な抽象化を行うことで元の証明に用いられていた変換が改良された。
また、形式化の過程で構築・蓄積された技術やノウハウは、後に別の定理を形式的に証明する際の道具として生かされる。上記の変換の形式化においてもベクトルの回転に関するライブラリが整備された。
|
