A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L

DOI10.1023/A:1006269330992zbMath0943.68149OpenAlexW1488122270WikidataQ56092193 ScholiaQ56092193MaRDI 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

zbMATH Keywords

Isabelle HOL

Mathematics Subject Classification ID

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 (4)

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

• PVS
• Automath
• IMPS
• Locales
• Secondary Sylow
• Unnamed Item
• Unnamed Item

This page was built for publication: A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L