A Modular Formalisation of Finite Group Theory
From MaRDI portal
Publication:3523168
DOI10.1007/978-3-540-74591-4_8zbMath1144.68356OpenAlexW1821564862MaRDI QIDQ3523168
Laurence Rideau, Enrico Tassi, Georges Gonthier, Assia Mahboubi, Laurent Théry
Publication date: 2 September 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00139131v2/file/RR-6156.pdf
Applications of logic to group theory (20A15) Abstract finite groups (20D99) Mechanization of proofs and logical operations (03B35)
Related Items
Completeness and decidability results for CTL in constructive type theory, Unnamed Item, Hints in Unification, Packaging Mathematical Structures, Regular language representations in the constructive type theory of Coq, Computational Complexity Via Finite Types, Unnamed Item, Effective homology of bicomplexes, formalized in Coq, Canonical Big Operators, Generating certified code from formal proofs: a case study in homological algebra, Unnamed Item, Incidence Simplicial Matrices Formalized in Coq/SSReflect, Constructive Mathematics and Functional Programming (Abstract), Point-Free, Set-Free Concrete Linear Algebra, Finite Groups Representation Theory with Coq, A formal study of Bernstein coefficients and polynomials, Classical mathematics for a constructive world, Social processes, program verification and all that, Two-Way Automata in Coq, Constructive Formalization of Hybrid Logic with Eventualities, Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
Uses Software
