- -

Relative Termination via Dependency Pairs

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Relative Termination via Dependency Pairs

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: paper.pdf
Tamaño: 363.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: jar_paper_online_ ...
Tamaño: 610.1Kb
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 es_ES
dc.contributor.author Yamada, Akihisa es_ES
dc.date.accessioned 2018-06-08T04:24:48Z
dc.date.available 2018-06-08T04:24:48Z
dc.date.issued 2017 es_ES
dc.identifier.issn 0168-7433 es_ES
dc.identifier.uri http://hdl.handle.net/10251/103613
dc.description.abstract [EN] A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel 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. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation. es_ES
dc.description.sponsorship Open access funding provided by Austrian Science Fund (FWF). We would like to thank Nao Hirokawa, Keiichirou Kusakari, and the anonymous reviewers for their helpful comments and suggestions in early stages of this work. es_ES
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation.ispartof Journal of Automated Reasoning es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Term rewriting es_ES
dc.subject Dependency pairs es_ES
dc.subject Termination es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Relative Termination via Dependency Pairs es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s10817-016-9373-5 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/J4FWF/START-Programm/Y 757/AT/
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/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ 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, G.; Yamada, A. (2017). Relative Termination via Dependency Pairs. Journal of Automated Reasoning. 58(3):391-411. https://doi.org/10.1007/s10817-016-9373-5 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion http://doi.org/10.1007/s10817-016-9373-5 es_ES
dc.description.upvformatpinicio 391 es_ES
dc.description.upvformatpfin 411 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 58 es_ES
dc.description.issue 3 es_ES
dc.identifier.pmid 30174365 en_EN
dc.identifier.pmcid PMC6109893 en_EN
dc.relation.pasarela S\352631 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Ministerio de Economía, Industria y Competitividad es_ES
dc.description.references Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for A $$\vee $$ ∨ C-termination. In: WRLA 2010, LNCS, vol. 6381, pp. 36–52. Springer (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 Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6, 1–18 (1988) es_ES
dc.description.references Bonacina, M., Hsiang, J.: On fairness of completion-based theorem proving strategies. In: RTA 1991, LNCS, vol. 488, pp. 348–360. Springer (1991) 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. Reason. 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: RTA 2001, LNCS, vol. 2051, pp. 93–107. Springer (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: IJCAR 2006, LNCS, vol. 4130, pp. 281–286. Springer (2006) es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency Pairs. J. Autom. Reason. 37(3), 155–203 (2006) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: RTA 2004, LNCS, vol. 3091, pp. 249–268. Springer (2004) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: AISC 2004, LNAI, vol. 3249, pp. 185–198. Springer (2004) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474–511 (2007) es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reason. 47(4), 481–501 (2011) es_ES
dc.description.references Hullot, J.M.: Canonical forms and unification. In: CADE 1980, LNCS, vol. 87, pp. 318–334. Springer (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: LOPSTR 2009, LNCS, vol. 6037, pp. 52–66. Springer (2010) es_ES
dc.description.references Iborra, J., Nishida, N., Vidal, G., Yamada, A.: Reducing relative termination to dependency pair problems. In: CADE-25, LNAI, vol. 9195, pp. 163–178. Springer (2015) 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.: TPA: termination proved automatically. In: RTA 2006, LNCS, vol. 4098, pp. 257–266. Springer (2006) es_ES
dc.description.references Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: FroCoS 2005, LNCS, vol. 3717, pp. 232–247. Springer (2005) es_ES
dc.description.references Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: RTA 2009, LNCS, vol. 5595, pp. 295–304. Springer (2009) es_ES
dc.description.references Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Trans. Inf. Syst. E84–D(5), 439–447 (2001) 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 Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38(1), 873–897 (2004) 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, London (2002) es_ES
dc.description.references Slagle, J.: Automated theorem-proving for theories with simplifiers commutativity and associativity. J. ACM 21(4), 622–642 (1974) 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: FLOPS 2008, LNCS, vol. 4989, pp. 113–129. Springer (2008) es_ES
dc.description.references Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: RTA-TLCA 2014, LNCS, pp. 466–475. Springer (2014) es_ES
dc.description.references Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. 111, 110–134 (2015) es_ES
dc.description.references Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inf. 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, chap. 6, 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