论文标题
Isabelle功能上的Lucas解释
Lucas-Interpretation on Isabelle's Functions
论文作者
论文摘要
自动推理的软件工具过于复杂，无法在数学教育和各自的推理中进行一般使用，而卢卡斯解关则提供了一个一般概念，可以将这些工具集成到教育软件中，以便可靠，灵活地检查学生的正式输入。本文在将原型实施迁移到证明助手Isabelle的功能包中时，对Lucas解释的技术简洁描述。该描述显示了Isabelle的编程语言的直接改编，并显示了解释器的简单迁移，因为设计（在将功能软件包介绍给Isabelle之前）认可了Isabelle作为中端的术语的适当性。本文将链接链接到公开存储库中的代码中，以邀请读者重新使用原型代码或采用一般概念。而且，由于在实现功能包之前已经设计了原型，因此本文是从Isabelle的代码结构开发中学到的经验教训的机会。
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-Interpretation 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 package was implemented, the paper is an opportunity for recording lessons learned from Isabelle's development of code structure.
