Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae
- Submitting institution
-
The University of Bath
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 145988328
- Type
- D - Journal article
- DOI
-
10.2168/LMCS-12(2:5)2016
- Title of journal
- Logical Methods in Computer Science
- Article number
- 5
- First page
- 1
- Volume
- 12
- Issue
- 2
- ISSN
- 1860-5974
- Open access status
- Out of scope for open access requirements
- Month of publication
- May
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- 2
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper achieves a cut-elimination result with unexpectedly tight complexity by integrating the traditional technique of threshold functions with the newer one of atomic flows. It establishes a general methodology for the developing area of deep inference. Perhaps more importantly, this paper triggered the first proof complexity result outside of deep inference, i.e., in mainstream proof complexity. Indeed, in CSL-LICS 2014, Das improved the best bounds for monotone proofs using techniques first pioneered in this paper.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -