{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:55:03Z","timestamp":1742975703867,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995263"},{"type":"electronic","value":"9783030995270"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Motivated by proof checking, we consider the problem of efficiently establishing equivalence of propositional formulas by relaxing the completeness requirements while still providing certain guarantees. We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of Boolean algebra. The starting point for our procedure is a variation of Aho, Hopcroft, Ullman algorithm for isomorphism of trees, which we generalize to directed acyclic graphs. We combine this algorithm with a term rewriting system we introduce to decide equivalence of terms. We prove that our rewriting system is terminating and confluent, implying the existence of a normal form. We then show that our algorithm computes this normal form in log linear (and thus sub-quadratic) time. We provide pseudocode and a minimal working implementation in Scala.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_11","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"196-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time"],"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-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. pp. 171\u2013177. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J. ACM 48(1), 70\u2013109 (2001). https:\/\/doi.org\/10.1145\/363647.363681","DOI":"10.1145\/363647.363681"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Bruns, G.: Free Ortholattices. Canadian Journal of Mathematics 28(5), 977\u2013985 (Oct 1976). https:\/\/doi.org\/10.4153\/CJM-1976-095-6","DOI":"10.4153\/CJM-1976-095-6"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 6015, pp. 150\u2013153. Springer, Berlin Heidelberg, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Brzozowski, J.: De Morgan bisemilattices. In: Proceedings 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2000). pp. 173\u2013178 (May 2000). https:\/\/doi.org\/10.1109\/ISMVL.2000.848616","DOI":"10.1109\/ISMVL.2000.848616"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Buss, S.R.: Alogtime algorithms for tree isomorphism, comparison, and canonization. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Computational Logic and Proof Theory. pp. 18\u201333. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)","DOI":"10.1007\/3-540-63385-5_30"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing. p. 151\u2013158. STOC \u201971, Association for Computing Machinery, New York, NY, USA (1971). https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (Jul 1962). https:\/\/doi.org\/10.1145\/368273.368557","DOI":"10.1145\/368273.368557"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Alur, R., Peled, D.A. (eds.) Computer Aided Verification, vol. 3114, pp. 175\u2013188. Springer, Berlin Heidelberg, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_14","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen. I. Mathematische Zeitschrift 39, 176\u2013210 (1935)","DOI":"10.1007\/BF01201353"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: Formalized foundations for the Stainless verifier. Proc. ACM Program. Lang 3 (November 2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Harrison, J.: HOL Light: An Overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, vol. 5674, pp. 60\u201366. Springer, Berlin Heidelberg, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"11_CR14","unstructured":"Hopcroft, J., UIIman, J., Aho, A.: The Design And Analysis Of Computer Algorithms. Addison-Wesley (1974)"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Hunt, H. B., I., Rosenkrantz, D.J., Bloniarz, P.A.: On the Computational Complexity of Algebra on Lattices. SIAM Journal on Computing 16(1), 129\u2013148 (Feb 1987). https:\/\/doi.org\/10.1137\/0216011","DOI":"10.1137\/0216011"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Kahn, A.B.: Topological sorting of large networks. Communications of the ACM 5(11), 558\u2013562 (Nov 1962). https:\/\/doi.org\/10.1145\/368996.369025","DOI":"10.1145\/368996.369025"},{"key":"11_CR17","unstructured":"Kalmbach, G.: Orthomodular Lattices. Academic Press Inc, London ; New York (Mar 1983)"},{"key":"11_CR18","unstructured":"Kraj\u00ed\u010dek, J.: Proof Complexity. Encyclopedia of Mathematics and Its Appplications, Vol. 170, Cambridge University Press (2019)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"key":"11_CR20","unstructured":"Kuncak, V.: Modular Data Structure Verification. Ph.D. thesis, EECS Department, Massachusetts Institute of Technology (February 2007), http:\/\/hdl.handle.net\/1721.1\/38533"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) Verified Software: Theories, Tools, Experiments. pp. 170\u2013190. Springer, Berlin Heidelberg, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_9","DOI":"10.1007\/978-3-642-54108-7_9"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Lewis, D.W.: Hazard detection by a quinary simulation of logic devices with bounded propagation delays. In: Proceedings of the 9th Design Automation Workshop. pp. 157\u2013164. DAC \u201972, Association for Computing Machinery, New York, NY, USA (Jun 1972). https:\/\/doi.org\/10.1145\/800153.804941","DOI":"10.1145\/800153.804941"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Lindell, S.: A logspace algorithm for tree canonization (extended abstract). In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing. p. 400\u2013404. STOC \u201992, Association for Computing Machinery, New York, NY, USA (1992). https:\/\/doi.org\/10.1145\/129712.129750","DOI":"10.1145\/129712.129750"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"McAllester, D.A.: Automatic recognition of tractability in inference relations. Journal of the ACM 40(2), 284\u2013303 (1993). https:\/\/doi.org\/10.1145\/151261.151265","DOI":"10.1145\/151261.151265"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Meinander, A.: A solution of the uniform word problem for ortholattices. Mathematical Structures in Computer Science 20(4), 625\u2013638 (Aug 2010). https:\/\/doi.org\/10.1017\/S0960129510000125","DOI":"10.1017\/S0960129510000125"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Merz, S., Vanzetto, H.: Automatic Verification of TLA + Proof Obligations with SMT Solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. pp. 289\u2013303. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_23","DOI":"10.1007\/978-3-642-28717-6_23"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: A brief overview of mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. pp. 67\u201372. Springer, Berlin Heidelberg, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_5","DOI":"10.1007\/978-3-642-03359-9_5"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233\u2013264 (Apr 1981). https:\/\/doi.org\/10.1145\/322248.322251","DOI":"10.1145\/322248.322251"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Pudl\u00e1k, P.: The Lengths of Proofs. In: Studies in Logic and the Foundations of Mathematics, vol. 137, pp. 547\u2013637. Elsevier (1998). https:\/\/doi.org\/10.1016\/S0049-237X(98)80023-2","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: Autoproof: Auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 566\u2013580. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (Jan 1987). https:\/\/doi.org\/10.1145\/7531.8928","DOI":"10.1145\/7531.8928"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Theorem Proving in Higher Order Logics. pp. 33\u201338. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2008). DOI: https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Whitman, P.M.: Free Lattices. Annals of Mathematics 42(1), 325\u2013330 (1941). https:\/\/doi.org\/10.2307\/1969001","DOI":"10.2307\/1969001"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI) (2008). https:\/\/doi.org\/10.1145\/1375581.1375624, see also [20]","DOI":"10.1145\/1375581.1375624"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"Zee, K., Kuncak, V., Rinard, M.: An integrated proof language for imperative programs. In: ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI) (2009). https:\/\/doi.org\/10.1145\/1543135.1542514","DOI":"10.1145\/1543135.1542514"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:47:01Z","timestamp":1710233221000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}