Proof Editor for Natural Deduction
Ladda ner
Typ
Examensarbete på kandidatnivå
Program
Publicerad
2021
Författare
ABRAHAMSSON, FREDDY
ANDERSSON, THERESE
FORSMAN, AXEL
RANTA, LO
ÅKESSON, MICHAEL
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Proof editor , Natural deduction , First order logic , PureScript