Projects per year
Abstract / Description of output
Most formal methods give rise to proof obligations (POs) which are putative lemmas that need proof.
Discharging these POs can become a bottleneck in the use of formal methods in practical applications.
It is our aim to increase the repertoire of techniques for reducing this bottleneck by tackling learning from proof attempts.
In many cases where a correct PO has not been discharged, an expert can easily see how to complete a proof.
We believe that it would be acceptable to rely on such expert intervention to do one proof if this would enable a system to kill off others "of the same form".
Discharging these POs can become a bottleneck in the use of formal methods in practical applications.
It is our aim to increase the repertoire of techniques for reducing this bottleneck by tackling learning from proof attempts.
In many cases where a correct PO has not been discharged, an expert can easily see how to complete a proof.
We believe that it would be acceptable to rely on such expert intervention to do one proof if this would enable a system to kill off others "of the same form".
Original language | English |
---|---|
Title of host publication | Proceedings of Dagstuhl Seminar 09381: Refinement Based Methods for the Construction of Dependable Systems |
Number of pages | 5 |
Publication status | Published - 2009 |
Fingerprint
Dive into the research topics of 'An Outline of a Proposed System that Learns from Experts How to Discharge Proof Obligations Automatically'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research