一个形式推理自主学习的移动应用
A Mobile Application for Self-Guided Study of Formal Reasoning
摘要：
在这项工作中，我们介绍AXolotl，旨在引导学生通过形式推理和术语操作的基础知识自学援助。与大多数现有的正式推理学习辅助工具不同，AXolotl是一个基于Android的应用程序，具有简单的触摸式界面。设计目标的一部分是尽量减少用户错误的可能性，这些错误会分散学习过程的注意力。例如错别字或所提供规则的不一致应用。该系统包括一个可缩放的校样查看器，它显示到目前为止所取得的进展，并允许将完成的校样存储为JPEG或LaTeX文件。这款软件可以在google play store上买到，并附带了一个小的问题库。可以使用简单的输入语言在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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
