{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:54:17Z","timestamp":1725814457972},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319137698"},{"type":"electronic","value":"9783319137704"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13770-4_3","type":"book-chapter","created":{"date-parts":[[2014,12,8]],"date-time":"2014-12-08T13:36:05Z","timestamp":1418045765000},"page":"9-20","source":"Crossref","is-referenced-by-count":4,"title":["Models for Logics and Conditional Constraints in Automated Proofs of Termination"],"prefix":"10.1007","author":[{"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"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17796-5_12","volume-title":"Algebraic Methodology and Software Technology","author":"B. Alarc\u00f3n","year":"2011","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving Termination Properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol.\u00a06486, pp. 201\u2013208. Springer, Heidelberg (2011)"},{"key":"3_CR2","unstructured":"Alarc\u00f3n, B., Lucas, S., Navarro-Marset, R.: Using Matrix Interpretations over the Reals in Proofs of Termination. In: Proc. of PROLE 2009, pp. 255\u2013264 (2009)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"issue":"4","key":"3_CR4","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. of Aut. Reas.\u00a034(4), 325\u2013363 (2006)","journal-title":"J. of Aut. Reas."},{"issue":"2-3","key":"3_CR5","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. of Aut. Reas.\u00a040(2-3), 195\u2013220 (2008)","journal-title":"J. of Aut. Reas."},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-540-70590-1_8","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2008","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal Termination. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 110\u2013125. Springer, Heidelberg (2008)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific (1998)","DOI":"10.1142\/3831"},{"issue":"5","key":"3_CR8","first-page":"1","volume":"27","author":"P. Hudak","year":"1992","unstructured":"Hudak, P., Peyton-Jones, S.J., Wadler, P.: Report on the Functional Programming Language Haskell: a non\u2013strict, purely functional language. Sigplan Notices\u00a027(5), 1\u2013164 (1992)","journal-title":"Sigplan Notices"},{"issue":"1","key":"3_CR9","first-page":"1","volume":"1998","author":"S. Lucas","year":"1998","unstructured":"Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming\u00a01998(1), 1\u201361 (1998)","journal-title":"Journal of Functional and Logic Programming"},{"issue":"3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S. Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications\u00a039(3), 547\u2013586 (2005)","journal-title":"RAIRO Theoretical Informatics and Applications"},{"key":"3_CR11","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. Information Processing Letters\u00a095, 446\u2013453 (2005)","journal-title":"Information Processing Letters"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Proving Operational Termination of Declarative Programs in General Logics. In: Proc. of PPDP 2014, pp. 111\u2013122. ACM Digital Library (2014)","DOI":"10.1145\/2643135.2643152"},{"key":"3_CR13","unstructured":"Lucas, S., Meseguer, J.: 2D Dependency Pairs for Proving Operational Termination of CTRSs. In: Proc. of WRLA 2014. LNCS, vol. 8663 (to appear, 2014)"},{"key":"3_CR14","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: Extending the 2D DP Framework for CTRSs. In: Selected papers of LOPSTR 2014. LNCS (to appear, 2015)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: General Logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium 1987, pp. 275\u2013329. North-Holland (1989)","DOI":"10.1016\/S0049-237X(08)70132-0"},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S1471068410000025","volume":"11","author":"M.T. Nguyen","year":"2011","unstructured":"Nguyen, M.T., de Schreye, D., Giesl, J., Schneider-Kamp, P.: Polytool: Polynomial interpretations as a basis for termination of logic programs. Theory and Practice of Logic Programming\u00a011(1), 33\u201363 (2011)","journal-title":"Theory and Practice of Logic Programming"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (April 2002)","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Prestel, A., Delzell, C.N.: Positive Polynomials. In: From Hilbert\u2019s 17th Problem to Real Algebra. Springer, Berlin (2001)","DOI":"10.1007\/978-3-662-04648-7"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"3_CR20","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons (1986)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-62950-5_69","volume-title":"Rewriting Techniques and Applications","author":"H. Zantema","year":"1997","unstructured":"Zantema, H.: Termination of Context-Sensitive Rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 172\u2013186. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13770-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T23:34:24Z","timestamp":1559086464000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13770-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319137698","9783319137704"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13770-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}