Proof Editor for Natural Deduction

Abstract

In this thesis, we present Logan, a proof editor for constructing Fitch-style proofs in first-order logic. This proof editor is intended to be used by students who are taking a course in logic. Compared to other available proof editors Logan aims to be easier to use, both when it comes to getting started and in the continued use of the proof editor. Logan also aims to be more helpful by giving feedback and hints to aid the students in their learning. User testing was conducted on a small sample size of students to evaluate Logan from a usability and user experience perspective to find potential issues. As a result, some usability problems were identified and remedied. The plan is to introduce Logan as a tool in the next instance of the course DAT060/DIT202 Logic in computer science at University of Gothenburg and Chalmers University of Technology. If realized, the deployment of Logan can be seen as beta-testing on a larger sample size of students than the conducted user testing. Thus potential missed bugs can be identified and fixed in future development of Logan.