{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:11Z","timestamp":1784844431442,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"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>We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inference rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the <jats:sc>Vampire<\/jats:sc> theorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_10","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"154-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Synthesis of\u00a0Recursive Programs in\u00a0Saturation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0845-5811","authenticated-orcid":false,"given":"Petra","family":"Hozzov\u00e1","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0954-7881","authenticated-orcid":false,"given":"Daneshvar","family":"Amrollahi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"additional","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"}]},{"given":"Eva Maria","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"10_CR1","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, pp. 1\u201325 (2015)"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P.: A Taxonomy of theorem-proving strategies. In: Artificial Intelligence Today: Recent Trends and Developments, pp. 43\u201384 (1999). https:\/\/doi.org\/10.1007\/3-540-48317-9_3","DOI":"10.1007\/3-540-48317-9_3"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-030-81685-8_4","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2021","unstructured":"D\u2019Antoni, L., Hu, Q., Kim, J., Reps, T.: Programmable program synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 84\u2013109. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_4"},{"key":"10_CR4","first-page":"183","volume":"4","author":"C Green","year":"1969","unstructured":"Green, C.: Theorem-proving by resolution as a basis for question-answering systems. Mach. Intell. 4, 183\u2013205 (1969)","journal-title":"Mach. Intell."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with Generalization in Superposition Reasoning. In: CICM, pp. 123\u2013137 (2020) https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"10_CR6","unstructured":"Hajdu, M., Kov\u00e1cs, L., Rawson, M., Voronkov, A.: The Vampire Approach to Induction. In: Practical Aspects of Automated Reasoning (2022)"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: FMCAD, pp. 1\u201310 (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_34","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_34"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Norman, C., Voronkov, A.: Program synthesis in saturation. In: CADE, pp. 307\u2013324 (2023)","DOI":"10.1007\/978-3-031-38499-8_18"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Integer induction in saturation. In: CADE, pp. 361\u2013377 (2021)","DOI":"10.1007\/978-3-030-79876-5_21"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Hozzov\u00e1, P., Amrollahi, D., Hajdu, M., Kov\u00e1cs, L., Voronkov, A., Wagner, E.M.: Synthesis of Recursive Programs in Saturation. EasyChair Preprint no. 12145, EasyChair (2024)","DOI":"10.1007\/978-3-031-63498-7_10"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Inala, J.P., Polikarpova, N., Qiu, X., Lerner, B.S., Solar-Lezama, A.: Synthesis of recursive ADT transformations from reusable templates. In: TACAS, pp. 247\u2013263 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_14","DOI":"10.1007\/978-3-662-54577-5_14"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, R.N.S., Sergey, I.: Cyclic program synthesis. In: PLDI, pp. 944\u2013959 (2021). https:\/\/doi.org\/10.1145\/3453483.3454087","DOI":"10.1145\/3453483.3454087"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Kim, J., Hu, Q., D\u2019Antoni, L., Reps, T.: Semantics-guided synthesis. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434311","DOI":"10.1145\/3434311"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S Kleene","year":"1945","unstructured":"Kleene, S.: On the interpretation of intuitionistic number theory. J. Symb. Log. 10, 109\u2013124 (1945)","journal-title":"J. Symb. Log."},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA, pp. 407\u2013426 (2013). https:\/\/doi.org\/10.1145\/2509136.2509555","DOI":"10.1145\/2509136.2509555"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV, pp. 1\u201335 (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/360924.360967","volume":"4","author":"RCT Lee","year":"1974","unstructured":"Lee, R.C.T., Waldinger, R.J., Chang, C.L.: An improved program-synthesizing algorithm and its correctness. Commun. ACM 4, 211\u2013217 (1974). https:\/\/doi.org\/10.1145\/360924.360967","journal-title":"Commun. ACM"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Milicevic, A.: Program extrapolation with Jennisys. In: OOPSLA, pp. 411\u2013430. OOPSLA \u201912 (2012). https:\/\/doi.org\/10.1145\/2384616.2384646","DOI":"10.1145\/2384616.2384646"},{"issue":"8","key":"10_CR19","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1109\/32.153379","volume":"18","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Waldinger, R.: Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18(8), 674\u2013704 (1992). https:\/\/doi.org\/10.1109\/32.153379","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"10_CR20","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980). https:\/\/doi.org\/10.1145\/357084.357090","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Miltner, A., Nu\u00f1ez, A.T., Brendel, A., Chaudhuri, S., Dillig, I.: Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498682","DOI":"10.1145\/3498682"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, vol.\u00a0I, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. ACM SIGPLAN Notices 51(6), 522\u2013538 (2016). https:\/\/doi.org\/10.1145\/2980983.2908093","DOI":"10.1145\/2980983.2908093"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Sergey, I.: Structuring the synthesis of heap-manipulating programs. 3(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3290385","DOI":"10.1145\/3290385"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in Saturation-Based Proof Search. In: CADE, pp. 477\u2013494 (2019)","DOI":"10.1007\/978-3-030-29436-6_28"},{"issue":"2","key":"10_CR26","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/S10703-017-0270-2","volume":"55","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C.W., Deters, M.: Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2), 73\u2013102 (2019). https:\/\/doi.org\/10.1007\/S10703-017-0270-2","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"10_CR27","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T Rybina","year":"2001","unstructured":"Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Trans. Comput. Log. 2(2), 155\u2013181 (2001). https:\/\/doi.org\/10.1145\/371316.371494","journal-title":"ACM Trans. Comput. Log."},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326 (2010). https:\/\/doi.org\/10.1145\/1706299.1706337","DOI":"10.1145\/1706299.1706337"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Tammet, T.: Completeness of resolution for definite answers. J. Logic Comput. 5(4), 449\u2013471 (1995)","DOI":"10.1093\/logcom\/5.4.449"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:36Z","timestamp":1747592256000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}