| EPSRC Reference: |
GR/J80702/01 |
| Title: |
COMPUTATIONAL MODELLING OF MATHEMATICAL REASONING |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| 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: |
|
| 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 |