Lucas-Interpretation on Isabelle's Functions

Walther Neuper
(Johannes Kepler University Linz, Austria)

Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with the purpose to reliably and flexibly check formal input of students.

This paper gives the first technically concise description of Lucas-Interpre- tation at the occasion of migrating a prototype implementation to the function package of the proof assistant Isabelle. The description shows straightforward adaptations of Isabelle's programming language and shows, how simple migration of the interpreter was, since the design (before the function package has been introduced to Isabelle) recognised appropriateness of Isabelle's terms as middle end.

The paper gives links into the code in an open repository as invitation to readers for re-using the prototyped code or adopt the general concept. And since the prototype has been designed before the function pack- age was implemented, the paper is an opportunity for recording lessons learned from Isabelle's development of code structure.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328, pp. 79–95.
Published: 30th October 2020.

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