在Coq中形式化Sylow定理
摘要：在《Coq》中对Sylow定理进行了形式化。这个形式化工作是在Georges Gonthier的ssreflect之上完成的，并花了几周的时间。形式化Sylow定理的目的有两个。第一，熟悉Georges的证明方法。第二，为在Coq中形式化群论的一个较大子集并做出一些非平凡的证明做出贡献。
作者：Laurent Thery (INRIA Sophia Antipolis)
论文ID：cs/0611057
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23