Simple Search

Query:

Enter a query and click »Search«...

Format:

Display: entries per page entries

Zbl 0943.68149
Kammüller, Florian; Paulson, Lawrence C.
A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L. (English)
[J] J. Autom. Reasoning 23, No.3-4, 235-264 (1999). ISSN 0168-7433; ISSN 1573-0670/e

Summary: The theorem of Sylow is proved in Isabelle H0L. We follow the proof by Wielandt that is more general than the original and uses a nontrivial combinatorial identity. The mathematical proof is explained in some detail, leading on to the mechanization of group theory and the necessary combinatorics in Isabelle. We present the mechanization of the proof in detail, giving reference to theorems contained in an appendix. Some weak points of the experiment with respect to a natural treatment of abstract algebraic reasoning give rise to a discussion of the use of module systems to represent abstract algebra in theorem provers. Drawing from that, we present tentative ideas for further research into a section concept for Isabelle.

MSC 2000:: *68T15 Theorem proving
03B35 Mechanical theorem proving
20E07 Subgroup theorems (group theory)
20-04 Machine computation, programs (group theory)

Keywords: Isabelle HOL

Comment on this Item PDF MathML XML ASCII DVI PS BibTeX Online Ordering Article Journal

	Scientific prize winners of the ICM 2010
	Overhang
	Lie groups, physics and geometry. An introduction for physicists, engineers and chemists.

Simple Search

Zentralblatt MATH Berlin [Germany]