Please use this identifier to cite or link to this item:
Title: Student proof exercises using MathsTiles and isabelle/HOL in an intelligent book
Contributor(s): Billingsley, William  (author)orcid ; Robinson, Peter (author)
Publication Date: 2007
Open Access: Yes
DOI: 10.1007/s10817-007-9072-3
Handle Link:
Abstract: 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 specialized 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 allows students to keep many answer fragments on the canvas at the same time and does not constrain the order in which an answer is written. Also, the tile syntax does not need to match the underlying Isar syntax exactly, and different tiles can be used for different questions. The exercises take place within the context of an Intelligent Book. We performed a user study and qualitative analysis of the system. Some users were able to complete proofs with much less training than is usual for the automated proof assistant itself, but there remain significant usability issues to overcome.
Publication Type: Journal Article
Source of Publication: Journal of Automated Reasoning, 39(2), p. 181-218
Publisher: Springer Netherlands
Place of Publication: Netherlands
ISSN: 1573-0670
Fields of Research (FoR) 2008: 130306 Educational Technology and Computing
080199 Artificial Intelligence and Image Processing not elsewhere classified
080602 Computer-Human Interaction
Socio-Economic Objective (SEO) 2008: 970108 Expanding Knowledge in the Information and Computing Sciences
890299 Computer Software and Services not elsewhere classified
930203 Teaching and Instruction Technologies
Peer Reviewed: Yes
HERDC Category Description: C1 Refereed Article in a Scholarly Journal
Appears in Collections:Journal Article
School of Science and Technology

Files in This Item:
5 files
File Description SizeFormat 
open/SOURCE02.pdfPost-peer review version1.26 MBAdobe PDF
Download Adobe
Show full item record
Google Media

Google ScholarTM



Items in Research UNE are protected by copyright, with all rights reserved, unless otherwise indicated.