Proof Editor for Natural Deduction

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
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material