{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:29:30Z","timestamp":1760056170631,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986819"},{"type":"electronic","value":"9783031986826"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_8","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:14:30Z","timestamp":1753154070000},"page":"130-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verified and\u00a0Optimized Implementation of\u00a0Orthologic Proof Search"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8179-7549","authenticated-orcid":false,"given":"Simon","family":"Guilloud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1900-3901","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Abrahamsson, O., Myreen, M.O.: Fast, verified computation for candle. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, pp. 4:1\u20134:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.4","DOI":"10.4230\/LIPIcs.ITP.2023.4"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: First International Conference on Certified Programs and Proofs, Kenting, Taiwan (2011)","DOI":"10.1007\/978-3-642-25379-9_13"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10817-014-9306-0","volume":"53","author":"T Braibant","year":"2014","unstructured":"Braibant, T., Jourdan, J.-H., Monniaux, D.: Implementing and reasoning about Hash-consed data structures in Coq. J. Autom. Reason. 53(3), 271\u2013304 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9306-0","journal-title":"J. Autom. Reason."},{"issue":"5","key":"8_CR4","doi-asserted-by":"publisher","first-page":"977","DOI":"10.4153\/CJM-1976-095-6","volume":"28","author":"G Bruns","year":"1976","unstructured":"Bruns, G.: Free ortholattices. Can. J. Math. 28(5), 977\u2013985 (1976). https:\/\/doi.org\/10.4153\/CJM-1976-095-6","journal-title":"Can. J. Math."},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1093\/logcom\/exaa073","volume":"31","author":"Y Forster","year":"2021","unstructured":"Forster, Y., Kirst, D., Wehr, D.: Completeness theorems for first-order logic analysed in constructive type theory: extended version. J. Log. Comput. 31(1), 112\u2013151 (2021). https:\/\/doi.org\/10.1093\/logcom\/exaa073","journal-title":"J. Log. Comput."},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Freese, R., Jezek, J., Nation, J.: Free Lattices. Mathematical Surveys and Monographs, vol.\u00a042. American Mathematical Society, Providence, Rhode Island, March 1995. https:\/\/doi.org\/10.1090\/surv\/042","DOI":"10.1090\/surv\/042"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Frumin, D.: Semantic cut elimination for the logic of bunched implications, formalized in Coq, December 2021. arXiv:2112.05515. https:\/\/doi.org\/10.48550\/arXiv.2112.05515","DOI":"10.48550\/arXiv.2112.05515"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen I. Math. Z. 39, 176\u2013210 (1935)","journal-title":"Math. Z."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Guilloud, S., Bucev, M., Milovancevic, D., Kuncak, V.: Formula normalizations in verification. In: 35th International Conference on Computer Aided Verification, Paris, LNCS, pp. 398\u2013422. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_19"},{"key":"8_CR10","unstructured":"Guilloud, S., Gambhir, S., Kuncak, V.: LISA \u2013 a modern proof system. In: 14th Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, pp. 17:1\u201317:19. Daghstuhl, Bialystok (2023)"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Guilloud, S., Gambhir, S., Kun\u010dak, V.: Interpolation and\u00a0quantifiers in\u00a0ortholattices. In: Verification, Model Checking, and Abstract Interpretation: 25th International Conference, VMCAI 2024, London, United Kingdom, 15\u201316 January 2024, Proceedings, Part I, pp. 235\u2013257. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-50524-9_11","DOI":"10.1007\/978-3-031-50524-9_11"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Guilloud, S., Kun\u010dak, V.: Orthologic with axioms. Proc. ACM Programm. Lang. 8(POPL), 39:1150\u201339:1178 (2024). https:\/\/doi.org\/10.1145\/3632881","DOI":"10.1145\/3632881"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Herrmann, C., Roddy, M.S.: On varieties of modular ortholattices which are generated by their finite-dimensional members, p.\u00a09 (2014)","DOI":"10.1007\/s00012-014-0305-0"},{"key":"8_CR14","unstructured":"James, D.W.H., Hinze, R.: A reflection-based proof tactic for lattices in Coq. In: Symposium on Trends in Functional Programming (2009)"},{"issue":"4","key":"8_CR15","doi-asserted-by":"publisher","first-page":"217","DOI":"10.18778\/0138-0680.47.4.01","volume":"47","author":"T Kawano","year":"2018","unstructured":"Kawano, T.: Labeled sequent calculus for orthologic. Bull. Sect. Logic 47(4), 217\u2013232 (2018). https:\/\/doi.org\/10.18778\/0138-0680.47.4.01","journal-title":"Bull. Sect. Logic"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Laurent, O.: Focusing in orthologic. In: Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, 22\u201326 June 2016, Porto, Portugal. LIPIcs, vol. 52, pp. 25:1\u201325:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Porto, Portugal (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.25","DOI":"10.4230\/LIPIcs.FSCD.2016.25"},{"issue":"4","key":"8_CR17","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1017\/S0960129510000125","volume":"20","author":"A Meinander","year":"2010","unstructured":"Meinander, A.: A solution of the uniform word problem for ortholattices. Math. Struct. Comput. Sci. 20(4), 625\u2013638 (2010). https:\/\/doi.org\/10.1017\/S0960129510000125","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"8_CR18","first-page":"75","volume":"80","author":"Y Miyazaki","year":"2005","unstructured":"Miyazaki, Y.: Some properties of orthologics. Studia Logica Int. J. Symbolic Logic 80(1), 75\u201393 (2005). arXiv:2001.6705","journal-title":"Studia Logica Int. J. Symbolic Logic"},{"key":"8_CR19","unstructured":"Navarro, J.A., Voronkov, A.: Generation of hard non-clausal random satisfiability problems. In: Proceedings of the 20th National Conference on Artificial Intelligence - Volume 1, AAAI 2005, pp. 436\u2013442. AAAI Press, Pittsburgh, Pennsylvania, July 2005"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"M\u00f6nting, J.S.: Cut elimination and word problems for varieties of lattices. Algebra Universalis 12(1), 290\u2013321 (1981). https:\/\/doi.org\/10.1007\/BF02483891","DOI":"10.1007\/BF02483891"},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/PL00000328","volume":"37","author":"M Sherif","year":"1997","unstructured":"Sherif, M.: Decision problem for orthomodular lattices. Algebra Universalis 37(1), 70\u201376 (1997). https:\/\/doi.org\/10.1007\/PL00000328","journal-title":"Algebra Universalis"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"41","DOI":"10.6092\/issn.1972-5787\/1574","volume":"2","author":"M Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41\u201362 (2009). https:\/\/doi.org\/10.6092\/issn.1972-5787\/1574","journal-title":"J. Formalized Reasoning"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-40537-2_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"H Tews","year":"2013","unstructured":"Tews, H.: Formalizing cut elimination of coalgebraic logics in Coq. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 257\u2013272. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40537-2_22"},{"key":"8_CR24","unstructured":"Truszkowska, W., Grabowski, A.: On the two short axiomatizations of ortholattices (2003)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-540-70590-1_28","volume-title":"Rewriting Techniques and Applications","author":"C Urban","year":"2008","unstructured":"Urban, C., Zhu, B.: Revisiting cut-elimination: one difficult proof is really a proof. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 409\u2013424. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70590-1_28"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-319-94821-8_34","volume-title":"Interactive Theorem Proving","author":"S Wimmer","year":"2018","unstructured":"Wimmer, S., Hu, S., Nipkow, T.: Verified memoization and dynamic programming. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 579\u2013596. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_34"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:38:38Z","timestamp":1759999118000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}