Please use this identifier to cite or link to this item:
https://hdl.handle.net/1959.11/22401
Title: | Student proof exercises using MathsTiles and isabelle/HOL in an intelligent book | Contributor(s): | Billingsley, William (author) ; Robinson, Peter (author) | Publication Date: | 2007 | Open Access: | Yes | DOI: | 10.1007/s10817-007-9072-3 | Handle Link: | https://hdl.handle.net/1959.11/22401 | 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 0168-7433 |
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:
File | Description | Size | Format | |
---|---|---|---|---|
open/SOURCE02.pdf | Post-peer review version | 1.26 MB | Adobe PDF Download Adobe | View/Open |
SCOPUSTM
Citations
18
checked on Oct 26, 2024
Page view(s)
1,484
checked on Nov 19, 2023
Download(s)
332
checked on Nov 19, 2023
Items in Research UNE are protected by copyright, with all rights reserved, unless otherwise indicated.