A string of pearls: Proofs of Fermat's Little Theorem
Date
2012
Authors
Chan, Hing Lun (Joseph)
Norrish, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Conference Organising Committee
Abstract
We discuss mechanised proofs of Fermat's Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial necklace proof that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for the direct number-theoretic approach.
Description
Keywords
Keywords: Artificial intelligence; Theorem proving
Citation
Collections
Source
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description