Supervisor: Alan Bundy, +44-131-650-2716, A.Bundy@ed.ac.uk
Other Suggested Supervisors: Roy McCasland, +44-131-650-2702, rmccasla@inf.ed.ac.uk
Principal goal of the project: To build a tool to assist a mathematician to manage a large corpus of proofs.
Description:
Interactive proof systems, such as Isabelle, PVS, HOL, Coq, Nuprl, etc, allow the development of large corpora of theorems and their proofs: sometimes running into thousands of proofs. The principal users of such systems, to date, have been computer scientists interested in the automatic verification of ICT systems. The proof obligations arising from formal methods tend to yield large (but not deep) theorems and even larger proofs. There is also increasing interest from research mathematicians, but the tools are not yet suitable for widespread use by non-computer scientists. This project is to address one of the deficiencies that prevent wider uptake.
To manage a large corpus of proofs, it is necessary to impose structure on it and to provide tools to browse and manipulate it. For instance, each proof step depends on previously proved theorems, axioms, rules of inference, definitions, etc. After many thousands of proofs, the user may realise that a slightly different definition or axiom would have and will make his/her job much easier. Unfortunately, implementing the consequences of even a minor change is a daunting undertaking, so that the user is forced either to live with the non-optimal corpus or restart the development: neither of which is an attractive option. The proof management tool envisaged here would keep track of the dependencies in the corpus, calculate the consequences of any change, automate the implementation of those changes as much as possible, and identify any residual changes for interactive manipulation.
There are many ways in which this basic proof management tool could be extended: stronger proof repair tools including the use of analogy, theorem proving, proof planning, linking to third-party reasoning systems, etc; corpus-critiquing to suggest improved axioms, definitions, lemmas, simplified proofs, etc; tools for constructing and adapting libraries of mathematical theories consisting of axioms, definitions, data-structures, etc; tools for importing, adapting and merging libraries from third-party systems, and for exporting such libraries. The project could follow any of these optional extensions depending on the interests of the student and demand from users.
Resources Required: Access to at least one interactive proof assistant with large corpora of proofs. Use of a wide range of mathematical manipulation and reasoning tools.
Degree of Difficulty: A challenging project calling for both mathematical and system-building experience and the ability to combine these to design and implement a useful tool.
Background Needed: Mathematics, automated reasoning, software engineering.
References: