Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell OConnor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013):
A Machine-Checked Proof of the Odd Order Theorem.
In: International Conference on Interactive Theorem Proving,
pp. 163–179,
doi:10.1017/S0960129511000132.
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi & Laurent Théry (2007):
A Modular Formalisation of Finite Group Theory.
Technical Report RR-6156.
Inria.
Jónathan Heras, Francisco Martín-Mateos & Vico Pascual (2015):
Modelling Algebraic Structures and Morphisms in ACL2.
Applicable algebra in engineering, communication and computing 26(3),
pp. 277–303,
doi:10.1007/s00200-015-0252-9.
Warren Hunt, Robert Krug & J Moore (2003):
Linear and Nonlinear Arithmetic in ACL2.
In: Daniel Geist & Enrico Tronci: Correct Hardware Design and Verification Methods.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 319–333,
doi:10.1145/2422.322411.
Joseph Rotman (1965):
The Theory of Groups: An Introduction.
Allyn and Bacon.
Eric Smith:
A Formalization of Groups.
books/kestrel/algebra/groups-encap.lisp, ACL2 repository.
Yuan Yu (1990):
Computer Proofs in Group Theory.
Journal of Automated Reasoning 6(3),
doi:10.1007/BF00244488.
eptcs@eptcs.org