Learning from Experts to Aid the Automation of Proof Search.

Alan Bundy; Gudmund Grov; Cliff B. Jones

Learning from Experts to Aid the Automation of Proof Search.

Alan Bundy, Gudmund Grov, Cliff B. Jones

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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".

Original language	English
Title of host publication	Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 2009)
Publication status	Published - 2009

Keywords / Materials (for Non-textual outputs)

Formal verification
Automated theorem proving
proof planning

Access to Document

ReportSubmitted manuscript, 102 KB
Full textSubmitted manuscript, 59.2 KB

A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A. (Principal Investigator), Bundy, A. (Sponsor), Grov, G. (Co-Investigator (External)), Ireland, A. (Co-Investigator (External)) & Jones, C. B. (Co-Investigator (External))
EPSRC
1/04/10 → 31/03/14
Project: Research

Cite this

@inproceedings{fe475182abec43a7bcfc1669cf742cbf,

title = "Learning from Experts to Aid the Automation of Proof Search.",

abstract = "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{"}.",

keywords = "Formal verification, Automated theorem proving , proof planning",

author = "Alan Bundy and Gudmund Grov and Jones, \{Cliff B.\}",

year = "2009",

language = "English",

booktitle = "Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 2009)",

}

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 -

Learning from Experts to Aid the Automation of Proof Search.

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

A14FM : using A1 to aid automation of proof search in formal methods

Cite this