正交逻辑证明搜索的验证与优化实现
Verified and Optimized Implementation of Orthologic Proof Search
AI总结：
本文在 Coq 中形式化并验证了正交逻辑的相继式演算证明系统及其切消定理，进而实现并优化了一个二次时间复杂度的完整证明搜索过程，最终将其封装为独立的 Coq 策略插件。
摘要：
我们报告了一个针对正交逻辑等式与不等式的优化且经过验证的判定过程的开发工作。该判定过程具有二次时间复杂度，并在自动推理工具中被用作经典命题逻辑的一个可靠、高效且可预测的近似。我们在 Coq 证明助手中形式化了一个用于正交逻辑的相继式演算风格的证明系统。随后，我们证明了其相对于正交格代数簇的可靠性与完备性，并形式化了一个切消定理（在此过程中，我们发现并修正了先前已发表证明中一个缺失的情形）。接着，我们实现并验证了一个完整的正交逻辑证明搜索过程。一个朴素实现的复杂度是指数级的，为了获得最优的二次运行时间，我们通过记忆化其结果并模拟引用相等性测试来优化该实现。我们利用由此得到的正确性定理实现了一个自反的 Coq 策略。我们给出的基准测试表明，该过程在各种优化下均符合其理论复杂度。最后，我们开发了包括关于正交逻辑的规范化以及一个布尔求解器在内的策略，并同样对其进行了基准测试。我们将这些策略作为一个独立的 Coq 插件提供。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
