Student research opportunities
Proof Optimisation
Project Code: CECS_106
This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.
Keywords:
theorem-proving
Supervisor:
Dr Michael NorrishOutline:
A proof over an LCF-style kernel is usually expressed (by the user) in terms of high-level steps or tactics. Ultimately however, the proof is still executed at the lowest level of primitive inference steps. If these steps are recorded, the resulting proof trace
is very long, for all that it may be possible to execute it quickly.
A possible project would be to investigate these traces and optimise them so that they proved the same results but did so faster. Many of the tricks of compiler optimisation might well have proof analogues, and insights from proof theory may also be relevant.
