- -

The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques

Mostrar el registro completo del ítem

Lucas Alba, S.; Meseguer, J.; Gutiérrez Gil, R. (2020). The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques. Journal of Automated Reasoning. 64(8):1611-1662. https://doi.org/10.1007/s10817-020-09542-3

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

Ficheros en el ítem

Thumbnail
Nombre: LucasMeseguerGutierrez ...
Tamaño: 776.2Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: LucMesGUt_The2DDe ...
Tamaño: 1.128Mb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques
Autor: Lucas Alba, Salvador Meseguer, José Gutiérrez Gil, Raúl
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] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...[+]
Palabras clave: Conditional term rewriting , Dependency pairs , Program analysis , Operational termination
Derechos de uso: Reserva de todos los derechos
Fuente:
Journal of Automated Reasoning. (issn: 0168-7433 )
DOI: 10.1007/s10817-020-09542-3
Editorial:
Springer-Verlag
Versión del editor: https://doi.org/10.1007/s10817-020-09542-3
Código del Proyecto:
info:eu-repo/grantAgreement/UPV//SP20180225/
info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/
info:eu-repo/grantAgreement/NRL//N00173-17-1-G002/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/
Agradecimientos:
Partially supported by the EU (FEDER) and projects RTI2018-094403-B-C32, PROMETEO/2019/098, SP20180225. Jose Meseguer was supported by grants NSF CNS 13-19109 and NRL N00173-17-1-G002. Salvador Lucas' research was partly ...[+]
Tipo: Artículo

References

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

Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10, LNCS, vol. 6486, pp. 201–208 (2011)

Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998) [+]
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)

Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10, LNCS, vol. 6486, pp. 201–208 (2011)

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

Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework. LNCS 4350, Springer, New York (2007)

Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2006)

Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett. 9(5), 212–215 (1979)

Durán, F., Lucas, S., Meseguer, J.: MTT: the Maude termination tool (system description). In: Proceedings of IJCAR’08, LNAI, vol. 5195, pp. 313–319 (2008)

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

Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination proofs in the dependency pair framework. In: Proceeding of IJCAR’06, LNAI, vol. 4130, pp. 281–286 (2006)

Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of LPAR’04, LNAI, vol. 3452, pp. 301–331 (2004)

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

Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87, LNCS, vol. 250, pp. 1–22 (1987)

Gutiérrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Proceedings of CADE 2019, LNCS, vol. 11716, pp. 287–299 (2019). Tool page: http://zenon.dsic.upv.es/ages/

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

Hodges, W.: Elementary predicate logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 1, pp. 1–131. Reidel Publishing Company, Dordrecht (1983)

Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979)

Lucas, S.: Using Well-founded relations for proving operational termination. J. Autom. Reason. to appear (2020). https://doi.org/10.1007/s10817-019-09514-2

Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)

Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018)

Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)

Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC’14, LNAI, vol. 8884, pp. 9–20 (2014)

Lucas, S., Meseguer, J.: 2D Dependency pairs for proving operational termination of CTRSs. In: Escobar, S., (ed) Proceedings of the 10th International Workshop on Rewriting Logic and its Applications, WRLA’14, LNCS, vol. 8663, pp. 195–212 (2014)

Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)

Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Methods Program. 85(1), 67–97 (2016)

Lucas, S., Meseguer, J., Gutiérrez, R.: Extending the 2D DP framework for conditional term rewriting systems. In: Selected Papers from LOPSTR’14, LNCS, vol. 8981, pp. 113–130 (2015)

Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci. 96, 74–106 (2018)

McCune, W.: Prover9 & Mace4. http://www.cs.unm.edu/~mccune/prover9/ (2005–2010)

Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002)

Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659–688 (2010)

Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Proceedings of RTA-TLCA’14, LNCS, vol. f8560, pp. 456–465 (2014)

Sternagel, T., Middeldorp, A.: Infeasible conditional critical pairs. In: Proceedings of IWC’15, pp. 13–18 (2014)

Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD Thesis, RWTH Aachen, Technical Report AIB-2007-17 (2007)

Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of IJCAR’04, LNAI, vol. 3097, pp. 75–90 (2004)

Wang, H.: Logic of many-sorted theories. J. Symb. Log. 17(2), 105–116 (1952)

[-]

recommendations

 

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

Mostrar el registro completo del ítem