Zobrazeno 1 - 7
of 7
pro vyhledávání: '"Hing Lun Chan"'
Autor:
Hing Lun Chan, Michael Norrish
Publikováno v:
Journal of Formalized Reasoning, Vol 6, Iss 1, Pp 63-87 (2013)
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 mechani
Externí odkaz:
https://doaj.org/article/c585e2e2e6ae41489a10fcf0369be5b6
Autor:
Michael Norrish, Hing Lun Chan
Publikováno v:
Journal of Automated Reasoning. 65:205-256
The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem pr
Autor:
Hing-Lun Chan, Michael Norrish
Publikováno v:
Journal of Automated Reasoning. 63:667-693
We present a formalisation of the theory of finite fields, from basic axioms to their classification, both existence and uniqueness, in HOL4 using the notion of subfields. The tools developed are applied to the characterisation of subfields of finite
Autor:
Hing Lun Chan
The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence "proof from the Book". Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a fin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e51ec85a091eebc035d3dcb5b9692567
Autor:
Hing Lun Chan, Michael Norrish
Publikováno v:
Interactive Theorem Proving ISBN: 9783319431437
ITP
ITP
We present a proof of the fact that \(2^{n} \le {{\mathrm{lcm}}}\{1, 2, 3, \dots , (n+1)\}\). This result has a standard proof via an integral, but our proof is purely number theoretic, requiring little more than list inductions. The proof is based o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3ea4cce86d8849adf0b4d1d4fc22de13
https://doi.org/10.1007/978-3-319-43144-4_9
https://doi.org/10.1007/978-3-319-43144-4_9
Autor:
Michael Norrish, Hing Lun Chan
Publikováno v:
Interactive Theorem Proving ISBN: 9783319221014
ITP
ITP
The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result proving “PRIMES in P”, as well as a brilliant application of ideas from finite fields. This paper describes the first step towards the goal of a full mechanisati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9a38e3e34c694beb67f1bad6c44628ef
https://doi.org/10.1007/978-3-319-22102-1_8
https://doi.org/10.1007/978-3-319-22102-1_8
Autor:
Michael Norrish, Hing Lun Chan
Publikováno v:
Certified Programs and Proofs ISBN: 9783642353079
CPP
CPP
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 mechanic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f7c72872adcabe71e11135cc7868fb8d
https://doi.org/10.1007/978-3-642-35308-6_16
https://doi.org/10.1007/978-3-642-35308-6_16