![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > New minimal linear inferences in Boolean logic independent of switch and medial
New minimal linear inferences in Boolean logic independent of switch and medialAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsAnalysis seminar Birmingham Popular Maths Lectures Theoretical computer science seminarOther talksLife : it’s out there, but what and why ? TBA The tragic destiny of Mileva Marić Einstein TBA TBA Quantum Sensing in Space |