Interpolation and Quantifiers in Ortholattices
We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for quantified orthologic, which we prove sound and complete for the class of all complete ortholattices. We show that orthologic does not admit quantifier elimination in general. Despite that, we show that interpolants always exist in orthologic. We give an algorithm to compute interpolants efficiently. We expect our result to be useful to quickly establish unreachability as a component of verification algorithms.
WOS:001166801100011
2024-01-01
978-3-031-50523-2
978-3-031-50524-9
Cham
14499
235
257
REVIEWED
Event name | Event place | Event date |
London, ENGLAND | JAN 15-16, 2024 | |