Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2017

04.10.2016

Fermat, Euler, Wilson - Three Case Studies in Number Theory

verfasst von: Christoph Walther, Nathan Wasser

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We report on computer assisted proofs of three theorems from Number Theory, viz. Fermat’s Little Theorem, Euler’s generalization of Fermat’s statement and Wilson’s Theorem. Common to the formal proofs is that permutation of certain number lists has to be proved, which causes the main effort in the development. We give a short survey of the https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9387-z/MediaObjects/10817_2016_9387_IEq1_HTML.gif   system used in this experiment and illustrate the proofs before presenting them formally. We also discuss alternative solutions, report on the required effort and conclude with some experiences gained from this experiment.
Vorheriger Artikel A Complete Uniform Substitution Calculus for Differential Dynamic Logic

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
An acronym for “A Verifier for Functional Programs”.
 
2
The base of this recursive definition is given by lemmas being proved without using other lemmas.
 
3
In allmost all cases, the induction axiom required for proving a lemma \(\ell \) is provided by one of the procedures used in \(\ell \). However, in rare cases the user must define an additional procedure like \(\mathfrak {\mathfrak {R}}\) for stipulating a specific induction axiom, either because this is needed or (as in the present case) eases a proof considerably.
 
4
Unfortunately, we did not succeed completely in hiding system internals, as there are 2 “tricks” in the formulation of lemmas which support automated equality reasoning, see Sect. 2.1 for a discussion.
 
5
\(x\ne 0\) is demanded in (1) as otherwise \(0^{0}\) has to be defined.
 
6
\({\mathbb {P}}(p)\) denotes that p is prime.
 
7
Here we use mathematical notation like \(\sum \nolimits _{i=1}^{m+1}\left( {\begin{array}{c}n\\ i-1\end{array}}\right) \cdot x^{i}\) instead of \(S(m+1,n,1,x)\) for sake of readability.
 
8
The use of (6) is not a “hack” for supporting the system, as lemma (1) has an automatic proof as well. But it is good practice in mathematics to formulate proofs as simple as possible, and this principle applies to formal reasoning in particular (saving a lemma in the present case).
 
9
Instead of constructor induction with a step case \(\forall n: {\mathbb {N}\,} \varphi (n)\rightarrow \varphi (n+1)\), https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9387-z/MediaObjects/10817_2016_9387_IEq98_HTML.gif   uses destructor induction with a step case \(\forall n:{\mathbb {N}\,} n\ne 0\wedge \varphi (n-1)\rightarrow \varphi (n)\) as the latter is more general. For instance, there is no constructive counterpart for the induction schema obtained from procedure \(\mathfrak {\mathfrak {R}}\) of Sect. 1.
 
10
As usual, \((x\equiv y)\,{\textit{mod}}\,z\) stands for \(x\,{\textit{mod}}\,z=y\,{\textit{mod}}\,z\).
 
11
As https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9387-z/MediaObjects/10817_2016_9387_IEq162_HTML.gif   does not provide a data structure set, we had to use lists in our formal proof. If sets were present, \(purged(\ldots )\) had to be replaced by \(\mathtt {true}\) and \(\approx \) by \(=\) in the lemmas, so that the lemmas (25) and (31) would become needless. This means that the use of lists does not complicate the proof, as only 1 user interaction for proving (25) and 2 user interactions for proving (31) could be saved. In the subsequent proofs of Sects. 2.3 and 3, only lemma (31) would become needless, reducing the savings even more.
 
12
Time refers to running https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9387-z/MediaObjects/10817_2016_9387_IEq172_HTML.gif   3.5 under Windows 7 Enterprise with an INTEL Core i7-2640M 2.80 GHz CPU using Java 1.8.0_45.
 
13
p being prime is not only suffcient but also necessary for the statement to hold as \((n-1)!\,{\textit{mod}}\,n\ne n-1\) for all non-primes \(n\ne 1\) . See [1] for a computer assisted proof.
 
14
As it happens, the residue classes modulo a prime form a field, however this more general fact is not needed here.
 
15
But we may ban the execution of procedure calls in a case term or in an instance of a lemma upon use of Case Analysis or Use Lemma respectively. We may also use the HPL-rule Normalization working like Simplification, except that procedure calls in the goalterm are not executed.
 
16
\(\subseteq \) denotes the subset relation which neither considers the order of list elements nor the number of element occurrences when comparing lists. For instance, \(\left( 3,2\right) \subseteq \left( 2,2,3\right) \) and vice versa.
 
17
Proofs of \(\sim \)16.000 theorems had been reported in [5], where \(\sim \)3800 were proven by automated induction and \(\sim \)1000 by user suggested induction.
 
18
For the case studies in Table 1, the success rate of the induction heuristic / the share of first-order provable lemmas ranges from \(93\,\%/32\,\%\) in the Fermat proof using the Pigeon Hole Principle to \(97\,\%/35\,\%\) when using the Binomial Theorem, and is 94–96 %/31–33 \(\%\) for the remaining proofs.
 
19
See e.g. the definition of primes and the required loop invariant called prime1.basic in [2].
 
Literatur
1.
2.
Boyer, R.S., Moore, JS.: A Computational Logic. Academic Press, New York (1979)
3.
Boyer, R.S., Moore, JS.: Proof checking the RSA public key encryption algorithm. Am. Math. Mon. 91(3), 181–189 (1984)
4.
Boyer, R.S., Moore, JS.: A theorem prover for a computational logic (keynote address). In: Proceedings of 10th International Conference on Automated Deduction (CADE-10). Lecture Notes in Computer Science, vol. 449, pp. 1–15, Kaiserslautern (1990)
5.
Boyer, R.S., Moore, JS.: On the difficulty of automating inductive reasoning. Remarks made at a CADE-11 Workshop on Inductive Reasoning, Saratoga Springs (1992)
6.
Dickson, L.E.: History of the theory of numbers. In: Divisibility and Primality. vol 1, Carnegie Institution of Washington, Publication No. 256, Washington (1919)
7.
Rasmussen, T.M.: An inductive approach to formalizing notions of number theory proofs. In: Computer Mathematics: Proceedings of the 5th Asian Symposium (ASCM 2001), Matsuyama, Japan pp. 131–140 (2001)
8.
Rosen, K.H.: Elementary Number Theory and Its Applications, 5th edn. Pearson Addison Wesley, Boston (2005)
9.
Russinoff, D.M.: An experiment with the Boyer–Moore theorem prover: A proof of Wilson’s theorem. J. Autom. Reason. 1(2), 121–139 (1985)MathSciNetCrossRefMATH
10.
11.
Walther, C., Schweitzer, S.: Verification in the classroom. J. Autom. Reason. 32(1), 35–73 (2004)CrossRef
12.
Walther, C., Schweitzer, S.: A pragmatic approach to equality reasoning. Technical Report VFR 06/02, Technische Universität Darmstadt, pp. 1–19 (2006) (available from [1])
13.
14.
15.
Metadaten
Titel
Fermat, Euler, Wilson - Three Case Studies in Number Theory
verfasst von
Christoph Walther
Nathan Wasser
Publikationsdatum
04.10.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9387-z

Premium Partner

    Bildnachweise