{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:06Z","timestamp":1747593606964,"version":"3.40.5"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Modern superposition inference systems aim at reducing the search space by introducing redundancy criteria on clauses and inferences. This paper focuses on reducing the number of superposition inferences with a single clause by blocking inferences into some terms, provided there were previously made inferences of a certain form performed with predecessors of this clause. Other calculi based on blocking inferences, for example basic superposition, rely on variable abstraction or equality constraints to express irreducibility of terms, resulting however in blocking inferences with all subterms of the respective terms. Here we introduce reducibility constraints in superposition to enable a more expressive blocking mechanism for inferences. We show that our calculus remains (refutationally) complete and present redundancy notions. Our implementation in the theorem prover Vampire demonstrates a considerable reduction in the size of the search space when using our new calculus.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_8","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"115-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reducibility Constraints in\u00a0Superposition"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0747-7171(03)00024-5","volume":"36","author":"J Avenhaus","year":"2003","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On Using Ground Joinable Equations in Equational Theorem Proving. J. Symb. Comput. 36(1), 217\u2013233 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00024-5","journal-title":"J. Symb. Comput."},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Equational problems. In: Term Rewriting and All That, p. 58-92. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L.: Canonical Equational Proofs. Progress in theoretical computer science, Birkh\u00e4user (1991). https:\/\/doi.org\/10.1007\/978-1-4684-7118-2","DOI":"10.1007\/978-1-4684-7118-2"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L Bachmair","year":"1988","unstructured":"Bachmair, L., Dershowitz, N.: Critical Pair Criteria for Completion. J. Symb. Comput. 6(1), 1\u201318 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80018-X","journal-title":"J. Symb. Comput."},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction: A Basis for Applications, vol.\u00a0I, chap.\u00a011, pp. 353\u2013397. Springer (1998). https:\/\/doi.org\/10.1007\/978-94-017-0437-3","DOI":"10.1007\/978-94-017-0437-3"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, pp. 19\u201399. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50004-7","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation and Superposition. In: CADE. pp. 462\u2013476 (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_185","DOI":"10.1007\/3-540-55602-8_185"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition with Delayed Unification. In: CADE. pp. 23\u201340 (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_2","DOI":"10.1007\/978-3-031-38499-8_2"},{"issue":"04","key":"8_CR9","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1142\/S0129054190000278","volume":"01","author":"H Comon","year":"1990","unstructured":"Comon, H.: Solving Symbolic Ordering Constraints. Int. J. Found. Comput. Sci. 01(04), 387\u2013411 (1990). https:\/\/doi.org\/10.1142\/S0129054190000278","journal-title":"Int. J. Found. Comput. Sci."},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Comon, H., Nieuwenhuis, R., Rubio, A.: Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract). In: Annual IEEE Symposium on Logic in Computer Science. pp. 375\u2013385 (1995). https:\/\/doi.org\/10.1109\/LICS.1995.523272","DOI":"10.1109\/LICS.1995.523272"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - A Distributed and Learning Equational Prover. J. Autom. Reason. 18(2), 189\u2013198 (1997). https:\/\/doi.org\/10.1023\/A:1005879229581","journal-title":"J. Autom. Reason."},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Dershowitz, N., Manna, Z.: Proving Termination with Multiset Orderings. Commun. ACM 22(8), 465-476 (aug 1979). https:\/\/doi.org\/10.1145\/359138.359142","DOI":"10.1145\/359138.359142"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Duarte, A., Korovin, K.: Ground Joinability and Connectedness in the Superposition Calculus. In: IJCAR. pp. 169\u2013187 (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_11","DOI":"10.1007\/978-3-031-10769-6_11"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Gleiss, B., Kov\u00e1cs, L., Rath, J.: Subsumption Demodulation in First-Order Theorem Proving. In: IJCAR. pp. 297\u2013315 (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_17","DOI":"10.1007\/978-3-030-51074-9_17"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Hajdu, M., Kov\u00e1cs, L., Rawson, M., Voronkov, A.: Reducibility constraints in superposition. EasyChair Preprint no. 12142 (EasyChair, 2024)","DOI":"10.1007\/978-3-031-63498-7_8"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Hullot, J.M.: Canonical Forms and Unification. In: CADE. pp. 318\u2013334 (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_25","DOI":"10.1007\/3-540-10009-1_25"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"6","author":"D Kapur","year":"1988","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure. J. Symb. Comput. 6(1), 19\u201336 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80019-1","journal-title":"J. Symb. Comput."},{"key":"8_CR18","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with Symbolic Constraints. Research Report RR-1358, INRIA (1990)"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 342\u2013376. Springer (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_23","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Knuth-Bendix Constraint Solving Is NP-Complete. In: Automata, Languages and Programming. pp. 979\u2013992 (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_79","DOI":"10.1007\/3-540-48224-5_79"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV. pp. 1\u201335 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. In: IJCAR. pp. 45\u201359 (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_2","DOI":"10.1007\/978-3-540-25984-8_2"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Lynch, C., Snyder, W.: Redundancy Criteria for Constrained Completion. In: RTA. pp. 2\u201316 (1993). https:\/\/doi.org\/10.1007\/978-3-662-21551-7_2","DOI":"10.1007\/978-3-662-21551-7_2"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins Problem. J. Autom. Reason. 19, 263\u2013276 (1997). https:\/\/doi.org\/10.1023\/A:1005843212881","journal-title":"J. Autom. Reason."},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, vol.\u00a0I, chap.\u00a07, pp. 371\u2013443. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50009-6","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic Superposition is Complete. In: ESOP. pp. 371\u2013389 (1992). https:\/\/doi.org\/10.1007\/3-540-55253-7_22","DOI":"10.1007\/3-540-55253-7_22"},{"issue":"3\u20134","key":"8_CR27","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W Nutt","year":"1989","unstructured":"Nutt, W., R\u00e9ty, P., Smolka, G.: Basic Narrowing Revisited. J. Symb. Comput. 7(3\u20134), 295\u2013317 (1989). https:\/\/doi.org\/10.1016\/S0747-7171(89)80014-8","journal-title":"J. Symb. Comput."},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In: TACAS. pp. 3\u201322 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1","DOI":"10.1007\/978-3-319-89960-2_1"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, Higher, Stronger: E 2.3. In: CADE. pp. 495\u2013507 (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"issue":"2","key":"8_CR30","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"8_CR31","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac068","author":"G Sutcliffe","year":"2022","unstructured":"Sutcliffe, G.: The Logic Languages of the TPTP World. Logic Journal of the IGPL (2022). https:\/\/doi.org\/10.1093\/jigpal\/jzac068","journal-title":"Logic Journal of the IGPL"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: The Architecture for First-Order Theorem Provers. In: CAV. pp. 696\u2013710 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","DOI":"10.1007\/978-3-319-08867-9_46"},{"issue":"4","key":"8_CR33","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/S10817-022-09621-7","volume":"66","author":"U Waldmann","year":"2022","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. J. Autom. Reason. 66(4), 499\u2013539 (2022). https:\/\/doi.org\/10.1007\/S10817-022-09621-7","journal-title":"J. Autom. Reason."},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE. pp. 140\u2013145 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Zhang, H., Kapur, D.: Consider only General Superpositions in Completion Procedures. In: RTA. pp. 513\u2013527 (1989). https:\/\/doi.org\/10.1007\/3-540-51081-8_129","DOI":"10.1007\/3-540-51081-8_129"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Zhang, H., Kapur, D.: Unnecessary Inferences in Associative-Commutative Completion Procedures. In: Mathematical Systems Theory (1990). https:\/\/doi.org\/10.1007\/BF02090774","DOI":"10.1007\/BF02090774"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:15Z","timestamp":1747592235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}