{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:03:32Z","timestamp":1725516212457},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_1","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"1-16","source":"Crossref","is-referenced-by-count":5,"title":["Modular Termination of Basic Narrowing"],"prefix":"10.1007","author":[{"given":"Mar\u00eda","family":"Alpuente","sequence":"first","affiliation":[]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Iborra","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Modular termination of basic narrowing. Technical Report DSIC-II\/04\/08, Universidad Polit\u00e9cnica de Valencia (2007)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Termination of Narrowing revisited. Theoretical Computer Science (to appear, 2008)","DOI":"10.1016\/j.tcs.2009.07.037"},{"key":"1_CR3","first-page":"49","volume-title":"Logic Programming Languages","author":"M. Alpuente","year":"1993","unstructured":"Alpuente, M., Falaschi, M., Gabbrielli, M., Levi, G.: The semantics of equational logic programming as an instance of CLP. In: Logic Programming Languages, pp. 49\u201381. The MIT Press, Cambridge (1993)"},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(94)00224-7","volume":"142","author":"M. Alpuente","year":"1995","unstructured":"Alpuente, M., Falaschi, M., Levi, G.: Incremental Constraint Satisfaction for Equational Logic Programming. Theoretical Computer Science\u00a0142(1), 27\u201357 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"1_CR5","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.\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Proc. of the 8th Int\u2019l Conf. on Automated Deduction, January 1986, pp. 5\u201320 (1986)","DOI":"10.1007\/3-540-16780-3_76"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Foundations of Software Science and Computation Structures","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H.: Intruder Theories (Ongoing Work). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 1\u20134. Springer, Heidelberg (2004)"},{"issue":"1","key":"1_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V. Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A Survey of Algebraic Properties used in Cryptographic Protocols. Journal of Computer Security\u00a014(1), 1\u201343 (2006)","journal-title":"Journal of Computer Security"},{"key":"1_CR9","first-page":"244","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 244\u2013320. Elsevier Science, Amsterdam (1990)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties. TCS\u00a0367 (2006)","DOI":"10.1016\/j.tcs.2006.08.035"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S. Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 153\u2013168. Springer, Heidelberg (2007)"},{"key":"1_CR12","unstructured":"Fay, M.: First-Order Unification in an Equational Theory. In: Fourth Int\u2019l Conf. on Automated Deduction, pp. 161\u2013167 (1979)"},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19&20","author":"M. Hanus","year":"1994","unstructured":"Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming\u00a019&20, 583\u2013628 (1994)","journal-title":"Journal of Logic Programming"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Equational Logic Programming","year":"1989","unstructured":"H\u00f6lldobler, S. (ed.): Foundations of Equational Logic Programming. LNCS, vol.\u00a0353. Springer, Heidelberg (1989)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical Forms and Unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"1_CR16","unstructured":"Hullot, J.-M.: Compilation de Formes Canoniques dans les Th\u00e9ories q\u0301uationelles. Th\u00e9se de Doctorat de Troisi\u00e8me Cycle. PhD thesis, Universit\u00e9 de Paris Sud, Orsay (France) (1981)"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0013826","volume-title":"Algebraic and Logic Programming","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 158\u2013200. Springer, Heidelberg (1992)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. HOSC, 123\u2013160 (2007)","DOI":"10.1007\/s10990-007-9000-6"},{"key":"1_CR19","first-page":"313","volume":"5","author":"A. Middeldorp","year":"1994","unstructured":"Middeldorp, A., Hamoen, E.: Completeness Results for Basic Narrowing. J. of Applicable Algebra in Engineering, Comm. and Computing\u00a05, 313\u2013353 (1994)","journal-title":"J. of Applicable Algebra in Engineering, Comm. and Computing"},{"key":"1_CR20","doi-asserted-by":"crossref","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, Heidelberg (2002)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0016858","volume-title":"Constraints in Computational Logics","author":"C. Prehofer","year":"1994","unstructured":"Prehofer, C.: On Modularity in Term Rewriting and Narrowing. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol.\u00a0845, pp. 253\u2013268. Springer, Heidelberg (1994)"},{"key":"1_CR22","unstructured":"Krishna Rao, M.R.K.: Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science (January 1995)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"P. R\u00e9ty","year":"1987","unstructured":"R\u00e9ty, P.: Improving Basic Narrowing Techniques. In: Lescanne, P. (ed.) RTA 1987. LNCS, vol.\u00a0256. Springer, Heidelberg (1987)"},{"volume-title":"Term Rewriting Systems","year":"2003","key":"1_CR24","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"issue":"3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett.\u00a025(3), 141\u2013143 (1987)","journal-title":"Inf. Process. Lett."},{"issue":"4","key":"1_CR26","first-page":"315","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain, X.: Modular & incremental automated termination proofs. Int. J. Approx. Reasoning\u00a032(4), 315\u2013355 (2004)","journal-title":"Int. J. Approx. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:08:17Z","timestamp":1605762497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}