The use of formal verification for mathematics and software is growing, yet the mainstream adoption of verification systems remains hindered by barriers and inefficiencies. The coNP-completeness of the validity problem for classical propositional logic in particular forces tools to rely on heuristics that either are incomplete or have impractical worst-case complexity. SAT and SMT solvers have proved highly effective in practice, but their integration into proof assistants is difficult, and their opacity can make their behaviour less predictable to end users. At the same time, simplification and normalization procedures are ubiquitous, but the most common ones either are weak (negation normal form), do not preserve equivalence (Tseitin's transform) or are computationally expensive (full conjunctive or disjunctive normal form).
In this thesis, we propose to use algebras that are slightly weaker than Boolean algebras but with good computational properties as an approximation of classical propositional reasoning. Concretely, we introduce \emph{orthologic-based reasoning}. Orthologic is a non-classical logic based on the algebraic class of ortholattices. It uses the connectives ¬, ∧ and ∨ of Boolean algebras and shares most of its axioms, but crucially does not assume the distributivity law. This means that all orthologic theorems are theorems of classical logic, but not conversely. This small weakening allows us to design polynomial-time algorithms, while retaining a large part of the expressivity of classical logic and offering well-characterized completeness guarantees.
Our contributions span the entire spectrum of verification: theoretical foundations, algorithms, applications and implementations. We propose two key new algorithms: (1) an O(n2) normalization algorithm that maps formulas to the smallest formula in its orthologic equivalence class, and (2) an O(n2(1+∣A∣)) algorithm for deciding the validity of a formula under orthologic axioms and an arbitrary set A of non-logical assumptions. To demonstrate the correctness of these algorithms, we develop the proof theory of orthologic and prove properties such as the subformula property and the interpolation property. We formalize key results in the Rocq proof assistant and demonstrate multiple applications. Among other things, we present a type system with union \lstinline+|+ and intersection \lstinline+&+ types where the subtyping relation is decided using our orthologic algorithm. We also implement orthologic normalization in the Stainless verifier, reducing the size of verification conditions and improving the cache hit rate.
Finally, we present Lisa, a new proof assistant whose logical core uses orthologic normalization to automatically consider equivalent formulas interchangeable. Lisa relies on mainstream set-theoretic foundations aimed at appealing to the mathematics community, and offers a proof script language that is fully compatible with Scala, enabling easy
