Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verified and Optimized Implementation of Orthologic Proof Search

Simon Guilloud, Clément Pit-Claudel

TL;DR

This work delivers a Coq-based formalization of orthologic with a sequent-calculus that restricts sequents to two formulas, together with a cut-elimination proof and a verified, memoized decision procedure that transitions from naive exponential time to a practical quadratic bound $O(n^2)$. It combines a reflection-based executable tactic, OL-normalization, and boolean solvers, augmented by a proof-producing OCaml tactic, all implemented as a standalone Coq plugin. Key contributions include multiple memoization variants (list and AVL-map) and a pointer-equality optimization, with rigorous correctness proofs ensuring equivalence to the non-memoized core and robustness across implementations. The results provide verified, efficient orthologic tooling suitable for integration into verification pipelines and offer a generalizable framework for verified memoization and reference-equality optimizations in recursive algorithms.

Abstract

We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automated reasoning tools. We formalize, in the Coq proof assistant, a proof system in sequent-calculus style for orthologic. We then prove its soundness and completeness with respect to the algebraic variety of ortholattices, and we formalize a cut-elimination theorem (in doing so, we discover and fix a missing case in a previously published proof). We then implement and verify a complete proof search procedure for orthologic. A naive implementation is exponential, and to obtain an optimal quadratic runtime, we optimize the implementation by memoizing its results and simulating reference equality testing. We leverage the resulting correctness theorem to implement a reflective Coq tactic. We present benchmarks showing the procedure, under various optimizations, matches its theoretical complexity. Finally, we develop tactics including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.

Verified and Optimized Implementation of Orthologic Proof Search

TL;DR

This work delivers a Coq-based formalization of orthologic with a sequent-calculus that restricts sequents to two formulas, together with a cut-elimination proof and a verified, memoized decision procedure that transitions from naive exponential time to a practical quadratic bound . It combines a reflection-based executable tactic, OL-normalization, and boolean solvers, augmented by a proof-producing OCaml tactic, all implemented as a standalone Coq plugin. Key contributions include multiple memoization variants (list and AVL-map) and a pointer-equality optimization, with rigorous correctness proofs ensuring equivalence to the non-memoized core and robustness across implementations. The results provide verified, efficient orthologic tooling suitable for integration into verification pipelines and offer a generalizable framework for verified memoization and reference-equality optimizations in recursive algorithms.

Abstract

We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automated reasoning tools. We formalize, in the Coq proof assistant, a proof system in sequent-calculus style for orthologic. We then prove its soundness and completeness with respect to the algebraic variety of ortholattices, and we formalize a cut-elimination theorem (in doing so, we discover and fix a missing case in a previously published proof). We then implement and verify a complete proof search procedure for orthologic. A naive implementation is exponential, and to obtain an optimal quadratic runtime, we optimize the implementation by memoizing its results and simulating reference equality testing. We leverage the resulting correctness theorem to implement a reflective Coq tactic. We present benchmarks showing the procedure, under various optimizations, matches its theoretical complexity. Finally, we develop tactics including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.
Paper Structure (13 sections, 1 theorem, 4 equations, 2 figures, 2 tables)

This paper contains 13 sections, 1 theorem, 4 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Formalizing Ortholattices and Orthologic
  5. Cut Elimination for Orthologic
  6. Decision Procedure for Orthologic
  7. Verified Memoization
  8. Reference Equality
  9. Proof-Producing Tactics and Validity Solvers
  10. Evaluation of Resulting Tactics
  11. Evaluation of the OL proof search tactics.
  12. Evaluating propositional solvers.
  13. Conclusion

Key Result

theorem thmcountertheorem

If an orthologic sequent $\Gamma, \Delta$ has a proof, then it has a proof where only subformulas of $\Gamma$ and $\Delta$ appear.

Figures (2)

  • Figure 1: Wall clock time required to prove a family of equalities with sizes ranging from 2 to 100 variables. Shaded regions indicate 95% confidence intervals. Colours indicate which implementation was used; line styles indicate which reduction strategy was used in the final step of the proof by reflection. Benchmarks were run on an Intel Core i9-13900K CPU with 64GB RAM.
  • Figure 2: Wall clock time required to prove random hard non-clausal formulas. Each point is an experiment and indicates the running time for two of the three solvers.

Theorems & Definitions (1)

  • theorem thmcountertheorem: Subformula Property, guilloudOrthologicAxioms2024