Research
Research Groups
- Logic and
Computation (Liverpool)
- Mathematical Reasoning
Group (Edinburgh)
Dream Group Only Links - Foundations of Programming (Nottingham)
Research Interests
- Engineering Autonomous Space Software
- Model Checking Agent Programming Languages
- The Use of Proof in the Location of Programming Errors
- The Use and Construction of Proof Planning Systems
- Rippling in a Higher Order Setting
- Rippling is a key proof planning technique used principally to automate proof by mathematical induction. There are a number of differing theories of rippling, especially where it can account for higher order properties, and a number of variations of the underlying technique. It is also a technique which is complex and error-prone both to implement and also to describe. Rippling is an extremely powerful automated reasoning technique, an in particular may help significantly in the automation of synthesis proofs using middle-out reasoning. However there are a number of challenges to be overcome before it can be easily adopted. The technique is in bad need of formalisation to clarify the ambiguities and to establish the relationships between different theories. Theoretical and experimental comparative work is required to evaluate the scope of variant theories. Experimental work is also required to evaluate how different rippling variants interact in practice and to detail their implementation in a clear fashion.
- Induction Challenges
- Applications of Artificial Intelligence to Animal Simulation and Anatomy
References
Theorem Proving Systems
- ACL2
- HOL
- Isabelle - HOL Logic
- IsaPlanner
- Omega
- OpenMath and its Core Content Dictionaries
- Proof General
- PROSPER
- PVS
Organisations, Departments and Research Groups
- Society for the Study of Artificial Intelligence and Simulation of Behaviour
- Association for Automated Reasoning
- Formal Methods at Saarbrucken
- Cambridge Computer Lab
- Edinburgh Informatics
- Edinburgh Calculemus Node