A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems.
Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : X (y z) → (x y) V z, and medial : (w x) V (y z) → (w V y) (x V z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known.
In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.
|Title of host publication||6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)|
|Number of pages||19|
|Publication status||Published - 6 Jul 2021|
|Event||6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 - Virtual, Buenos Aires, Argentina|
Duration: 17 Jul 2021 → 24 Jul 2021
|Name||Leibniz International Proceedings in Informatics, LIPIcs|
|Conference||6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021|
|City||Virtual, Buenos Aires|
|Period||17/07/21 → 24/07/21|
Bibliographical noteFunding Information:
Funding This work was supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. Alex Rice acknowledges funding from the Royal Society.
© 2021 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.
- Linear inference
- Linear logic
- Proof theory
ASJC Scopus subject areas