EPSRC logo

Details of Grant 

EPSRC Reference: EP/C526120/1
Title: Complexity Gaps in Propositional Proof Complexity
Principal Investigator: Dantchev, Dr SS
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: Durham, University of
Scheme: First Grant Scheme Pre-FEC
Starts: 01 September 2005 Ends: 29 February 2008 Value (£): 116,905
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:  
Summary on Grant Application Form
W e propose to study the complexity (in terms of size) of formal proofs. The theorems, we want to prove, are written in a special mathematical language called First Order (FO) logic; almost all natural mathematical theorems can be expressed in this way. The rules, we are allowed to use in order to construct a proof, constitute a proof system; different sets of rules result in proof systems of different strength.W e conjecture that there are Complexity gap phenomena for a number of natural proof systems. That is, every FO theorem is either easy (i.e. has a very short proof) or hard (has only very long proofs) in the given proof system. Moreover, we suggest that there is a simple criterion that separates the hard propositions from the easy ones, so that one does not need to try to prove a theorem in order to see whether it is hard or easy.Our research, if successful, would result in a precise understanding of the strength of a number of natural proof systems and therefore would help in the development of automated (computer) theorem provers.
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: