研究課題
若手研究
定理証明支援系とは，プログラム等についての数学的性質とその証明をコンピュータ言語で記述できるようなソフトウェアシステムである．記述された証明の正しさはシステムにより機械的にチェックされるため，プログラムが仕様通りに動作するか等の保証を与える手法の一つとして注目されている．しかし，複雑な証明を人間が考え記述しなければいけないという問題点がある．本研究では，証明の難しさを緩和するために項書換系の理論を応用し，Coqにプラグインとして実装することで証明の部分的な自動化を図る．
