Proposer: Alan Bundy, 502716, A.Bundy@ed.ac.uk
Self-Proposed: No
Supervisor: Alan Bundy, 502716, A.Bundy@ed.ac.uk
Other Suggested Supervisors: Roy McCasland, Lucas Dixon
Subject Areas: Automated Reasoning/Theorem Proving,
Suitable for the following degrees: MSc in Informatics, MSc in Artificial Intelligence, MSc in Computer Science,
Principal goal of the project:To develop the theory of Zariski Spaces within the Isabelle Theorem Prover and to use Isabelle to prove some theorems about them.
Description of the project:
The field of automated theorem proving has been active since the late 1950s. This field has the potential to bring practical benefits to working mathematicians: improving productivity in theory development and theorem proving; ensuring the soundness of derivation; supporting rapid revision and maintenance of mathematical theories; assisting referees of mathematical papers; etc. However, there has been virtually no take-up of this technology -- mainly because it was not seen as sufficiently powerful. Fortunately, there has been a steady increase of the usability, capability and efficiency of automated theorem proving, and the time may now be ripe to re-evaluate the applicability of theorem proving technology to mathematical research.
Zariski Spaces is a branch of algebra that is being actively developed. The Zariski Space of a module M over a ring R is the semimodule of the set of varieties of submodules of M over the semiring formed by the Zariski Topology on R. One of the main inventors and developers of Zariski Spaces, Dr Roy McCasland, is a research fellow in the School of Informatics, studying the automated generation of theorems. He will co-supervise the project, advising on the implementation of the theory, the choice of conjectures to prove and their automated proof.
Isabelle is one of the most popular and successful tactic-based, interactive theorem proving systems. It has been used as the basis of a number of previous case studies, mostly in the area of formal verification or the formal development of well-established mathematics. The excitement of this project will be the chance to apply Isabelle to cutting edge, but accessible, mathematics, and to work with one of the leading experts in the field.
Zariski Spaces is the tip of a pyramid of mathematical theories: semi-groups, groups, rings, topology, etc. Many of these theories are already implemented in Isabelle but some will need to be added. A major part of the project will be to evaluate and analyse the ability of Isabelle to build mathematical theories in a modular way. This has been the subject of a previous study by 2003-04 MSc student, Chris Laumann, who identified many options, limitations and tradeoffs in Isabelle's modularity functionality. This project will be a further opportunity to investigate these issues and to extend the study to the functionality offered by rival provers. Note that success is not guaranteed, but that a well-argued analysis of partial success/failure will also be a considerable contribution to the field. Indeed, analysis of the applicability of the tools is the real purpose of the project -- not just theorem bagging.
Resources Required: Access to the Isabelle prover.
Degree of Difficulty: Some mathematical aptitude is essential. A basic implementation is fairly straightforward, modulo the difficulties discussed above, but there are plenty of opportunities for analysis and challenging theorem proving.
Background Needed: Attendence at the Automated Reasoning course is essential. Note that this is a UG3 course, but is open to MSc students.
References: