{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T10:55:32Z","timestamp":1774436132021,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Swiss National Fund","award":["200021_197288"],"award-info":[{"award-number":["200021_197288"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polynomial-time equivalence checking that is sound with respect to Boolean algebra semantics. We generalize ortholattice reasoning and obtain an algorithm for proving a larger class of classically valid formulas.<\/jats:p>\n          <jats:p>As the key result, we analyze a proof system for orthologic augmented with axioms. An important feature of the system is that it limits the number of formulas in a sequent to at most two, which makes the extension with axioms non-trivial. We show a generalized form of cut elimination for this system, which implies a sub-formula property. From there we derive a cubic-time algorithm for provability from axioms, or equivalently, for validity in finitely presented ortholattices. We further show that propositional resolution of width 5 proves all formulas provable in orthologic with axioms. We show that orthologic system subsumes resolution of width 2 and arbitrarily wide unit resolution and is complete for reasoning about generalizations of propositional Horn clauses.<\/jats:p>\n          <jats:p>Moving beyond ground axioms, we introduce effectively propositional orthologic (by analogy with EPR for classical logic), presenting its semantics as well as a sound and complete proof system. Our proof system implies the decidability of effectively propositional orthologic, as well as its fixed-parameter tractability for a bounded maximal number of variables in each axiom. As a special case, we obtain a generalization of Datalog with negation and disjunction.<\/jats:p>","DOI":"10.1145\/3632881","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1150-1178","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Orthologic with Axioms"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8179-7549","authenticated-orcid":false,"given":"Simon","family":"Guilloud","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/b978-0-934613-40-8.50006-3"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70953-4"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498698"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.5075\/epfl-thesis-8260"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1976-095-6"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2003.12.011"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/502807.502810"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022993408070"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/113446.113468"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00652069"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_19"},{"key":"e_1_3_1_20_1","first-page":"17:1","volume-title":"14th Conference on Interactive Theorem Proving (Leibniz International Proceedings in Informatics)","author":"Guilloud Simon","year":"2023","unstructured":"Simon Guilloud, Sankalp Gambhir, and Viktor Kuncak. 2023b. LISA \u2013 A Modern Proof System. In 14th Conference on Interactive Theorem Proving (Leibniz International Proceedings in Informatics). Daghstuhl, Bialystok, 17:1\u201317:19."},{"key":"e_1_3_1_21_1","unstructured":"Simon Guilloud Sankalp Gambhir and Viktor Kun\u010dak. 2023c. LISA Proof Assistant. https:\/\/github.com\/epfl-lara\/lisa"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883401"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.3390\/logics1010004"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2203.02872"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1515\/dema-2005-0402"},{"key":"e_1_3_1_26_1","volume-title":"Orthomodular Lattices","author":"Kalmbach Gudrun","year":"1983","unstructured":"Gudrun Kalmbach. 1983. Orthomodular Lattices. Academic Press Inc, London ; New York."},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.18778\/0138-0680.47.4.01"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.25"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00015-5"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000125"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90124-X"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347481"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_1_40_1","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","author":"Robinson John Alan","year":"2001","unstructured":"John Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning (in 2 Volumes). Elsevier and MIT Press, MIT."},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02483891"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00000328"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90006-9"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/42790"},{"key":"e_1_3_1_46_1","volume-title":"Principles of Database and Knowledge-Base Systems, Volume II","author":"Ullman Jeffrey D.","year":"1989","unstructured":"Jeffrey D. Ullman. 1989. Principles of Database and Knowledge-Base Systems, Volume II. Computer Science Press, New Yor, United States."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62688-3_47"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632881","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632881","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:28Z","timestamp":1751659588000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632881"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632881"],"URL":"https:\/\/doi.org\/10.1145\/3632881","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}