Isabelle/PIDE作为教育工具的平台
Isabelle/PIDE as Platform for Educational Tools
摘要：
Isabelle/PIDE平台解决了LCF系列的证明助手是否适合作为教育工具的技术基础的问题。像HOL、Coq或Isabelle这样的系统传统上强大的逻辑基础到目前为止已经被TTY（或像著名的Proof General / Emacs接口这样的小变体）的一些不可访问的交互所抵消。因此，数学教育工具与完全正式的背景理论的基本问题，往往是否定的回答，由于现有的证明引擎偶然的弱点。“PIDE”（意为“ProverIDE”）的理念是将现有的证明器（如Isabelle）集成到一个更大的环境中，以方便最终用户和其他工具的访问。我们使用Scala将ML中的证明引擎公开给JVM世界，那里已经存在许多用户界面、编辑器框架和教育工具。这将最终导致组合数学助手，其中逻辑引擎是在后台，而不妨碍形式化方法，形式化数学，特别是数学教育的应用程序的看法。
英文摘要：
The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have so far been counter-balanced by somewhat inaccessible interaction via the TTY (or minor variations like the well-known Proof General / Emacs interface). Thus the fundamental question of math education tools with fully-formal background theories has often been answered negatively due to accidental weaknesses of existing proof engines. The idea of "PIDE" (which means "Prover IDE") is to integrate existing provers like Isabelle into a larger environment, that facilitates access by end-users and other tools. We use Scala to expose the proof engine in ML to the JVM world, where many user-interfaces, editor frameworks, and educational tools already exist. This shall ultimately lead to combined mathematical assistants, where the logical engine is in the background, without obstructing the view on applications of formal methods, formalized mathematics, and math education in particular.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
