|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Learning from experts to aid the automation of proof search |
| Authors:
Alan Bundy
; Gudmund Grov
; Cliff Jones
|
| Date:Sep 2009 |
| Publication Title:AVoCS'09: PreProceedings of the Ninth International Workshop on Automated Verification of Critical Systems |
| Publisher:Swansea University |
|
Publication Type:Conference Paper
Publication Status:Published
|
|
Volume No:CSR-2-2009
Page Nos:229-232
|
|
|
- Abstract:
-
Most formal methods give rise to proof obligations which are putative lemmas that need proof. Discharging these POs can become a bottleneck in the use of formal methods in practical applications. Some techniques for reducing this bottleneck are known it is our aim to increase the repertoire of techniques by tackling learning from proof attempts. Even after obvious fixed heuristics are used, there remains the problem of what to do with POs that are not discharged automatically. 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".
- Copyright:
- 2009 by Swansea University. All Rights Reserved
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-1347,
- author = {
Alan Bundy
and Gudmund Grov
and Cliff Jones
},
- title = {Learning from experts to aid the automation of proof search},
- book title = {AVoCS'09: PreProceedings of the Ninth International Workshop on Automated Verification of Critical Systems},
- publisher = {Swansea University},
- year = 2009,
- month = {Sep},
- volume = {CSR-2-2009},
- pages = {229-232},
- url = {http://www.cs.swan.ac.uk/avocs09/proceedings.php},
- }
|
