论文标题
一种自我引导的正式推理研究应用程序
A Mobile Application for Self-Guided Study of Formal Reasoning
论文作者
论文摘要
在这项工作中，我们介绍了Axolotl，这是一种自学援助，旨在指导学生介绍正式推理和任期操纵的基础知识。与大多数现有的正式推理研究辅助工具不同，Axolotl是一种基于Android的应用，具有简单的基于触摸的界面。设计目标的一部分是最大程度地减少分散学习过程的用户错误的可能性。例如错别字或提供规则的不一致。该系统包括一个可缩放的证明查看器，该查看器显示到迄今为止所取得的进展，并允许将完整的证明存储为JPEG或乳胶文件。该软件可在Google Play商店中找到，并带有一个小问题。可以使用简单的输入语言在Axolotl中打开其他问题。当前，Axolotl支持可以使用将单个表达式转换为一组表达式的规则来解决的问题。这涵盖了我们在逻辑课程的第一学期介绍中发现的教育方案，并有助于弥合命题和一阶推理之间的差距。未来的发展将包括重写规则，这些规则采用一组表达式并返回一组表达式以及量化的一阶扩展。
In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.
