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

Add to your list(s) Download to your calendar using vCal

• Alex Rice (University of Cambridge)
• Friday 11 June 2021, 13:00-14:00
• https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09.

If you have a question about this talk, please contact Anupam Das.

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) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ 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.

This talk is based on joint work with Anupam Das that will be published in the proceedings of FSCD 2021 .

Zoom link: https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience
• https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09

Note that ex-directory lists are not shown.