Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Preprints and Working Papers
  4. Verified and Optimized Implementation of Orthologic Proof Search
 
preprint

Verified and Optimized Implementation of Orthologic Proof Search

Guilloud, Simon  
•
Pit-Claudel, Clément  
2025

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

Verified_and_Optimized_Implementation_of_Orthologic_Proof_Search.pdf

Type

Main Document

Version

http://purl.org/coar/version/c_71e4c1898caa6e32

Access type

openaccess

License Condition

CC BY

Size

562.26 KB

Format

Adobe PDF

Checksum (MD5)

6915c60b07db5e2f7d650c4de7d016e1

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés