Loading...
Please wait, while we are loading the content...
Similar Documents
An Inductive Approach to Formalizing Notions of Number Theory Proofs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Rasmussen, Thomas Marthedal |
| Copyright Year | 2001 |
| Abstract | In certain proofs of theorems of, e.g., number theory and the algebra of finite fields, one-to-one correspondences and the “pairing off” of elements often play an important role. In textbook proofs these concepts are often not made precise but if one wants to develop a rigorous formalization they have to be. We have, using an inductive approach, developed constructs for handling these concepts. We illustrate their usefulness by considering formalizations of Euler-Fermat’s and Wilson’s Theorems. The formalizations have been mechanized in Isabelle/HOL, making a comparison with other approaches possible. |
| Starting Page | 131 |
| Ending Page | 140 |
| Page Count | 10 |
| File Format | PDF HTM / HTML |
| DOI | 10.1142/9789812799661_0014 |
| Alternate Webpage(s) | http://www.imm.dtu.dk/~tmr/num-tphols2001.ps |
| Alternate Webpage(s) | http://www.imm.dtu.dk/~tmr/num-ascm2001.ps |
| Alternate Webpage(s) | http://www.inf.ed.ac.uk/publications/online/0046/b328.pdf |
| Alternate Webpage(s) | https://doi.org/10.1142/9789812799661_0014 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |