Verified and Optimized Implementation of Orthologic Proof Search

Simon Guilloud, Clément Pit-Claudel

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…