caa a22 4500 463182952 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10817-007-9072-3 doi (NATIONALLICENCE)springer-10.1007/s10817-007-9072-3 Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book [Elektronische Daten] [William Billingsley, Peter Robinson] 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. Springer Science+Business Media, Inc., 2007 Intelligent book nationallicence MathsTiles nationallicence Isabelle nationallicence Billingsley William University of Cambridge, Cambridge, England, UK aut Robinson Peter University of Cambridge, Cambridge, England, UK aut Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 181-218 0168-7433 39:2<181 2007 39 10817 https://doi.org/10.1007/s10817-007-9072-3 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9072-3 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Billingsley William University of Cambridge, Cambridge, England, UK aut NATIONALLICENCE 700 1- Robinson Peter University of Cambridge, Cambridge, England, UK aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 181-218 0168-7433 39:2<181 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer