{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T02:14:29Z","timestamp":1783649669826,"version":"3.55.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"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,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"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>\n                    Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on\n                    <jats:italic>partial clauses<\/jats:italic>\n                    and\n                    <jats:italic>redundancy formulas<\/jats:italic>\n                    . The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover\n                    <jats:sc>Vampire<\/jats:sc>\n                    . Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of\n                    <jats:sc>Vampire<\/jats:sc>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_28","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:58Z","timestamp":1753789678000},"page":"532-551","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Partial Redundancy in Saturation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On Using Ground Joinable Equations in Equational Theorem Proving. Journal of Symbolic Computation (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00024-5","DOI":"10.1016\/S0747-7171(03)00024-5"},{"key":"28_CR2","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Equational problems. In: Term Rewriting and All That, chap.\u00a04. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"key":"28_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"},{"key":"28_CR4","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Dershowitz, N.: Critical Pair Criteria for Completion. Journal of Symbolic Computation (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80018-X","DOI":"10.1016\/S0747-7171(88)80018-X"},{"key":"28_CR5","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: CADE (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_105","DOI":"10.1007\/3-540-52885-7_105"},{"key":"28_CR6","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Automated Deduction: A Basis for Applications, vol.\u00a0I, chap.\u00a011. Springer (1998). https:\/\/doi.org\/10.1007\/978-94-017-0437-3","DOI":"10.1007\/978-94-017-0437-3"},{"key":"28_CR7","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":"28_CR8","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation. Information and Computation (1995). https:\/\/doi.org\/10.1006\/inco.1995.1131","DOI":"10.1006\/inco.1995.1131"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Chvalovsk\u00fd, K., Suda, M.: Regularization in Spider-Style Strategy Discovery and Schedule Construction. In: IJCAR (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_12","DOI":"10.1007\/978-3-031-63498-7_12"},{"key":"28_CR10","doi-asserted-by":"publisher","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for Full Higher-order Logic. In: CADE (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_23","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"28_CR11","doi-asserted-by":"publisher","unstructured":"Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition with Delayed Unification. In: CADE (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_2","DOI":"10.1007\/978-3-031-38499-8_2"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Comon, H.: Solving Symbolic Ordering Constraints. International Journal of Foundations of Computer Science (1990).https:\/\/doi.org\/10.1142\/S0129054190000278","DOI":"10.1142\/S0129054190000278"},{"key":"28_CR13","doi-asserted-by":"publisher","unstructured":"Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch, M.: Deciding the confluence of ordered term rewrite systems. ACM TOCL (2003). https:\/\/doi.org\/10.1145\/601775.601777","DOI":"10.1145\/601775.601777"},{"key":"28_CR14","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 (1995). https:\/\/doi.org\/10.1109\/LICS.1995.523272","DOI":"10.1109\/LICS.1995.523272"},{"key":"28_CR15","doi-asserted-by":"publisher","unstructured":"Dershowitz, N., Manna, Z.: Proving Termination with Multiset Orderings. Communications of the ACM (1979). https:\/\/doi.org\/10.1145\/359138.359142","DOI":"10.1145\/359138.359142"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"Desharnais, M., Toth, B., Waldmann, U., Blanchette, J., Tourret, S.: A Modular Formalization of Superposition in Isabelle\/HOL. In: ITP (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.12","DOI":"10.4230\/LIPIcs.ITP.2024.12"},{"key":"28_CR17","doi-asserted-by":"publisher","unstructured":"Duarte, A., Korovin, K.: Ground Joinability and Connectedness in the Superposition Calculus. In: IJCAR (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_11","DOI":"10.1007\/978-3-031-10769-6_11"},{"key":"28_CR18","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., Nieuwenhuis, R.: Constraints and Theorem Proving, p. 159\u2013201. Springer Berlin Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45406-3_4","DOI":"10.1007\/3-540-45406-3_4"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Coutelier, R., Kov\u00e1cs, L., Voronkov, A.: Term Ordering Diagrams (extended) (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.22181","DOI":"10.48550\/arXiv.2505.22181"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Kov\u00e1cs, L., Voronkov, A.: Partial Redundancy in Saturation (extended) (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.22213","DOI":"10.48550\/arXiv.2505.22213"},{"key":"28_CR21","doi-asserted-by":"publisher","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure. Journal of Symbolic Computation (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80019-1","DOI":"10.1016\/S0747-7171(88)80019-1"},{"key":"28_CR22","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with Symbolic Constraints. Research report, INRIA (1990), https:\/\/www.researchgate.net\/publication\/245850515"},{"key":"28_CR23","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. Springer (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_23","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Korovin, K.: iProver \u2014 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: IJCAR (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"28_CR25","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Knuth-Bendix Constraint Solving Is NP-Complete. In: ICALP (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_79","DOI":"10.1007\/3-540-48224-5_79"},{"key":"28_CR26","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"28_CR27","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. In: IJCAR (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_2","DOI":"10.1007\/978-3-540-25984-8_2"},{"key":"28_CR28","doi-asserted-by":"publisher","unstructured":"Lynch, C., Snyder, W.: Redundancy Criteria for Constrained Completion. In: RTA (1993). https:\/\/doi.org\/10.1007\/978-3-662-21551-7_2","DOI":"10.1007\/978-3-662-21551-7_2"},{"key":"28_CR29","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: Things to Know when Implementing KBO. Journal of Automated Reasoning (2006). https:\/\/doi.org\/10.1007\/s10817-006-9031-4","DOI":"10.1007\/s10817-006-9031-4"},{"key":"28_CR30","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, chap.\u00a07. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50009-6","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"28_CR31","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R.: Simple LPO constraint solving methods. Information Processing Letters (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90226-Y","DOI":"10.1016\/0020-0190(93)90226-Y"},{"key":"28_CR32","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic Superposition is Complete. In: ESOP (1992). https:\/\/doi.org\/10.1007\/3-540-55253-7_22","DOI":"10.1007\/3-540-55253-7_22"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation (1995).https:\/\/doi.org\/10.1006\/jsco.1995.1020","DOI":"10.1006\/jsco.1995.1020"},{"key":"28_CR34","doi-asserted-by":"publisher","unstructured":"Pais, J., Peterson, G.E.: Using forcing to prove completeness of resolution and paramodulation. Journal of Symbolic Computation (1991). https:\/\/doi.org\/10.1016\/S0747-7171(08)80130-7","DOI":"10.1016\/S0747-7171(08)80130-7"},{"key":"28_CR35","unstructured":"Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs (September 2016), https:\/\/isa-afp.org\/entries\/SuperCalc.html"},{"key":"28_CR36","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In: TACAS (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1","DOI":"10.1007\/978-3-319-89960-2_1"},{"key":"28_CR37","doi-asserted-by":"publisher","unstructured":"Riazanov, A., Voronkov, A.: Partially adaptive code trees. In: Logics in Artificial Intelligence (2000). https:\/\/doi.org\/10.1007\/3-540-40006-0_15","DOI":"10.1007\/3-540-40006-0_15"},{"key":"28_CR38","doi-asserted-by":"publisher","unstructured":"Riazanov, A., Voronkov, A.: Efficient Checking of Term Ordering Constraints. In: CADE (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_3","DOI":"10.1007\/978-3-540-25984-8_3"},{"key":"28_CR39","doi-asserted-by":"publisher","unstructured":"Robinson, G., Wos, L.: Paramodulation and Theorem-Proving in First-Order Theories with Equality, p. 298\u2013313. Springer Berlin Heidelberg, Berlin, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_19","DOI":"10.1007\/978-3-642-81955-1_19"},{"key":"28_CR40","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, Higher, Stronger: E 2.3. In: CADE (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"28_CR41","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: Stepping Stones in the TPTP World. In: IJCAR (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_3","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"28_CR42","doi-asserted-by":"publisher","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A Comprehensive Framework for Saturation Theorem Proving. Journal of Automated Reasoning (2022). https:\/\/doi.org\/10.1007\/S10817-022-09621-7","DOI":"10.1007\/S10817-022-09621-7"},{"key":"28_CR43","doi-asserted-by":"publisher","unstructured":"Zhang, H., Kapur, D.: Consider only General Superpositions in Completion Procedures. In: RTA (1989). https:\/\/doi.org\/10.1007\/3-540-51081-8_129","DOI":"10.1007\/3-540-51081-8_129"},{"key":"28_CR44","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 Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:26:01Z","timestamp":1781882761000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","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":"Stuttgart","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}