A Mobile Application for Self-Guided Study of Formal Reasoning

David M. Cerna
(Research Institute For Symbolic Computation)
Rafael P.D. Kiesel
(Knowlege Based Systems, Technical University of Vienna)
Alexandra Dzhiganskaya
(University of Applied Arts Vienna)

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.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software (ThEdu'19), Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313, pp. 35–53.
Published: 28th February 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.313.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org