Proof Editor for Natural Deduction in First-order Logic

University essay from Göteborgs universitet/Institutionen för data- och informationsteknik

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

  AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)