Verified and Optimized Implementation of Orthologic Proof Search

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; to obtain an optimal quadratic run time, 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 that the procedure, under various optimizations, matches its theoretical complexity.

Finally, we develop a collection of tactics, including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.