OnlineProver: First Experience with Teaching Formal Proofs

Abstract

OnlineProver is an interactive proof checker, tailored for the educational setting. The main features are a user-friendly interface for editing and checking proofs, and a DSL for specifying deduction systems and exercises about them. The user interface
provides feedback directly in the derivation, based on error messages provided by a proof checking web-service. A basic philosophy of the tool, is that it should aid the student, while still maintain that the students construct the proofs as if it was on paper. We gathered feedback on the tool through a questionnaire, and we provide a comprehensive evaluation of its effectiveness, assessing its impact on teaching and learning approaches, along with technical aspects.
The evaluation showed that the students were satisfied with using OnlineProver as part of the teaching and gave a first conformation of the learning approach behind. This gives clear directions for future developments.