  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.
