Interpolation and Quantifiers in Ortholattices
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915390761730048 |
|---|---|
| author | Guilloud, Simon Gambhir, Sankalp Kunčak, Viktor |
| author_facet | Guilloud, Simon Gambhir, Sankalp Kunčak, Viktor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_11141 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Interpolation and Quantifiers in Ortholattices Guilloud, Simon Gambhir, Sankalp Kunčak, Viktor Logic in Computer Science 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. |
| title | Interpolation and Quantifiers in Ortholattices |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.11141 |