EPSRC logo

Details of Grant 

EPSRC Reference: GR/J80702/01
Title: COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING
Principal Investigator: Bundy, Professor A
Other Investigators:
Ireland, Professor A Smaill, Dr A Lowe, Dr H
Researcher Co-Investigators:
Project Partners:
Department: Artificial Intelligence
Organisation: University of Edinburgh
Scheme: Standard Research (Pre-FEC)
Starts: 01 March 1994 Ends: 31 May 1996 Value (£): 609,531
EPSRC Research Topic Classifications:
Artificial Intelligence
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:  
Summary on Grant Application Form
The design and implementation of proof plans to guide the search for a proof in automatic theorem proving. The application of this work to provide automated assistance in the synthesis, verification and transformation of both software and hardware.Progress:A proof plan is a high-level outline of a proof. One proof plan can describe a family of similar proofs. We have analysed a number of induct;ive proofs and extracted descriptions of their common structure in computational form. We use proof plans to guide the search for inductive proofs. Inductive reasoning is important for applications in software and hardware development. It is needed whenever a system contains repetition, e.g. loops, recursion, parametization, etc.Our theorem proving system consists of three parts: a proof planner, CLAM, a proof editor, MOLLUSC and a cooperative problem solver, BARNACLE. CLAM reasons about the current conjecture and builds a proof plan for it. It sends this to MOLLUSC, which uses it to produce a detailed proof. MOLLUSC is a generic proof editor --- it can be customised to reason in a logical theory by supplying the logical rules of that theory. Using BARNACLE a user can interact with the proof planning process, asking for explanations of the choices made and overriding them when desired.We have applied the BARNACLE-CLAM-Mollusc system to the synthesis, verification and transformation of functional programs and logic programs. Some simple programs have been synthesised completely automatically from specifications of their required behaviour. More complex programs can be automatically verified to meet their specifications. Inefficient programs can be transformed into more efficient programs meeting the same specification. Recently, we have also looked at the problem of verifying hardware. Among the devices that we have automatically verified are an n-bit multiplier and an ALU. We are currently working on a complete microprocessor. After the implementation and specification have been encoded in a logical formalism, the proof plans are found automatically within a few minutes. This work is described in a wide range of research papers. These papers and our software are available via FTP from Edinburgh. Contact; gordon@aisb.ed.uk for details.
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