RESEARCH STUDENT
— Tom Gransden MComp Computer Science (University of Leicester)
Ph.D Student
|
G1 Ken Edwards Building
School of Computing and Mathematical Sciences,
University of Leicester,
University Road,
Leicester,
LE1 7RH.
T: +44 (0)116 252 3883
F: +44 (0)116 252 3883
E: tg153 (AT) le.ac.uk
|
Having begun my undergraduate studies at Leicester in 2008, I graduated in 2012 with an MComp in Computer Science.
I am now working under the supervision of Dr. Neil Walkinshaw and Prof. Rajeev Raman on my PhD: Boosting Automated Reasoning by Mining Existing Proofs.
My PhD studies are funded by a PhD studentship from the College of Science and Engineering PhD Studentship Scheme.
I am researching the topic of tactic mining for Interactive Theorem Provers (ITP's) in an attempt to provide better automation
than is currently available. Users conduct proofs in ITP's by entering a finite sequence of proof steps - these can be thought of as
functions that either solve a proof or advances the proof state in some way. What I am investigating is how
we can apply machine learning techniques to libraries of these proof step sequences. If
we can infer useful models from these examples, then hopefully we can use this newly learned information to automate the proofs of new conjectures. This method
could be reasonabily applied to any ITP that uses tactics, and has a library of existing proofs that could be mined.
Away from the topics of my PhD, I am mostly interested in the theoretical side of Computer Science. Artificial Intelligence interests me a lot,
and I was fortunate enough to be able to learn about computer chess for my 3rd year project. In addition to researching the key concepts, I implemented a chess
game in Java, with my own GUI and game engine. If anyone is interested I can try and dig out my old code.
I am also interested in Formal Verification. For my masters dissertation, I used the SPIN model checker to verify some Service Oriented Computing protocols that
were specified in a domain specific language. The main tasks were the representation of the models in PROMELA, and the formulation of the desired properties in
Linear Temporal Logic.
Thomas Gransden
Boosting Automated Reasoning by Mining Existing Proofs [paper][slides][poster]
Automated Reasoning Workshop 2013
Dundee, Scotland
Thomas Gransden, Neil Walkinshaw and Rajeev Raman
Mining State-Based Models from Proof Corpora [preprint - (arXiv)][paper - (SpringerLink)][data][slides][bibtex]
Conferences on Intelligent Computer Mathematics 2014 (Mathematical Knowledge Management Track)
Coimbra, Portugal
Thomas Gransden
Combining SEPIA and ML4PG [paper][slides][poster]
Automated Reasoning Workshop 2015
Birmingham, England
Thomas Gransden, Neil Walkinshaw and Rajeev Raman
SEPIA: Search for Proofs Using Inferred Automata [preprint - (arXiv)][paper - (SpringerLink)][data][slides][bibtex]
Conference on Automated Deduction (CADE-25)
Berlin, Germany
I have written a few software tools over the course of my research. They can be
seen at my bitbucket page
The main component of my research is SEPIA, a technique to automatically prove Coq theorems using Extended Finite State Machines..
I have provided teaching assistance for the following modules:
- CO2012 - Software Project Management and Professionalism
- CO1001 - Logic and Problem Solving
- CO3098 - Web Technologies
- CO7206 - Software Reengineering
- CO1005 - Data Structures and Development Environments
- CO1019 - Databases and Web Applications
| 