{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:13:03Z","timestamp":1760015583306,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_2","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"23-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Superposition with\u00a0Delayed Unification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1343-5084","authenticated-orcid":false,"given":"Ahmed","family":"Bhayat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5550-196X","authenticated-orcid":false,"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, chap. 8, pp. 447\u2013533 (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"10th International Conference on Automated Deduction","author":"L Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 427\u2013441. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_105"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-55602-8_185","volume-title":"Automated Deduction\u2014CADE-11","author":"L Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 462\u2013476. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_185"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints (1997)","DOI":"10.1007\/BFb0054259"},{"key":"2_CR6","unstructured":"Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Logical Methods Comput. Sci. 17 (2021)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-030-29436-6_4","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Bentkamp","year":"2019","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 55\u201373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_4"},{"issue":"4","key":"2_CR8","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-51074-9_16","volume-title":"Automated Reasoning","author":"A Bhayat","year":"2020","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 278\u2013296. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_16"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Domenjoud, E.: A technical note on AC-unification. The number of minimal unifiers of the equation $$\\alpha x_1+ \\cdots + \\alpha x_p \\doteq _{AC} \\beta y_1 + \\cdots + \\beta y_q$$. J. Autom. Reason. 8 (1992)","DOI":"10.1007\/BF00263448"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS (LNAI), vol. 5803, pp. 435\u2013443. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04617-9_55"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"GP Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed $$\\lambda $$-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-031-30823-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Korovin","year":"2023","unstructured":"Korovin, K., Kov\u00e1cs, L., Reger, G., Schoisswohl, J., Voronkov, A.: ALASCA: reasoning in quantified linear arithmetic. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 647\u2013665. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_33"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-55253-7_22","volume-title":"ESOP \u201992","author":"R Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic superposition is complete. In: Krieg-Br\u00fcckner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 371\u2013389. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55253-7_22"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: LICS, pp. 64\u201374. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-89960-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2018","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 3\u201322. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1"},{"issue":"2,3","key":"2_CR18","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2,3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-31365-3_37","volume-title":"Automated Reasoning","author":"S Schulz","year":"2012","unstructured":"Schulz, S.: Fingerprint indexing for paramodulation and rewriting. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 477\u2013483. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_37"},{"issue":"1\u20132","key":"2_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1\u20132), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-53904-2_93","volume-title":"Rewriting Techniques and Applications","author":"W Snyder","year":"1991","unstructured":"Snyder, W., Lynch, C.: Goal directed strategies for paramodulation. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 150\u2013161. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53904-2_93"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108\u2013116. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_8"},{"issue":"1","key":"2_CR23","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-030-51074-9_18","volume-title":"Automated Reasoning","author":"U Waldmann","year":"2020","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 316\u2013334. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_18"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:57Z","timestamp":1693609437000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","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":"77","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":"28","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":"5","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":"36% - 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":"6","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)"}}]}}