{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:14Z","timestamp":1762459694691,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T00:00:00Z","timestamp":1549843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"MINECO","award":["TIN2015-69175-C4-1-R"],"award-info":[{"award-number":["TIN2015-69175-C4-1-R"]}]},{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["PROMETEOII\/2015\/013"],"award-info":[{"award-number":["PROMETEOII\/2015\/013"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1007\/s10817-019-09514-2","type":"journal-article","created":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T07:01:58Z","timestamp":1549868518000},"page":"167-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Using Well-Founded Relations for Proving Operational Termination"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9923-2108","authenticated-orcid":false,"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,11]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST\u201910, LNCS, vol. 6486, pp. 201\u2013208, Springer (2011)","key":"9514_CR1","DOI":"10.1007\/978-3-642-17796-5_12"},{"issue":"4","key":"9514_CR2","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10817-017-9417-5","volume":"60","author":"L Aguirre","year":"2018","unstructured":"Aguirre, L., Mart\u00ed-Oliet, N., Palomino, M., Pita, I.: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. J. Automat. Reason. 60(4), 421\u2013463 (2018)","journal-title":"J. Automat. Reason."},{"key":"9514_CR3","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-62950-5_68","volume-title":"Rewriting Techniques and Applications","author":"Thomas Arts","year":"1997","unstructured":"Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA\u201997, LNCS, vol. 1232, pp. 157\u2013171, Springer, Berlin (1997)"},{"issue":"1\u20132","key":"9514_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9514_CR5","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)"},{"unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude\u2014A High-Performance Logical Framework. LNCS, vol. 4350, Springer (2007)","key":"9514_CR6"},{"key":"9514_CR7","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2009.07.062","volume":"248","author":"F Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electron. Notes Theor. Comput. Sci. 248, 93\u2013113 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"9514_CR8","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10990-008-9028-2","volume":"21","author":"F Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., March\u00e9, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. High. Order Symb. Comput. 21(1\u20132), 59\u201388 (2008)","journal-title":"High. Order Symb. Comput."},{"key":"9514_CR9","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.entcs.2009.03.036","volume":"237","author":"S Falke","year":"2009","unstructured":"Falke, S., Kapur, D.: Operational termination of conditional rewriting with built-in numbers and semantic data structures. Electron. Notes Theor. Comput. Sci. 237, 75\u201390 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9514_CR10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19\u201332 (1967)","journal-title":"Math. Asp. Comput. Sci."},{"key":"9514_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39\u201372 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"3","key":"9514_CR12","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reason."},{"key":"9514_CR13","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J\u00fcrgen Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of LPAR\u201904, LNAI, vol. 3452, pp. 301\u2013331 (2004)"},{"doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Proceedings of IJCAR\u201906, LNAI, vol. 4130, pp. 281\u2013286 (2006)","key":"9514_CR14","DOI":"10.1007\/11814771_24"},{"doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT\u201987, LNCS, vol. 250, pp. 1\u201322 (1987)","key":"9514_CR15","DOI":"10.1007\/BFb0014969"},{"key":"9514_CR16","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Guti\u00e9rrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE\u201916, pp. 215\u2013230 (2016)","key":"9514_CR17"},{"key":"9514_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"W Hodges","year":"1993","unstructured":"Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)"},{"key":"9514_CR19","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"Martin Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proceedings of RTA 2009, LNCS, vol. 5595, pp. 295\u2013304 (2009)"},{"key":"9514_CR20","volume-title":"Computation as Logic","author":"R Lalement","year":"1993","unstructured":"Lalement, R.: Computation as Logic. Masson-Prentice Hall International, Paris (1993)"},{"issue":"1","key":"9514_CR21","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1016\/S0890-5401(02)93176-7","volume":"178","author":"S Lucas","year":"2002","unstructured":"Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294\u2013343 (2002)","journal-title":"Inf. Comput."},{"unstructured":"Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA\u201916, LNCS, vol. 9942, pp. 1\u201321 (2016)","key":"9514_CR22"},{"unstructured":"Lucas, S.: Directions of operational termination. In: Proceedings of PROLE\u201918. \nhttp:\/\/hdl.handle.net\/11705\/PROLE\/2018\/009\n\n (2018). Accessed 9 Feb 2019","key":"9514_CR23"},{"issue":"4","key":"9514_CR24","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10817-017-9419-3","volume":"60","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465\u2013501 (2018)","journal-title":"J. Autom. Reason."},{"key":"9514_CR25","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.ipl.2018.04.002","volume":"136","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90\u201395 (2018)","journal-title":"Inf. Process. Lett."},{"key":"9514_CR26","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446\u2013453 (2005)","journal-title":"Inf. Process. Lett."},{"key":"9514_CR27","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/j.jlamp.2016.03.003","volume":"86","author":"S Lucas","year":"2017","unstructured":"Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236\u2013268 (2017)","journal-title":"J. Log. Algebr. Methods Program."},{"doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP\u201914, pp. 111\u2013122. ACM Digital Library (2014)","key":"9514_CR28","DOI":"10.1145\/2643135.2643152"},{"unstructured":"McCune, W.: Prover9 & Mace4. \nhttp:\/\/www.cs.unm.edu\/~mccune\/prover9\/\n\n (2005\u20132010). Accessed 9 Feb 2019","key":"9514_CR29"},{"key":"9514_CR30","volume-title":"Introduction to Mathematical Logic","author":"E Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, London (1997)","edition":"4"},{"key":"9514_CR31","first-page":"275","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Jos\u00e9 Meseguer","year":"1989","unstructured":"Meseguer, J.: General logics. In: Logic Colloquium\u201987, pp. 275\u2013329 (1989)"},{"key":"9514_CR32","volume-title":"Equational Logic as a Programming Language","author":"MJ O\u2019Donnell","year":"1985","unstructured":"O\u2019Donnell, M.J.: Equational Logic as a Programming Language. The MIT Press, Cambridge (1985)"},{"key":"9514_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002)"},{"unstructured":"Prawitz, D.: Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965. Reprinted by Dover Publications (2006)","key":"9514_CR34"},{"doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.M.: One-path reachability logic. In: Proceedings of LICS 2013, pp. 358\u2013367. IEEE Press (2013)","key":"9514_CR35","DOI":"10.1109\/LICS.2013.42"},{"key":"9514_CR36","volume-title":"Foundations Without Foundationalism: A Case for Second-Order Logic","author":"S Shapiro","year":"1991","unstructured":"Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991)"},{"key":"9514_CR37","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1016\/j.jlap.2009.08.001","volume":"79","author":"F Schernhammer","year":"2010","unstructured":"Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659\u2013688 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"9514_CR38","first-page":"19","volume-title":"Lecture Notes in Computer Science","author":"Traian Florin \u015eerb\u0103nu\u0163\u0103","year":"2006","unstructured":"Serbanuta, T., Rosu, G.: Computationally equivalent elimination of conditions. In: Proceedings of RTA\u201906, LNCS, vol. 4098, pp. 19\u201334. Springer, Berlin (2006)"},{"unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67\u201369 (1949)","key":"9514_CR39"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09514-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09514-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09514-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,10]],"date-time":"2020-02-10T19:07:42Z","timestamp":1581361662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09514-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,11]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["9514"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09514-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,2,11]]},"assertion":[{"value":"29 June 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 February 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}