Supervisor: Alan Bundy, +44-131-650-2716, A.Bundy@ed.ac.uk
Other Suggested Supervisors: Jacques Fleuriot, +44-131-650-9342, jdf@inf.ed.ac.uk
Principal goal of the project: To build a teaching aid that will support students in performing proofs in nonstandard analysis.
Description:
Reasoning with epsilon arguments in analysis is one of the hardest tasks that student mathematicians have to tackle as most of them find it hard to deal with formulae containing more than two alternations of quantifiers. This is not surprising as it has been observed that the manipulation of quantifiers is ``one of the least often acquired and most rarely understood concepts at all levels''. Most students (and teachers) still find it congenial to think informally in terms of infinitesimal numbers.
Nonstandard analysis (NSA) is a definitional theory of extended reals which supports reasoning about analysis, calculus, etc using infinitesimal and infinite numbers. It was invented by the logician Abraham Robinson in the 1960s. NSA provides an alternative to the traditional epsilon/delta proofs, but with the following advantages:
An obvious solution to the problems of teaching standard analysis is to teach NSA rather than traditional analysis. Apart from inertia, one main barrier to switching to NSA is that naive NSA proofs can be as prone to error as the original infinitesimal proofs. This is where mechanical theorem proving comes in. If students had access to a computer-based tool for checking and/or generating NSA proofs they could be freed of the risk of error. The full benefits of NSA could then be realised: simpler definitions, theorems and proofs, more in accord with school-level introductions to calculus and, to some, more intuitive.
For his Cambridge PhD project, Fleuriot implemented a theory of NSA in the higher-order logic of the interactive theorem prover Isabelle, using purely definitional means. This mechanization, which develops the so-called hyperreal numbers, asserts no axioms and progresses by conservative extensions of Isabelle/HOL theories only. Since coming to Edinburgh, Fleuriot has continued his development of NSA in Isabelle, covering a large part of analysis and the development of both differential and integral calculus. He has interactively proved several thousands of theorems in real analysis, including some well-known theorems, such as Rolles Theorem, the Intermediate Value Theorem, and the Fundamental Theorem of Calculus.
Fleuriot has supervised the PhD of Maclean, in which many of these NSA proofs are further automated using techniques of proof planning, especially rippling. As a result, human interaction is no longer necessary to produce machine proofs of many elementary NSA theorems.
The aim of this project is to develop a teaching aid based on a powerful, fully-programmable theorem proving core (provided by Isabelle) that provides the necessary theories, tactics and programming environment and protects users from error.
Resources Required: Access to the Isabelle system, tactics to automate NSA proofs and a library of NSA theorems and proofs.
Degree of Difficulty: This is a challenging project combining knowledge of mathematics with automated reasoning and computers in education.
Background Needed: Knowledge of mathematical analysis is essential. Knowledge of any of automated reasoning, non-standard analysis, computers in education or the ML programming language would be an advantage.
References: