New minimal linear inferences in boolean logic independent of switch and medial

Anupam Das, Alex A. Rice

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publication6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
EditorsNaoki Kobayashi
PublisherSchloss Dagstuhl
Number of pages19
ISBN (Electronic)9783959771917
DOIs
Publication statusPublished - 6 Jul 2021
Event6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 - Virtual, Buenos Aires, Argentina
Duration: 17 Jul 202124 Jul 2021

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume195
ISSN (Electronic)1868-8969

Conference

Conference6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021
Country/TerritoryArgentina
CityVirtual, Buenos Aires
Period17/07/2124/07/21

Bibliographical note

Funding 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.

Publisher Copyright:
© 2021 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.

Keywords

  • Implementation
  • Linear inference
  • Linear logic
  • Proof theory
  • Rewriting

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'New minimal linear inferences in boolean logic independent of switch and medial'. Together they form a unique fingerprint.

Cite this