| EPSRC Reference: |
GR/N24988/01 |
| Title: |
A CORE CALCULUS FOR HIGHER LEVEL PATTERNS OF PROOF IN TYPE THEORY |
| Principal Investigator: |
McKinna, Dr J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Durham, University of |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2000 |
Ends: |
30 September 2003 |
Value (£): |
63,451
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Existing type theory based theorem provers are based on a fundamental model of theorem proving/problem solving as interactive construction of terms well-typed relative to a context. The basic kernel of all such systems is a typechecking algorithm for such terms, and a set of basic rules of inference which are syntax-directed by the term structure. This machinery can obstruct the isolation of appropriate patterns of inference which are common particularly in inductive theorem proving, but which are considerably more specialized than a full-scale analysis based on the ideas of proof planning, especially those of rippling and fertilization. We seek a calculus of problems and their solutions which extends the usual presentations of type theory, and which would allow us to capture some of these higher-level proof steps as basic rules of inference. We expect thereby to make a positive impact on expert and non-expert users alike in the development, maintenance, re-use and intelligibility of formal proofs.
|
|
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: |
|