Formalizing Moessner's theorem and generalizations in \textsc{Nuprl}

DOI10.1016/J.JLAMP.2021.100713OpenAlexW3194152347MaRDI QIDQ2667184

Alexandra Silva, Dexter Kozen, Mark Bickford

Publication date: 24 November 2021

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2021.100713

zbMATH Keywords

Pascal triangleformalizationMoessner's theoremNuprl

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Special sequences and polynomials (11B83) Formal power series rings (13F25)

Related Items (1)

A tribute to José Manuel Valença

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A proof of Moessner's theorem by coinduction
• Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
• On Moessner’s Theorem
• On the Moessner Theorem on Integral Powers

This page was built for publication: Formalizing Moessner's theorem and generalizations in \textsc{Nuprl}