Formalising Sylow's theorems in Coq

Simple item page
dc.creatorThery, Laurent
dc.date2006-11-14
dc.date.accessioned2026-07-07T07:31:42Z
dc.date.available2026-07-07T07:31:42Z
dc.descriptionThis report presents a formalisation of Sylow's theorems done in {\sc Coq}. The formalisation has been done in a couple of weeks on top of Georges Gonthier's {\sc ssreflect} \cite{ssreflect}. There were two ideas behind formalising Sylow's theorems. The first one was to get familiar with Georges way of doing proofs. The second one was to contribute to the collective effort to formalise a large subset of group theory in {\sc Coq} with some non-trivial proofs.}
dc.identifierhttps://arxiv.org/abs/cs/0611057
dc.identifierhttp://arxiv.org/abs/cs/0611057
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/118847
dc.subjectLogic in Computer Science
dc.titleFormalising Sylow's theorems in Coq
dc.typetext

Files

Collections

arXiv