Details of Grant 

EPSRC Reference:	GR/R84092/01
Title:	Pythagoras: Machine Support for Semi-formalised Proof Oriented Mathematics
Principal Investigator:	Luo, Professor Z
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	Durham, University of
Scheme:	Standard Research (Pre-FEC)
Starts:	01 April 2003	Ends:	30 September 2004	Value (£):	123,195
EPSRC Research Topic Classifications:	Fundamentals of Computing Logic & Combinatorics
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:
Summary on Grant Application Form
Machine support for both numerical and symbolic computational mathematics has been very successfully used in mathematics, science and education. This proposal aims to investigate the issues involved in the achievement of such support for proof oriented mathematics. We believe that the theory and technology of interactive theorem proving can be effectively applied to building tools to help research mathematicians as well as students of mathematics in their proof development effort. We believe that a key to this is to focus not on the full formalisation of mathematics but on what we here call semi-formalised mathematics. This is mathematics which is completely formal as far as the formulation of definitions and results is concerned, but where proofs are allowed to have steps which may not be instances of rules of inference, but instead are documented with various kinds of less formal evidence for the step. We shall study the theory and techniques needed to build supporting computer environments for the development and presentation of semi-formal mathematics. Our method is to implement a generic environment based on an existing proof development system. We will develop and implement techniques of meta-variables in multiple-contexts that will provide effective support for the representation and development of semi-formal proofs. The evaluation will be conducted via case studies for educational uses of our tools in Mathematics and Computer Science courses.
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: