On linear rewriting systems for Boolean logic and some applications to proof theory
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 90917410
- Type
- D - Journal article
- DOI
-
10.2168/LMCS-12(4:9)2016
- Title of journal
- Logical Methods in Computer Science
- Article number
- 9
- First page
- 1
- Volume
- 12
- Issue
- 4
- ISSN
- 1860-5974
- Open access status
- Compliant
- Month of publication
- December
- 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
-
1
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper studies linear inequalities in Boolean algebra. It is significant because firstly it solves an open problem from the 1990s in computability logic and Blass' game semantics for linear logic: the multiplicative fragment is not axiomatisable (Corollary 6.9). Secondly it uses novel graph-theoretic methods, yielding several consequences in pure proof theory (e.g. Sections 7, 8).
A short version was published at RTA-TLCA'15, the leading rewriting conference, and was invited to a special journal issue.
The work inspired a recent surge of interest in Combinatorial/Graph-based proofs e.g. papers at LICS'19, LICS'20, and Tableaux'19.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -