Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book

The Intelligent Book project aims to improve online education by designing materials that can model the subject matter they teach, in the manner of a Reactive Learning Environment. In this paper, we investigate using an automated proof assistant, particularly Isabelle/HOL, as the model supporting first year undergraduate exercises in which students write proofs in number theory. Automated proof assistants are generally considered to be difficult for novices to learn. We examine whether, by providing a very specialised interface, it is possible to build something that is usable enough to be of educational value. To ensure students cannot “game the system” the exercise avoids tactic-choosing interaction styles, but asks the student to write out the proof. Proofs are written using MathsTiles: composable tiles that resemble written mathematics. Unlike traditional syntax-directed editors, MathsTiles allow students to keep many answer fragments on the canvas at the same time, and do no...

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: William Billingsley, Peter Robinson
• Keywords: Intelligent Book, Intelligent Book Project, JAR 2007, Proof Assistant