定理証明支援系に興味を持ったが，特に証明したい定理があるとか数学に生かしたいといった目的はないので，仕組みを知るためにゼロから作ってみる．定理証明支援系といっても様々だが，ここでは主にCoqを念頭において話を進める．
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。
