{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:25:59Z","timestamp":1725863159067},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319448015"},{"type":"electronic","value":"9783319448022"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-44802-2_2","type":"book-chapter","created":{"date-parts":[[2016,8,17]],"date-time":"2016-08-17T16:32:52Z","timestamp":1471451572000},"page":"26-46","source":"Crossref","is-referenced-by-count":1,"title":["Use of Logical Models for Proving Operational Termination in General Logics"],"prefix":"10.1007","author":[{"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,18]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6486, pp. 201\u2013208. Springer, Heidelberg (2011)"},{"key":"2_CR2","unstructured":"Alarc\u00f3n, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Lucio, F., Moreno, G., Pe\u00f1a, R.. (eds.) Proceedings of the IX Jornadas Sobre Programaci\u00f3n y Lenguajes, PROLE 2009, pp. 255\u2013264, September 2009"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"issue":"5","key":"2_CR4","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Rybalchenko, A., Podelski, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"issue":"1\u20132","key":"2_CR5","doi-asserted-by":"crossref","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 Symbolic Comput. 21(1\u20132), 59\u201388 (2008)","journal-title":"High.-Order Symbolic Comput."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0014969","volume-title":"TAPSOFT 1987","author":"J Goguen","year":"1987","unstructured":"Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalsky, R.A., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1\u201322. Springer, Heidelberg (1987)"},{"key":"2_CR7","doi-asserted-by":"crossref","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."},{"key":"2_CR8","unstructured":"Guti\u00e9rrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories (Submitted). http:\/\/zenon.dsic.upv.es\/ages\/"},{"issue":"3","key":"2_CR9","doi-asserted-by":"crossref","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 Theor. Inform. Appl. 39(3), 547\u2013586 (2005)","journal-title":"RAIRO Theor. Inform. Appl."},{"key":"2_CR10","doi-asserted-by":"crossref","first-page":"32","DOI":"10.4204\/EPTCS.200.3","volume":"200","author":"S Lucas","year":"2015","unstructured":"Lucas, S.: Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving. Electron. Proc. Theor. Comput. Sci. 200, 32\u201347 (2015)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"2_CR11","doi-asserted-by":"crossref","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. Inform. Proc. Lett. 95, 446\u2013453 (2005)","journal-title":"Inform. Proc. Lett."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","first-page":"7","volume-title":"Artificial Intelligence and Symbolic Computation","author":"S Lucas","year":"2014","unstructured":"Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Aranda-Corral, G.A., Calmet, J., Mart\u00edn-Mateos, F.J. (eds.) AISC 2014. LNCS (LNAI), vol. 8884, pp. 7\u201318. Springer, Heidelberg (2014)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Operational termination of membership equational programs: the order-sorted way. In: Rosu, G. (ed.) Proceedings of the 7th International Workshop on Rewriting Logic and its Applications, WRLA 2008. Electronic Notes in Theoretical Computer Science, vol. 238, pp. 207\u2013225 (2009)","DOI":"10.1016\/j.entcs.2009.05.021"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Danvy, O. (ed.) Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014, pp. 111\u2013122. ACM Digital Library (2014)","DOI":"10.1145\/2643135.2643152"},{"key":"2_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"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"2_CR17","unstructured":"Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Schmidt-Schauss, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. LIPICS, vol. 10, pp. 251\u2013266 (2011)"},{"key":"2_CR18","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)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44802-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:53:17Z","timestamp":1498337597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44802-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319448015","9783319448022"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44802-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}