| EPSRC Reference: |
GR/R29697/01 |
| Title: |
The Semantics of Classical Proofs |
| Principal Investigator: |
Hyland, Professor JME |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Pure Maths and Mathematical Statistics |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
21 February 2002 |
Ends: |
20 February 2005 |
Value (£): |
77,518
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Logic & Combinatorics |
|
| EPSRC Industrial Sector Classifications: |
| Information Technologies |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
22 Feb 2001
|
MathFIT
|
Deferred
|
|
|
Summary on Grant Application Form |
|
Classical proof is of fundamental importance in both Mathematics and Computer Science. In proof theory some of the most interesting and hardest problems centre round the equivalence of proofs and the classification of this through rules of local permutability. The sequent calculus in particular exhibits strong symmetry properties which make it hard to model. Current research concentrates on semantics which pass through a double negation translation and which therefore violate some of these symmetries. We propose to harness recent work in enriched cateogry theory to furnish a fully symmetric calculus and to provide the natural supporting theoretical results. We intend to use this analysis in a search for concrete and interesting models, inspired perhaps by process calculus and by conventional combinatorial and mathematical structures. We plan to commence an investigation of applications in mathematics (Herbrand's theorem, Ramsay's theorem) and Computer Science (productive use of failure in classical proof search).
|
|
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.cam.ac.uk |