UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Formalizing Moessner's theorem and generalizations in Nuprl

Bickford, M; Kozen, D; Silva, A; (2022) Formalizing Moessner's theorem and generalizations in Nuprl. Journal of Logical and Algebraic Methods in Programming , 124 , Article 100713. 10.1016/j.jlamp.2021.100713.

[thumbnail of Moessner-Nuprl.pdf] Text
Moessner-Nuprl.pdf - Accepted Version
Access restricted to UCL open access staff until 24 August 2022.

Download (288kB)

Abstract

Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^{n}, 2^{n}, 3^{n},...Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its known generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl. On the one hand, the formalization remains remarkably close to the original proof. On the other hand, it leads to new insights in the proof, pointing to small gaps and ambiguities that would never raise any objections in pen and pencil proofs, but which must be resolved in machine formalization.

Type: Article
Title: Formalizing Moessner's theorem and generalizations in Nuprl
DOI: 10.1016/j.jlamp.2021.100713
Publisher version: https://doi.org/10.1016/j.jlamp.2021.100713
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher's terms and conditions.
Keywords: Moessner's theorem, Pascal triangle, Formalization, Nuprl
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10139900
Downloads since deposit
1Download
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item