标题： 正交格中的插值和量词 显示英文标题

标题： Interpolation and Quantifiers in Ortholattices

摘要： 我们研究\emph{正交逻辑}中的量词和插值性质。\emph{正交逻辑}是经典逻辑的一种非分配性弱化形式，其公式有效性相对于经典逻辑而言是可靠的，但其决策过程为二次时间。我们提出了一个基于序贯的量化正交逻辑证明系统，并证明了该系统对于所有完全正交格类而言是可靠且完备的。 我们证明了正交逻辑通常不允许量词消去。 尽管如此，我们证明了插值在正交逻辑中始终存在。我们给出了一个高效计算插值的算法。我们期望我们的结果能够快速将不可达性作为验证算法的一个组成部分。 显示英文摘要

摘要： 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.