Computer Laboratory

Technical reports

The Intelligent Book: technologies for intelligent and adaptive textbooks, focussing on Discrete Mathematics

William H. Billingsley

June 2008, 156 pages

This technical report is based on a dissertation submitted April 2007 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Wolfson College.


An “Intelligent Book” is a Web-based textbook that contains exercises that are backed by computer models or reasoning systems. Within the exercises, students work using appropriate graphical notations and diagrams for the subject matter, and comments and feedback from the book are related into the content model of the book. The content model can be extended by its readers. This dissertation examines the question of how to provide an Intelligent Book that can support undergraduate questions in Number Theory, and particularly questions that allow the student to write a proof as the answer. Number Theory questions pose a challenge not only because the student is working on an unfamiliar topic in an unfamiliar syntax, but also because there is no straightforward procedure for how to prove an arbitrary Number Theory problem.

The main contribution is a system for supporting student-written proof exercises, backed by the Isabelle/HOL automated proof assistant and a set of teaching scripts. Students write proofs using MathsTiles: a graphical notation consisting of composable tiles, each of which can contain an arbitrary piece of mathematics or logic written by the teacher. These tiles resemble parts of the proof as it might be written on paper, and are translated into Isabelle/HOL’ws Isar syntax on the server. Unlike traditional syntax-directed editors, MathsTiles allow students to freely sketch out parts of an answer and do not constrain the order in which an answer is written. They also allow details of the language to change between or even during questions.

A number of smaller contributions are also presented. By using the dynamic nature of MathsTiles, a type of proof exercise is developed where the student must search for the statements he or she wishes to use. This allows questions to be supported by informal modelling, making them much easier to write, but still ensures that the interface does not act as a prop for the answer. The concept of searching for statements is extended to develop “massively multiple choice” questions: a mid-point between the multiple choice and short answer formats. The question architecture that is presented is applicable across different notational forms and different answer analysis techniques. The content architecture uses an informal ontology that enables students and untrained users to add and adapt content within the book, including adding their own chapters, while ensuring the content can also be referred to by the models and systems that advise students during exercises.

Full text

PDF (3.2 MB)

BibTeX record

  author =	 {Billingsley, William H.},
  title = 	 {{The Intelligent Book: technologies for intelligent and
         	   adaptive textbooks, focussing on Discrete Mathematics}},
  year = 	 2008,
  month = 	 jun,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-719}