{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:31:56Z","timestamp":1784845916700,"version":"3.55.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T00:00:00Z","timestamp":1706832000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T00:00:00Z","timestamp":1706832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s10817-023-09693-z","type":"journal-article","created":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T14:03:41Z","timestamp":1706882621000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Non-termination in Term Rewriting and Logic Programming"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3519-025X","authenticated-orcid":false,"given":"\u00c9tienne","family":"Payet","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,2,2]]},"reference":[{"key":"9693_CR1","volume-title":"From Logic Programming to Prolog. Prentice Hall International series in computer science","author":"KR Apt","year":"1997","unstructured":"Apt, K.R.: From Logic Programming to Prolog. Prentice Hall International series in computer science. Prentice Hall, Hoboken (1997)"},{"key":"9693_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"1","key":"9693_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(91)90004-L","volume":"86","author":"RN Bol","year":"1991","unstructured":"Bol, R.N., Apt, K.R., Klop, J.W.: An analysis of loop checking mechanisms for logic programs. Theoret. Comput. Sci. 86(1), 35\u201379 (1991)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"9693_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0743-1066(99)00006-0","volume":"41","author":"M Codish","year":"1999","unstructured":"Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. J. Logic Program. 41(1), 103\u2013123 (1999)","journal-title":"J. Logic Program."},{"issue":"1\/2","key":"9693_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symbol. Comput. 3(1\/2), 69\u2013116 (1987)","journal-title":"J. Symbol. Comput."},{"key":"9693_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-31365-3_19","volume-title":"Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR\u201912)","author":"F Emmes","year":"2012","unstructured":"Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR\u201912). LNCS, vol. 7364, pp. 225\u2013240. Springer, Berlin (2012)"},{"key":"9693_CR7","unstructured":"Endrullis, J., Zantema, H.: Proving non-termination by finite automata. In: Fern\u00e1ndez, M. (ed.) Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA\u201915). Leibniz International Proceedings in Informatics (LIPIcs), vol. 36, pp. 160\u2013176. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2015)"},{"key":"9693_CR8","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/326619.326789","volume-title":"Proceedings of the 1994 ACM Symposium on Applied Computing (SAC\u201994)","author":"M Gabbrielli","year":"1994","unstructured":"Gabbrielli, M., Giacobazzi, R.: Goal independency and call patterns in the analysis of logic programs. In: Berghel, H., Hlengl, T., Urban, J.E. (eds.) Proceedings of the 1994 ACM Symposium on Applied Computing (SAC\u201994), pp. 394\u2013399. ACM, New York (1994)"},{"issue":"3","key":"9693_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1051\/ita:1999118","volume":"33","author":"A Geser","year":"1999","unstructured":"Geser, A., Zantema, H.: Non-looping string rewriting. RAIRO Theoret. Inf. Appl. 33(3), 279\u2013302 (1999)","journal-title":"RAIRO Theoret. Inf. Appl."},{"issue":"1","key":"9693_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Automat. Reason. 58(1), 3\u201331 (2017)","journal-title":"J. Automat. Reason."},{"key":"9693_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS\u201905)","author":"J Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS\u201905). LNAI, vol. 3717, pp. 216\u2013231. Springer, Berlin (2005)"},{"key":"9693_CR12","unstructured":"Giesl, J., et al.: AProVE (Automated Program Verification Environment). http:\/\/aprove.informatik.rwth-aachen.de\/ (2023)"},{"key":"9693_CR13","first-page":"147","volume-title":"Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201908)","author":"A Gupta","year":"2008","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201908), pp. 147\u2013158. ACM, New York (2008)"},{"issue":"1","key":"9693_CR14","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1137\/0212012","volume":"12","author":"JV Guttag","year":"1983","unstructured":"Guttag, J.V., Kapur, D., Musser, D.R.: On proving uniform termination and restricted termination of rewriting systems. SIAM J. Comput. 12(1), 189\u2013214 (1983)","journal-title":"SIAM J. Comput."},{"key":"9693_CR15","unstructured":"Hofbauer, D.: MnM (MultumNonMulta) (2023)"},{"issue":"2","key":"9693_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"9693_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"JW Lloyd","year":"1987","unstructured":"Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)","edition":"2"},{"key":"9693_CR18","unstructured":"Lucas, S., Guti\u00e9rrez, R.: MU-TERM. http:\/\/zenon.dsic.upv.es\/muterm\/ (2019)"},{"key":"9693_CR19","unstructured":"Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Diploma Thesis, HTWK Leipzig, Germany (2008)"},{"key":"9693_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Proceedings of the 5th GI-Conference on Theoretical Computer Science","author":"DMR Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of the 5th GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167\u2013183. Springer, Berlin (1981)"},{"issue":"2\u20133","key":"9693_CR21","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2008.05.013","volume":"403","author":"\u00c9 Payet","year":"2008","unstructured":"Payet, \u00c9.: Loop detection in term rewriting using the eliminating unfoldings. Theoret. Comput. Sci. 403(2\u20133), 307\u2013327 (2008)","journal-title":"Theoret. Comput. Sci."},{"key":"9693_CR22","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-13838-7_2","volume-title":"Proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR\u201918), Revised Selected Papers, LNCS","author":"\u00c9 Payet","year":"2018","unstructured":"Payet, \u00c9.: Guided unfoldings for finding loops in standard term rewriting. In: Mesnard, F., Stuckey, P.J. (eds.) Proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR\u201918), Revised Selected Papers, LNCS, vol. 11408, pp. 22\u201337. Springer, Berlin (2018)"},{"key":"9693_CR23","unstructured":"Payet, \u00c9.: Binary non-termination in term rewriting and logic programming. In: Yamada, A. (ed.) Proceedings of the 19th International Workshop on Termination (WST\u201923) (2023)"},{"key":"9693_CR24","unstructured":"Payet, \u00c9.: NTI (Non-Termination Inference). http:\/\/lim.univ-reunion.fr\/staff\/epayet\/Research\/NTI\/NTI.html and https:\/\/github.com\/etiennepayet\/nti (2023)"},{"issue":"2","key":"9693_CR25","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/1119479.1119481","volume":"28","author":"\u00c9 Payet","year":"2006","unstructured":"Payet, \u00c9., Mesnard, F.: Nontermination inference of logic programs. ACM Trans. Program. Lang. Syst. 28(2), 256\u2013289 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9693_CR26","unstructured":"Sahlin, D.: The Mixtus approach to automatic partial evaluation of full Prolog. In: Debray, S.K., Hermenegildo, M.V. editors, Proc. of the 1990 North American Conference on Logic Programming, pages 377\u2013398. MIT Press (1990)"},{"key":"9693_CR27","first-page":"649","volume-title":"Proceedings of the 7th International Conference on Logic Programming (ICLP\u201990)","author":"D De Schreye","year":"1990","unstructured":"De Schreye, D., Verschaetse, K., Bruynooghe, M.: A practical technique for detecting non-terminating queries for a restricted class of Horn clauses, using directed, weighted graphs. In: Warren, D.H.D., Szeredi, P. (eds.) Proceedings of the 7th International Conference on Logic Programming (ICLP\u201990), pp. 649\u2013663. MIT, New York (1990)"},{"issue":"2","key":"9693_CR28","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF03037237","volume":"15","author":"Y-D Shen","year":"1997","unstructured":"Shen, Y.-D.: An extended variant of atoms loop check for positive logic programs. New Gen Comput. 15(2), 187\u2013204 (1997)","journal-title":"New Gen Comput."},{"key":"9693_CR29","unstructured":"Sternagel, C., Middeldorp, A.: $${\\sf T}_{{\\sf T}}{\\sf T}_{{\\sf 2}}$$ (Tyrolean Termination Tool 2). http:\/\/cl-informatik.uibk.ac.at\/software\/ttt2\/ (2020)"},{"key":"9693_CR30","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)"},{"key":"9693_CR31","unstructured":"The Annual International Termination Competition. http:\/\/termination-portal.org\/wiki\/Termination_Competition"},{"key":"9693_CR32","unstructured":"Termination Problems Data Base. http:\/\/termination-portal.org\/wiki\/TPDB"},{"key":"9693_CR33","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-25979-4_6","volume-title":"Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA\u201904)","author":"J Waldmann","year":"2004","unstructured":"Waldmann, J.: Matchbox: a tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA\u201904). LNCS, vol. 3091, pp. 85\u201394. Springer, Berlin (2004)"},{"key":"9693_CR34","unstructured":"Wang, Y., Sakai, M.: On non-looping term rewriting. In: Geser, A., S\u00f8ndergaard, H. (ed.) Proceedings of the 8th International Workshop on Termination (WST\u201906), pp. 17\u201321 (2006)"},{"key":"9693_CR35","unstructured":"Yamada, A.: NaTT (Nagoya Termination Tool). https:\/\/www.trs.css.i.nagoya-u.ac.jp\/NaTT\/ (2023)"},{"key":"9693_CR36","unstructured":"Zankl, H., Middeldorp, A.: Nontermination of string rewriting using SAT. In: Hofbauer, D., Serebrenik, A. (ed.) Proceedings of the 9th International Workshop on Termination (WST\u201907), pp. 52\u201355 (2007)"},{"issue":"2","key":"9693_CR37","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10817-005-6545-0","volume":"34","author":"H Zantema","year":"2005","unstructured":"Zantema, H.: Termination of string rewriting proved automatically. J. Automat. Reason. 34(2), 105\u2013139 (2005)","journal-title":"J. Automat. Reason."},{"key":"9693_CR38","unstructured":"Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht. UU-CS, Department of Computer Science. Utrecht University, The Netherlands (1996)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09693-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09693-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09693-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T13:12:59Z","timestamp":1710767579000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09693-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,2]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["9693"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09693-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2,2]]},"assertion":[{"value":"30 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"4"}}