BUDGE: A PROGRAMMING LANGUAGE AND A THEOREM PROVER
DOI:
https://doi.org/10.17605/OSF.IO/X7654Keywords:
Programming language, theorem prover, computational model, Godel numberingAbstract
We present a simple programming language based on Godel numbering and prime factorization, enhanced with explicit, scoped loops, allowing for easy program composition. Further, we will present a theorem prover that allows expressing and working with formal systems. The theorem prover is simple as it relies merely on a substitution rule and set equality to derive theorems. Finally, we will represent the programming language in the theorem prover. We will show the syntax and semantics of both, and then provide a few example programs and their evaluation.
References
1. Hofstadter, Douglas R. Godel, Escher, Bach: An Eternal Golden Braid¨. New York: Basic books, 1979.
2. Korniłowicz, Artur, and Piotr Rudnicki. ”Fundamental Theorem of Arithmetic.” Formalized Mathematics 12, no. 2 (2004): 179-186.
3. Conway, John H.”Fractran: A simple universal programming language for arithmetic.” In Open problems in Communication and Computation, pp. 4-26. Springer, New York, NY, 1987.
4. McCracken, Daniel D., and Edwin D. Reilly. ”Backus-Naur Form (BNF).” In Encyclopedia of Computer Science, pp. 129-131. 2003.
5. Clocksin, William F., and Christopher S. Mellish. Programming in Prolog. Springer Science & Business Media, 2003.
6. Velleman, Daniel J. How to Prove It: A Structured Approach. Cambridge University Press, 2019.
7. Sitnikovski, B. Budge programming language and theorem prover (Python implementation). [Online]. Available: https://github.com/bor0/budge/ (Accessed Aug. 2022)
2. Korniłowicz, Artur, and Piotr Rudnicki. ”Fundamental Theorem of Arithmetic.” Formalized Mathematics 12, no. 2 (2004): 179-186.
3. Conway, John H.”Fractran: A simple universal programming language for arithmetic.” In Open problems in Communication and Computation, pp. 4-26. Springer, New York, NY, 1987.
4. McCracken, Daniel D., and Edwin D. Reilly. ”Backus-Naur Form (BNF).” In Encyclopedia of Computer Science, pp. 129-131. 2003.
5. Clocksin, William F., and Christopher S. Mellish. Programming in Prolog. Springer Science & Business Media, 2003.
6. Velleman, Daniel J. How to Prove It: A Structured Approach. Cambridge University Press, 2019.
7. Sitnikovski, B. Budge programming language and theorem prover (Python implementation). [Online]. Available: https://github.com/bor0/budge/ (Accessed Aug. 2022)
Downloads
Published
2023-04-21
How to Cite
Sitnikovski, B. . (2023). BUDGE: A PROGRAMMING LANGUAGE AND A THEOREM PROVER. CENTRAL ASIAN JOURNAL OF MATHEMATICAL THEORY AND COMPUTER SCIENCES, 4(4), 41–45. https://doi.org/10.17605/OSF.IO/X7654
Issue
Section
Articles
