Room 502, Level 5, School of Computing Science, Sir Alywn Williams Building, University of Glasgow, Glasgow, G12 8QQ
Research title: Proof Logging for Constraint Propagation Algorithms
I am interested in trustworthy symbolic artificial intelligence, specifically how we can use formal arguments and mathematical proof to make A.I. techniques self-certifying. Currently, I am researching proof logging for constraint propagation algorithms, an important part of constraint programming. The idea is that, alongside a solution, a solver should produce a mathematical proof that its answer is correct, which can then be verified and audited by an external program.