| EPSRC Reference: |
GR/K09205/01 |
| Title: |
SUPPPORTING PLANNING, REFLECTION RE-USE IN THE INTERFACES TO THEOREM PROVING ASSISTANTS |
| Principal Investigator: |
Harrison, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of York |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 April 1995 |
Ends: |
31 March 1998 |
Value (£): |
147,550
|
| EPSRC Research Topic Classifications: |
| Human-Computer Interactions |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The objective of the project is to discover and evaluate general interaction properties of Theorem Proving Assistants which support planning, reflection and re-use, and to express these properties in a way which can be used in the specification and design of future systems.To achieve this objective the project will: Evaluate existing interfaces to Theorem Proving Assistants using HCI modelling techniques such as those reported in current University of York research and using protocol analysis techniques. Produce a generic abstract model of a Theorem Proving Assistant in terms of which significant interaction properties of such systems can be explicated. Produce a generic specification of an interface to a Theorem Proving Assistant which is to support proof planning and re-use of partial proofs. Engineer a new interface to an existing system to show how proof planning and proof reuse can be supported in it. Analyse the consequences for the interface specification of introducing additional functionality to the system, e.g., introduction of different proof theories (window logics, sequent calculus), introduction of decision procedures for common types, introduction of additional tactics. Evaluate the new interface in comparison to the previous interface.
|
|
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.york.ac.uk |