Interpolation and Quantifiers in Ortholattices
summary
Sequent proof system for quantified orthologic is sound and complete for complete ortholattices, and validity checking runs in quadratic-time decision and normalization is quadratic as well. Quantifiers are added as greatest lower and least upper bounds but there is no quantifier elimination (counterexample using M2 and M4). Proof-representation interpolation fails, yet implication-based interpolants always exist; the construction is inductive on proofs, yields interpolants in time linear in the proof and overall interpolants computable in quadratic time for formulas.
AI-written summary · about
chapters (10)
- 0:00Interpolation and quantifiers
- 1:07Studying ortholattices
- 2:55Proof system for orthologic
- 5:26Model checking interpolation
- 6:51Quantified orthologic semantics
- 7:54Quantifier elimination
- 9:40Interpolation limitations
- 10:44Implication-based interpolation
- 12:31Summary of results
- 13:59Q&A
related talks
14mLOUD: Synthesizing Strongest and Weakest Specifications
29mQuantitative strongest post: a calculus for reasoning about the flow of quantitative inform
18mQualifying System F-sub
17mCalculational design of Incorrectness Separation Logic
30mRelatively Complete Verification of Probabilistic Programs
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
59mUnification Modulo Equational Theories in Languages with Binding Operators
25mA Logic for the Imprecision of Abstract Interpretations