A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
From MaRDI portal
Publication:1961914
DOI10.1023/A:1006269330992zbMath0943.68149OpenAlexW1488122270MaRDI QIDQ1961914
Florian Kammüller, Lawrence Charles Paulson
Publication date: 11 September 2000
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006269330992
Subgroup theorems; subgroup growth (20E07) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to group theory (20-04)
Related Items
Verification of the Miller-Rabin probabilistic primality test. ⋮ A mechanized proof of the basic perturbation lemma ⋮ Formalizing non-interference for a simple bytecode language in Coq ⋮ Generating certified code from formal proofs: a case study in homological algebra
Uses Software
