{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:10:25Z","timestamp":1762459825979,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T00:00:00Z","timestamp":1579132800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T00:00:00Z","timestamp":1579132800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100007136","name":"Secretar\u00eda de Estado de Investigaci\u00f3n, Desarrollo e Innovaci\u00f3n","doi-asserted-by":"publisher","award":["RTI2018-094403-B-C32"],"award-info":[{"award-number":["RTI2018-094403-B-C32"]}],"id":[{"id":"10.13039\/501100007136","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100011596","name":"Conselleria d\u2019Educaci\u00f3, Investigaci\u00f3, Cultura i Esport","doi-asserted-by":"publisher","award":["PROMETEO\/2019\/098"],"award-info":[{"award-number":["PROMETEO\/2019\/098"]}],"id":[{"id":"10.13039\/501100011596","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004233","name":"Universitat Polit\u00e8cnica de Val\u00e8ncia","doi-asserted-by":"publisher","award":["SP20180225"],"award-info":[{"award-number":["SP20180225"]}],"id":[{"id":"10.13039\/501100004233","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 13-19109"],"award-info":[{"award-number":["CNS 13-19109"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009917","name":"U.S. Naval Research Laboratory","doi-asserted-by":"publisher","award":["N00173-17-1-G002"],"award-info":[{"award-number":["N00173-17-1-G002"]}],"id":[{"id":"10.13039\/100009917","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,12]]},"DOI":"10.1007\/s10817-020-09542-3","type":"journal-article","created":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T06:02:42Z","timestamp":1579154562000},"page":"1611-1662","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The 2D Dependency Pair Framework for Conditional Rewrite Systems\u2014Part II: Advanced Processors and Implementation Techniques"],"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"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,16]]},"reference":[{"issue":"1\u20132","key":"9542_CR1","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":"9542_CR2","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 (2011)","DOI":"10.1007\/978-3-642-17796-5_12"},{"key":"9542_CR3","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)"},{"key":"9542_CR4","volume-title":"Handbook of Mathematical Logic","author":"J Barwise","year":"1977","unstructured":"Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977)"},{"key":"9542_CR5","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 4350, Springer, New York (2007)"},{"issue":"4","key":"9542_CR6","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E Contejean","year":"2006","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325\u2013363 (2006)","journal-title":"J. Autom. Reason."},{"issue":"5","key":"9542_CR7","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett. 9(5), 212\u2013215 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9542_CR8","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: MTT: the Maude termination tool (system description). In: Proceedings of IJCAR\u201908, LNAI, vol. 5195, pp. 313\u2013319 (2008)","DOI":"10.1007\/978-3-540-71070-7_27"},{"issue":"2\u20133","key":"9542_CR9","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2\u20133), 195\u2013220 (2008)","journal-title":"J. Autom. Reason."},{"key":"9542_CR10","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination proofs in the dependency pair framework. In: Proceeding of IJCAR\u201906, LNAI, vol. 4130, pp. 281\u2013286 (2006)","DOI":"10.1007\/11814771_24"},{"key":"9542_CR11","doi-asserted-by":"crossref","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":"10.1007\/978-3-540-32275-7_21"},{"issue":"3","key":"9542_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":"9542_CR13","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)","DOI":"10.1007\/BFb0014969"},{"key":"9542_CR14","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Proceedings of CADE 2019, LNCS, vol. 11716, pp. 287\u2013299 (2019). Tool page: http:\/\/zenon.dsic.upv.es\/ages\/"},{"key":"9542_CR15","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proceedings of RTA\u201904, LNCS, vol. 3091, pp. 249\u2013268 (2004)","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"9542_CR16","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"W Hodges","year":"1983","unstructured":"Hodges, W.: Elementary predicate logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 1, pp. 1\u2013131. Reidel Publishing Company, Dordrecht (1983)"},{"key":"9542_CR17","unstructured":"Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979)"},{"key":"9542_CR18","doi-asserted-by":"publisher","unstructured":"Lucas, S.: Using Well-founded relations for proving operational termination. J. Autom. Reason. to appear (2020). https:\/\/doi.org\/10.1007\/s10817-019-09514-2","DOI":"10.1007\/s10817-019-09514-2"},{"issue":"4","key":"9542_CR19","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":"9542_CR20","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":"9542_CR21","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":"9542_CR22","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC\u201914, LNAI, vol. 8884, pp. 9\u201320 (2014)","DOI":"10.1007\/978-3-319-13770-4_3"},{"key":"9542_CR23","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: 2D Dependency pairs for proving operational termination of CTRSs. In: Escobar, S., (ed) Proceedings of the 10th International Workshop on Rewriting Logic and its Applications, WRLA\u201914, LNCS, vol. 8663, pp. 195\u2013212 (2014)","DOI":"10.1007\/978-3-319-12904-4_11"},{"key":"9542_CR24","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."},{"issue":"1","key":"9542_CR25","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","volume":"85","author":"S Lucas","year":"2016","unstructured":"Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Methods Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"9542_CR26","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: Extending the 2D DP framework for conditional term rewriting systems. In: Selected Papers from LOPSTR\u201914, LNCS, vol. 8981, pp. 113\u2013130 (2015)","DOI":"10.1007\/978-3-319-17822-6_7"},{"key":"9542_CR27","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.jcss.2018.04.002","volume":"96","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci. 96, 74\u2013106 (2018)","journal-title":"J. Comput. Syst. Sci."},{"key":"9542_CR28","unstructured":"McCune, W.: Prover9 & Mace4. http:\/\/www.cs.unm.edu\/~mccune\/prover9\/ (2005\u20132010)"},{"key":"9542_CR29","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, New York (2002)"},{"key":"9542_CR30","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":"9542_CR31","doi-asserted-by":"crossref","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Proceedings of RTA-TLCA\u201914, LNCS, vol. f8560, pp. 456\u2013465 (2014)","DOI":"10.1007\/978-3-319-08918-8_31"},{"key":"9542_CR32","unstructured":"Sternagel, T., Middeldorp, A.: Infeasible conditional critical pairs. In: Proceedings of IWC\u201915, pp. 13\u201318 (2014)"},{"key":"9542_CR33","unstructured":"Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD Thesis, RWTH Aachen, Technical Report AIB-2007-17 (2007)"},{"key":"9542_CR34","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of IJCAR\u201904, LNAI, vol. 3097, pp. 75\u201390 (2004)","DOI":"10.1007\/978-3-540-25984-8_4"},{"issue":"2","key":"9542_CR35","doi-asserted-by":"publisher","first-page":"105","DOI":"10.2307\/2266241","volume":"17","author":"H Wang","year":"1952","unstructured":"Wang, H.: Logic of many-sorted theories. J. Symb. Log. 17(2), 105\u2013116 (1952)","journal-title":"J. Symb. Log."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09542-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-020-09542-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09542-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,15]],"date-time":"2021-01-15T00:59:04Z","timestamp":1610672344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-020-09542-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,16]]},"references-count":35,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["9542"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09542-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,1,16]]},"assertion":[{"value":"4 February 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 January 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}