- -

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

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

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

Ficheros en el ítem

Thumbnail
Nombre: paper.pdf
Tamaño: 363.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: jar_paper_online_ ...
Tamaño: 610.1Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Relative Termination via Dependency Pairs
Autor: Iborra, José Nishida, Naoki Vidal Oriola, Germán 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:
[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 ...[+]
Palabras clave: Term rewriting , Dependency pairs , Termination
Derechos de uso: Reserva de todos los derechos
Fuente:
Journal of Automated Reasoning. (issn: 0168-7433 )
DOI: 10.1007/s10817-016-9373-5
Editorial:
Springer-Verlag
Versión del editor: http://doi.org/10.1007/s10817-016-9373-5
Código del Proyecto:
info:eu-repo/grantAgreement/J4FWF/START-Programm/Y 757/AT/
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/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/
Agradecimientos:
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.
Tipo: Artículo

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)

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: WRLA 2010, LNCS, vol. 6381, pp. 36–52. Springer (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)

Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6, 1–18 (1988)

Bonacina, M., Hsiang, J.: On fairness of completion-based theorem proving strategies. In: RTA 1991, LNCS, vol. 488, pp. 348–360. Springer (1991)

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. Reason. 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: RTA 2001, LNCS, vol. 2051, pp. 93–107. Springer (2001)

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)

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

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

Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: AISC 2004, LNAI, vol. 3249, pp. 185–198. Springer (2004)

Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474–511 (2007)

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

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

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)

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)

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.: TPA: termination proved automatically. In: RTA 2006, LNCS, vol. 4098, pp. 257–266. Springer (2006)

Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: FroCoS 2005, LNCS, vol. 3717, pp. 232–247. Springer (2005)

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

Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Trans. Inf. Syst. E84–D(5), 439–447 (2001)

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

Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38(1), 873–897 (2004)

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, London (2002)

Slagle, J.: Automated theorem-proving for theories with simplifiers commutativity and associativity. J. ACM 21(4), 622–642 (1974)

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: FLOPS 2008, LNCS, vol. 4989, pp. 113–129. Springer (2008)

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

Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. 111, 110–134 (2015)

Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inf. 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, chap. 6, 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