TY - GEN
T1 - Learning from Experts to Aid the Automation of Proof Search.
AU - Bundy,Alan
AU - Grov,Gudmund
AU - Jones,Cliff B.
PY - 2009
Y1 - 2009
N2 - 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".
AB - 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".
KW - Formal verification
KW - Automated theorem proving
KW - proof planning
M3 - Conference contribution
BT - Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 2009)
ER -