EPSRC logo

Details of Grant 

EPSRC Reference: GR/N37414/01
Title: A GENERIC APPROACH TO PROOF PLANNING
Principal Investigator: Fleuriot, Dr J
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Sch of Informatics
Organisation: University of Edinburgh
Scheme: Fast Stream
Starts: 01 July 2001 Ends: 30 September 2004 Value (£): 62,839
EPSRC Research Topic Classifications:
Artificial Intelligence
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors Information Technologies
Related Grants:
Panel History:  
Summary on Grant Application Form
The aim of this project is to undertake a study of proof planning within a logic independent context. It will involve linking the higher order proof planner Lambda-Clam with the generic theorem prover Isavelle. The study will proceed by developing suitable syntactic translations between the two logic independent fashion. Both Lambada-Clam and Isabelle will be extended: new generic tactics will be written for Isabelle that correspond to lowest level methods in the proof planner while mechanisms will be investigated to produce new, logic-independent methods in Lambda-Clam. The combination of systems will be used to test whether proof planning can be generalised by considering non-trivial examples form at least two, but preferably more, logics. The research will be performed by the principal investigator together with a requested Phd Student.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.ed.ac.uk