- -

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 sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: paper_web.pdf
Tamaño: 495.4Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: springer_online.pdf
Tamaño: 266.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Iborra, José es_ES
dc.contributor.author Nishida, Naoki es_ES
dc.contributor.author Vidal Oriola, Germán Francisco es_ES
dc.contributor.author Yamada, Akihisa es_ES
dc.date.accessioned 2016-06-13T08:38:40Z
dc.date.available 2016-06-13T08:38:40Z
dc.date.issued 2015-07-25
dc.identifier.isbn 978-3-319-21400-9
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/65714
dc.description The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21401-6_11 es_ES
dc.description.abstract 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 a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation. es_ES
dc.description.sponsorship 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 supported by the Austrian Science Fund (FWF): Y757 es_ES
dc.format.extent 16 es_ES
dc.language Inglés es_ES
dc.publisher Springer es_ES
dc.relation.ispartof Automated Deduction - CADE-25 es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;9195
dc.rights Reserva de todos los derechos es_ES
dc.subject Termination es_ES
dc.subject Term rewriting es_ES
dc.subject Dependency pair es_ES
dc.subject Program analysis es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Reducing relative termination to dependency pair problems es_ES
dc.type Capítulo de libro es_ES
dc.type Comunicación en congreso es_ES
dc.identifier.doi 10.1007/978-3-319-21401-6_11
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ es_ES
dc.relation.projectID 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/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/FWF//Y 757/AT/Certifying termination and complexity proofs of programs/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 25th International Conference on Automated Deduction (CADE - 25) es_ES
dc.relation.conferencedate August 1-7, 2015 es_ES
dc.relation.conferenceplace Berlin, Germany es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-319-21401-6_11 es_ES
dc.description.upvformatpinicio 163 es_ES
dc.description.upvformatpfin 178 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.senia 302344 es_ES
dc.contributor.funder Ministerio de Economía y Competitividad es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Austrian Science Fund es_ES
dc.description.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) es_ES
dc.description.references Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000) es_ES
dc.description.references Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen (2001) es_ES
dc.description.references Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) es_ES
dc.description.references Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1&2), 69–115 (1987) es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning 40(2–3), 195–220 (2008) es_ES
dc.description.references Geser, A.: Relative termination. Dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany (1990) es_ES
dc.description.references Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93–107. Springer, Heidelberg (2001) es_ES
dc.description.references 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) es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155–203 (2006) es_ES
dc.description.references 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) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reasoning 47(4), 481–501 (2011) es_ES
dc.description.references Hullot, J.M.: Canonical forms and unification. CADE-5. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980) es_ES
dc.description.references 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) es_ES
dc.description.references Kamin, S., Lévy, J.J.: Two generalizations of the recursive path ordering (1980, unpublished note) es_ES
dc.description.references Klop, J.W.: Term rewriting systems: a tutorial. Bull. Eur. Assoc. Theor. Comput. Sci. 32, 143–183 (1987) es_ES
dc.description.references 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) es_ES
dc.description.references Koprowski, A.: TPA: termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 257–266. Springer, Heidelberg (2006) es_ES
dc.description.references 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) es_ES
dc.description.references Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975) es_ES
dc.description.references 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) es_ES
dc.description.references Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables. ENTCS 86(3), 52–69 (2003) es_ES
dc.description.references Nishida, N., Vidal, G.: Termination of narrowing via termination of rewriting. Appl. Algebra Eng. Commun. Comput. 21(3), 177–225 (2010) es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer-Verlag, London (2002) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. (2014). doi: 10.1016/j.scico.2014.07.009 es_ES
dc.description.references Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24(1/2), 89–105 (1995) es_ES
dc.description.references 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) es_ES


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

Mostrar el registro sencillo del ítem