Interpolation and Quantifiers in Ortholattices

Explore the intricacies of orthologic in this 16-minute conference talk presented at VMCAI'24. Delve into the study of quantifiers and interpolation properties within this non-distributive weakening of classical logic. Discover a sequent-based proof system for quantified orthologic, proven sound and complete for all complete ortholattices. Learn why orthologic generally doesn't allow quantifier elimination, yet still permits the existence of interpolants. Examine an efficient algorithm for computing these interpolants. Gain insights into how this research can be applied to quickly establish unreachability in verification algorithms. Join speakers Sankalp Gambhir, Simon Guilloud, and Viktor Kunčak as they present their findings on this fascinating topic in theoretical computer science.