arXiv 1507.040022015-07-14cs.CYcs.LO

NaDeA：Isabelle中形式化的自然演绎助手

NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle

Jørgen Villadsen, Alexander Birch Jensen, Anders Schlichtkrull

备注：: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, João Marcos, María Manzano, Sophie Pinchinat, François Schwarzentruber

摘要：

我们提出了一个新的软件工具，用于教学逻辑的基础上自然演绎。它的证明系统在证明助手Isabelle中得到了形式化的描述，使得它的定义非常精确。形式化的合理性已在Isabelle中得到证明。该工具是用TypeScript / JavaScript开发的开源软件，因此可以直接在浏览器中使用，无需进一步安装。虽然开发的本科计算机科学的学生谁是用来学习和编程具体的计算机代码在程序设计语言，我们认为相关的方法为更广泛的受众和其他证明系统。

英文摘要：

We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in Isabelle. The tool is open source software developed in TypeScript / JavaScript and can thus be used directly in a browser without any further installation. Although developed for undergraduate computer science students who are used to study and program concrete computer code in a programming language we consider the approach relevant for a broader audience and for other proof systems as well.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。