Interpolation and Quantifiers in Ortholattices
Logic in Computer Science
2025-07-16 v1
Abstract
We study quantifiers and interpolation properties in \emph{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.
Keywords
Cite
@article{arxiv.2507.11141,
title = {Interpolation and Quantifiers in Ortholattices},
author = {Simon Guilloud and Sankalp Gambhir and Viktor Kunčak},
journal= {arXiv preprint arXiv:2507.11141},
year = {2025}
}