Verified and Optimized Implementation of Orthologic Proof Search

TL;DR

This paper presents a verified, quadratic-time decision procedure for orthologic equalities and inequalities, formalized in Coq, optimized for efficiency, and integrated into automated reasoning tools with practical benchmarks.

Contribution

We developed and verified a quadratic-time orthologic proof search algorithm in Coq, including formal proofs of soundness, completeness, and cut-elimination, with optimized implementation and practical tactics.

Findings

The decision procedure runs in quadratic time under optimization.

Formal proofs of soundness and completeness were completed in Coq.

Benchmarks demonstrate the optimized procedure matches theoretical complexity.

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.