Properties of the Hebrew Calendar

David M. Russinoff

We describe an ACL2 program that implements the Hebrew calendar and the formal verification of several of its properties, including the critical result that the algorithm that determines the placement of the new year ensures that the length of every year belongs to a small set of admissible values. These properties have been accepted for many centuries without the benefit of explicit proof, in spite of subtleties in the underlying arguments. For the sake of accessibility to a broad audience, the program is coded in Restricted Algorithmic C (RAC), a simple language consisting of the most basic constructs of C, for which an automatic translator to the ACL2 logic has been implemented. While RAC is primarily intended for modeling arithmetic hardware designs, this novel application provides a relatively simple illustration of the language and the translator.

In Rob Sumners and Cuong Chau: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2022), Austin, Texas, USA, 26th-27th May 2022, Electronic Proceedings in Theoretical Computer Science 359, pp. 48–60.
Published: 24th May 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: