EPSRC logo

Details of Grant 

EPSRC Reference: GR/K25038/01
Title: USER INTERFACE DESIGN FOR MECHANIZED THEOREM PROVING
Principal Investigator: Melham, Professor T
Other Investigators:
Gray, Mr P Calder, Professor M
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