Proof Editor for Natural Deduction in First-order Logic

Abstract

The subject of this thesis is the presentation and evaluation of Conan, an editor for writing natural deduction proofs in first-order logic. The intent is for the editor to serve as a supplementary tool alongside a course in logic. For this reason, emphasis was put on making sure the editor would have a low learning curve, ensuring that learning to use it would not take away from the limited time in a typical university course. Though editors for writing this kind of proof already exist, they are often cumbersome or difficult to use. A pre-study was conducted to determine that there is indeed a lack of editors that fulfil the requirements set forth in this thesis. The interface of Conan was evaluated both heuristically using Jakob Nielsen’s heuristics and also through limited user tests. This evaluation suggested that the interface was easy to use, quick to learn and that students were positive toward using the editor for writing proofs. We also present arguments for why Conan would be an aid from the perspective of pedagogy, though no in-depth research on this matter was conducted.