一个面向科学和教育的定理证明器
A Theorem Prover for Scientific and Educational Purposes
摘要：
我们提出了一个原型的综合推理环境的教育目的。所提出的工具是一个片段的证明助手和自动定理证明。我们描述了现有的和计划的定理证明器的功能，特别是教育片段的功能。这目前支持使用无类型的λ演算的术语，并针对本科生和研究人员。我们展示了如何使用该工具来支持学生的理解函数式编程和讨论的一般问题的过程中建立定理证明软件，旨在支持研究和教育。
英文摘要：
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
