| EPSRC Reference: |
GR/K25038/01 |
| Title: |
USER INTERFACE DESIGN FOR MECHANIZED THEOREM PROVING |
| Principal Investigator: |
Melham, Professor T |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computing Science |
| Organisation: |
University of Glasgow |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 November 1994 |
Ends: |
31 October 1997 |
Value (£): |
159,150
|
| EPSRC Research Topic Classifications: |
| Human Communication in ICT |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The principal objective of this project is to apply the principles of Human-Computer Interaction to the design of interfaces to interactive theorem provers. Interactive provers such as Larch and HOL have a significant user base in both academia and in the commercial sector. They have an important application in the mechanisation of proof for formal methods. A commonly cited obstacle to the use of theorem provers is the poor quality of the interfaces. This project aims to remedy this problem.Progress:In the three months the project has been running, a research associate has been employed and computing equipment suitable for running interactive theorem provers has been purchased. The latest versions of several theorem proving systems have been obtained and installed, as have a number of interfaces for these provers. The project team have been familiarising themselves with this software and the theories behind it. They have also been making contacts with other researchers active in the area. A study of the relevant literature has begun; this includes literature on Human-Computer Interaction, the empirical study of programming, proof in higher-order logic and the HOL system, and relevant material from automated theorem proving. Some preliminary experiments have been performed in order to identify the basic phenomena of interactive proof. These studies have helped to develop an appropriate experimental method. An analytical study of the visibility of state in the basic HOL system has also been undertaken. This has helped to clarify some syntax-level issues .
|
|
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.gla.ac.uk |