{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:41:22Z","timestamp":1726188082293},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"7-8","license":[{"start":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T00:00:00Z","timestamp":1713571200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T00:00:00Z","timestamp":1713571200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2024,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list <jats:inline-formula><jats:alternatives><jats:tex-math>$$ nil $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>nil<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and the operation <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textit{cons}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>cons<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, that adds an element to the front of a list. First we show that, for <jats:inline-formula><jats:alternatives><jats:tex-math>$$m \\ge 1$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>m<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, quantifier-free <jats:inline-formula><jats:alternatives><jats:tex-math>$$m$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>m<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-step induction does not simulate quantifier-free <jats:inline-formula><jats:alternatives><jats:tex-math>$$(m + 1)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>m<\/mml:mi>\n                    <mml:mo>+<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-step induction. Secondly, we show that for all <jats:inline-formula><jats:alternatives><jats:tex-math>$$m \\ge 1$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>m<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, quantifier-free <jats:inline-formula><jats:alternatives><jats:tex-math>$$m$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>m<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-step induction does not prove the right cancellation property of the concatenation operation on lists defined by left-recursion.\n<\/jats:p>","DOI":"10.1007\/s00153-024-00923-8","type":"journal-article","created":{"date-parts":[[2024,4,21]],"date-time":"2024-04-21T02:37:57Z","timestamp":1713667077000},"page":"813-835","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantifier-free induction for lists"],"prefix":"10.1007","volume":"63","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jannik","family":"Vierling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,20]]},"reference":[{"issue":"3","key":"923_CR1","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1134\/S0037446619030029","volume":"60","author":"SA Aleksandrova","year":"2019","unstructured":"Aleksandrova, S.A., Bazhenov, N.A.: On decidability of list structures. Sib. Math. J. 60(3), 377\u2013388 (2019)","journal-title":"Sib. Math. J."},{"key":"923_CR2","first-page":"714","volume":"12","author":"NA Bazhenov","year":"2015","unstructured":"Bazhenov, N.A.: Automatic structures and the theory of lists. Sib. Electron. Math. Rep. 12, 714\u2013722 (2015)","journal-title":"Sib. Electron. Math. Rep."},{"key":"923_CR3","first-page":"350","volume-title":"Programming Languages and Systems, volume 7705 of Lecture Notes in Computer Science","author":"J Brotherston","year":"2012","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems, volume 7705 of Lecture Notes in Computer Science, pp. 350\u2013367. Springer, Berlin (2012)"},{"key":"923_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling\u2014Meta-Level Guidance for Mathematical Reasoning, Volume 56 of Cambridge Tracts in Theoretical Computer Science","author":"A Bundy","year":"2005","unstructured":"Bundy, A., Basin, D.A., Hutter, D., Ireland, A.: Rippling\u2014Meta-Level Guidance for Mathematical Reasoning, Volume 56 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2005)"},{"key":"923_CR5","first-page":"359","volume-title":"Proceedings of the Eleventh International Joint Conference on Artificial Intelligence","author":"A Bundy","year":"1989","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A., Stevens, A.: A rational reconstruction and extension of recursion analysis. In: Sridharan, N.S. (ed.) Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, vol. 1, pp. 359\u2013365. Morgan Kaufmann, Burlington (1989)"},{"key":"923_CR6","first-page":"392","volume-title":"Automated Deduction\u2014CADE-24, Volume 7898 of Lecture Notes in Computer Science","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) Automated Deduction\u2014CADE-24, Volume 7898 of Lecture Notes in Computer Science, pp. 392\u2013406. Springer, Berlin (2013)"},{"key":"923_CR7","first-page":"333","volume-title":"Intelligent Computer Mathematics, Volume 9150 of Lecture Notes in Computer Science","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: TIP: Tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics, Volume 9150 of Lecture Notes in Computer Science, pp. 333\u2013337. Springer, Berlin (2015)"},{"key":"923_CR8","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chapter 14, pp. 913\u2013962. North-Holland, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"issue":"4","key":"923_CR9","doi-asserted-by":"publisher","first-page":"625","DOI":"10.2307\/2272846","volume":"39","author":"J Corcoran","year":"1974","unstructured":"Corcoran, J., Frank, W., Maloney, M.: String theory. J. Symb. Logic 39(4), 625\u2013637 (1974)","journal-title":"J. Symb. Logic"},{"key":"923_CR10","first-page":"172","volume-title":"Frontiers of Combining Systems, Volume 10483 of Lecture Notes in Computer Science","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems, Volume 10483 of Lecture Notes in Computer Science, pp. 172\u2013188. Springer, Berlin (2017)"},{"key":"923_CR11","first-page":"70","volume-title":"Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science","author":"SH Einarsd\u00f3ttir","year":"2018","unstructured":"Einarsd\u00f3ttir, S.H., Johansson, M., Pohjola, J.\u00c5.: Into the infinite\u2014theory exploration for coinduction. In: Fleuriot, J.D., Wang, D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science, pp. 70\u201386. Springer, Berlin (2018)"},{"key":"923_CR12","first-page":"84","volume":"114","author":"SS Goncharov","year":"1986","unstructured":"Goncharov, S.S.: A theory of lists and its models. Vychislitel\u2019nye Sistemy 114, 84\u201395 (1986)","journal-title":"Vychislitel\u2019nye Sistemy"},{"issue":"2","key":"923_CR13","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s11225-005-2976-1","volume":"79","author":"A Grzegorczyk","year":"2005","unstructured":"Grzegorczyk, A.: Undecidability without arithmetization. Stud. Logica 79(2), 163\u2013230 (2005)","journal-title":"Stud. Logica"},{"key":"923_CR14","first-page":"72","volume-title":"Andrzej Mostowski and Foundational Studies","author":"A Grzegorczyk","year":"2008","unstructured":"Grzegorczyk, A., Zdanowski, K.: Undecidability and Concatenation. In: Ehrenfeucht, A., Marek, V.W., Srebrny, M. (eds.) Andrzej Mostowski and Foundational Studies, pp. 72\u201391. IOS Press, Amsterdam (2008)"},{"key":"923_CR15","first-page":"123","volume-title":"Intelligent Computer Mathematics, volume 12236 of Lecture Notes in Computer Science","author":"M Hajd\u00fa","year":"2020","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: Benzm\u00fcller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics, volume 12236 of Lecture Notes in Computer Science, pp. 123\u2013137. Springer, Berlin (2020)"},{"key":"923_CR16","first-page":"246","volume-title":"Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2021, volume 2 of Conference Series: Formal Methods in Computer-Aided Design","author":"M Hajdu","year":"2021","unstructured":"Hajdu, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: Piskac, R., Whalen, M.W. (eds.) Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2021, volume 2 of Conference Series: Formal Methods in Computer-Aided Design, pp. 246\u2013255. TU Wien Academic Press, Vienna (2021)"},{"issue":"4","key":"923_CR17","first-page":"11:1","volume":"16","author":"S Hetzl","year":"2020","unstructured":"Hetzl, S., Vierling, J.: Clause Set Cycles and Induction. Log. Methods Comput. Sci. 16(4), 11:1-11:17 (2020)","journal-title":"Log. Methods Comput. Sci."},{"key":"923_CR18","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Vierling, J.: Unprovability results for clause set cycles. Theor. Comput. Sci. (2022)","DOI":"10.1016\/j.tcs.2022.07.003"},{"key":"923_CR19","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Vierling, J.: Induction and Skolemization in saturation theorem proving. Ann. Pure Appl. Logic 174(1) (2023)","DOI":"10.1016\/j.apal.2022.103167"},{"issue":"4","key":"923_CR20","first-page":"10:1","volume":"13","author":"S Hetzl","year":"2018","unstructured":"Hetzl, S., Wong, T.L.: Some observations on the logical foundations of inductive theorem proving. Log. Methods Comput. Sci. 13(4), 10:1-10:26 (2018)","journal-title":"Log. Methods Comput. Sci."},{"key":"923_CR21","first-page":"7","volume-title":"Frontiers of Combining Systems, volume 8152 of Lecture Notes in Computer Science","author":"A Kersani","year":"2013","unstructured":"Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Frontiers of Combining Systems, volume 8152 of Lecture Notes in Computer Science, pp. 7\u201322. Springer, Berlin (2013)"},{"key":"923_CR22","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF00289260","volume":"15","author":"DJ Moore","year":"1981","unstructured":"Moore, D.J., Russell, B.: Axiomatic data type specifications: a first order theory of linear lists. Acta Informatica 15, 193\u2013207 (1981)","journal-title":"Acta Informatica"},{"key":"923_CR23","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201978, pp. 151\u2013157. Association for Computing Machinery, New York, NY, USA (1978)","DOI":"10.1145\/512760.512776"},{"issue":"4","key":"923_CR24","doi-asserted-by":"publisher","first-page":"105","DOI":"10.2307\/2268308","volume":"11","author":"WV Quine","year":"1946","unstructured":"Quine, W.V.: Concatenation as a basis for arithmetic. J. Symb. Logic 11(4), 105\u2013114 (1946)","journal-title":"J. Symb. Logic"},{"key":"923_CR25","doi-asserted-by":"crossref","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.), Automated Deduction\u2014CADE 27, volume 11716 of Lecture Notes in Computer Science, pp. 477\u2013494. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-29436-6_28"},{"key":"923_CR26","first-page":"382","volume-title":"FM 2014: Formal Methods, volume 8442 of Lecture Notes in Computer Science","author":"K Rustan","year":"2014","unstructured":"Rustan, K., Leino, M., Moskal, M.: Co-induction simply\u2014automatic co-inductive proofs in a program verifier. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods, volume 8442 of Lecture Notes in Computer Science, pp. 382\u2013398. Springer, Berlin (2014)"},{"issue":"1","key":"923_CR27","doi-asserted-by":"publisher","first-page":"7","DOI":"10.2307\/2964452","volume":"23","author":"JR Shoenfield","year":"1958","unstructured":"Shoenfield, J.R.: Open sentences and the induction axiom. J. Symb. Log. 23(1), 7\u201312 (1958)","journal-title":"J. Symb. Log."},{"key":"923_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9915-5","volume-title":"Introduction to Axiomatic Set Theory, volume 1 of Graduate Texts in Mathematics","author":"G Takeuti","year":"1971","unstructured":"Takeuti, G., Zaring, W.M.: Introduction to Axiomatic Set Theory, volume 1 of Graduate Texts in Mathematics. Springer, Berlin (1971)"},{"key":"923_CR29","first-page":"261","volume":"1","author":"A Tarski","year":"1935","unstructured":"Tarski, A.: Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1, 261\u2013405 (1935)","journal-title":"Studia Philosophica"},{"issue":"2","key":"923_CR30","doi-asserted-by":"publisher","first-page":"182","DOI":"10.2307\/2269809","volume":"31","author":"JW Thatcher","year":"1966","unstructured":"Thatcher, J.W.: Decision problems for multiple successor arithmetics. J. Symb. Logic 31(2), 182\u2013190 (1966)","journal-title":"J. Symb. Logic"},{"key":"923_CR31","unstructured":"Vierling, J.: The limits of automated inductive theorem provers. Ph.D. thesis, Technische Universit\u00e4t Wien (2022)"},{"issue":"1","key":"923_CR32","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1215\/00294527-2008-028","volume":"50","author":"A Visser","year":"2009","unstructured":"Visser, A., Commas, G.: A study of sequentiality and concatenation. Notre Dame J. Formal Logic 50(1), 61\u201385 (2009)","journal-title":"Notre Dame J. Formal Logic"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00923-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-024-00923-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00923-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T04:02:57Z","timestamp":1726113777000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-024-00923-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,20]]},"references-count":32,"journal-issue":{"issue":"7-8","published-print":{"date-parts":[[2024,11]]}},"alternative-id":["923"],"URL":"https:\/\/doi.org\/10.1007\/s00153-024-00923-8","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2024,4,20]]},"assertion":[{"value":"27 April 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}