- -

Reducing relative termination to dependency pair problems

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Reducing relative termination to dependency pair problems

Mostrar el registro completo del ítem

Iborra, J.; Nishida, N.; Vidal Oriola, GF.; Yamada, A. (2015). Reducing relative termination to dependency pair problems. En Automated Deduction - CADE-25. Springer. 163-178. https://doi.org/10.1007/978-3-319-21401-6_11

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/65714

Ficheros en el ítem

Thumbnail
Nombre: paper_web.pdf
Tamaño: 495.4Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: springer_online.pdf
Tamaño: 266.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Reducing relative termination to dependency pair problems
Autor: Iborra, José Nishida, Naoki Vidal Oriola, Germán Francisco Yamada, Akihisa
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce ...[+]
Palabras clave: Termination , Term rewriting , Dependency pair , Program analysis
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-319-21400-9
Fuente:
Automated Deduction - CADE-25. (issn: 0302-9743 )
DOI: 10.1007/978-3-319-21401-6_11
Editorial:
Springer
Versión del editor: http://link.springer.com/chapter/10.1007/978-3-319-21401-6_11
Título del congreso: 25th International Conference on Automated Deduction (CADE - 25)
Lugar del congreso: Berlin, Germany
Fecha congreso: August 1-7, 2015
Serie: Lecture Notes in Computer Science;9195
Código del Proyecto:
info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/
info:eu-repo/grantAgreement/MINECO//TIN2013-44742-C4-1-R/ES/VALIDACION ASISTIDA DE PROGRAMAS MEDIANTE METODOS PRECISOS Y RIGUROSOS PARA UNA INGENIERIA DEL SOFTWARE ROBUSTA/
info:eu-repo/grantAgreement/FWF//Y 757/AT/Certifying termination and complexity proofs of programs/
Descripción: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21401-6_11
Agradecimientos:
Germán Vidal is partially supported by the EU (FEDER) and the Spanish Ministerio de Economía y Competitividad under grant TIN2013-44742-C4-R and by the Generalitat Valenciana under grant PROMETEOII201/013. Akihisa Yamadais ...[+]
Tipo: Capítulo de libro Comunicación en congreso

References

Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for A $$\vee $$ C-termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35–51. Springer, Heidelberg (2010)

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)

Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen (2001) [+]
Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for A $$\vee $$ C-termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35–51. Springer, Heidelberg (2010)

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)

Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen (2001)

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1&2), 69–115 (1987)

Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning 40(2–3), 195–220 (2008)

Geser, A.: Relative termination. Dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany (1990)

Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93–107. Springer, Heidelberg (2001)

Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155–203 (2006)

Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 185–198. Springer, Heidelberg (2004)

Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)

Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reasoning 47(4), 481–501 (2011)

Hullot, J.M.: Canonical forms and unification. CADE-5. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)

Iborra, J., Nishida, N., Vidal, G.: Goal-directed and relative dependency pairs for proving the termination of narrowing. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 52–66. Springer, Heidelberg (2010)

Kamin, S., Lévy, J.J.: Two generalizations of the recursive path ordering (1980, unpublished note)

Klop, J.W.: Term rewriting systems: a tutorial. Bull. Eur. Assoc. Theor. Comput. Sci. 32, 143–183 (1987)

Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 232–247. Springer, Heidelberg (2005)

Koprowski, A.: TPA: termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 257–266. Springer, Heidelberg (2006)

Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)

Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975)

Liu, J., Dershowitz, N., Jouannaud, J.-P.: Confluence by critical pair analysis. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 287–302. Springer, Heidelberg (2014)

Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables. ENTCS 86(3), 52–69 (2003)

Nishida, N., Vidal, G.: Termination of narrowing via termination of rewriting. Appl. Algebra Eng. Commun. Comput. 21(3), 177–225 (2010)

Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer-Verlag, London (2002)

Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: RTA 2012. LIPIcs, vol. 15, pp. 339–354. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Vidal, G.: Termination of narrowing in left-linear constructor systems. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 113–129. Springer, Heidelberg (2008)

Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 466–475. Springer, Heidelberg (2014)

Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. (2014). doi: 10.1016/j.scico.2014.07.009

Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24(1/2), 89–105 (1995)

Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181–259. Cambridge University Press, Cambridge (2003)

[-]

recommendations

 

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro completo del ítem