Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Graph Theory
Units: 24 units
Background
Mechanising mathematics is the task of turning (relatively) well-understood mathematics into verified proofs with an interactive theorem-proving system. Such verified material can then lie behind high-assurance software.
This project is an opportunity for students who wants to learn the HOL4 theorem-proving system and realise an important piece of mathematics. At thesis level (24 units), the simple mechanisation of the mathematics would need to be augmented with an application of the mechanisation and/or significant novelty in the nature of the proofs.
Research Questions and Tasks
The aim of this research project is to mechanize some advanced topics of Graphy Theory in the HOL theorem prover (HOL4), following proofs given in [Diestel] (or [Diestel4]). The focus will be on Graph Minors, Tree-Width and WQO (well-quasi-ordering), etc. The basic definitions of (simple) graphs are already there. This will include the following tasks:
- Define the concepts of graph minors (and topological minors) following Secion 1.7 of [Diestel];
- Mechanize all theorems of various chapters of [Diestel] needed by theorems in Chapter 12 of [Diestel] (see below). This includes some theorems in Chapter 9 (Ramsey Theory for Graphs).
- Mechanize all major theorems of Chapter 12 (Minors, Trees and WQO) of [Diestel] if the proofs are explicitly given in the book (otherwise the actual proof may be huge, i.e. in 500 pages acrossing 20+ papers).
The development should follow modern techniques and guidelines for HOL4, e.g. [HOLTutorial] and [HOL4]. Ideally, the project will be submitted to HOL4 official as part of its core theories.
NOTE: The student will get some basic training through a mini course to get familar with interactive theorem proving (ITP) techniques (and HOL4 in particular).
References
- [HOLTutorial] The HOL System LOGIC
- [HOL4] The HOL System DESCRIPTION
- [Diestel] Diestel, R.: Graph Theory, 5th Edition. Springer-Verlag (2017). doi:10.1007/978-3-662-53622-3
- [Diestel4] Diestel, R.: Graph Theory, 4th Edition. Springer-Verlag (2010).
Requirements:
Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; mathematics (discrete mathematics and graph theory basics)