Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Ideas for a high-level proof strategy language
Authors: Cliff B. Jones ; Gudmund Grov ; Alan Bundy
Date: 2010
Publication Title:5th Automated Formal Methods Workshop (AFM'10)
Publication Type:Conference Paper Publication Status:Pre-print
Finding ways to prove theorems mechanically was one of the earliest challenges tackled by the AI community. Notable progress has been made but there is still always a limit to any set of heuristic search techniques. From a proof done by human users, we wish to find out whether AI techniques can also be used to learn from a human user. AI4FM (Artificial Intelligence for Formal Methods) is a four-year project that starts officially in April 2010 (see It focuses on helping users of ``formal methods'' many of which give rise to proof obligations that have to be (mechanically) verified (by a theorem prover). In industrial-sized developments, there are often a large number of proof obligations and, whilst many of them succumb to similar proof strategies, those that remain can hold up engineers trying to use formal methods. The goal of AI4FM is to learn enough from one manual proof, to discharge proof obligations automatically that yield to similar proof strategies. To achieve this, a high-level (proof) strategy language is required, and in this paper we outline some ideas of such language, and towards extracting them.
2010 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Cliff B. Jones and Gudmund Grov and Alan Bundy },
title = {Ideas for a high-level proof strategy language},
book title = {5th Automated Formal Methods Workshop (AFM'10)},
year = 2010,

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh