- -

Using Well-Founded Relations for Proving Operational Termination

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Using Well-Founded Relations for Proving Operational Termination

Mostrar el registro completo del ítem

Lucas Alba, S. (2020). Using Well-Founded Relations for Proving Operational Termination. Journal of Automated Reasoning. 64(2):167-195. https://doi.org/10.1007/s10817-019-09514-2

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

Ficheros en el ítem

Thumbnail
Nombre: Lucas - Using ...
Tamaño: 727.4Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Lucas_UsingWellFo ...
Tamaño: 772.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Using Well-Founded Relations for Proving Operational Termination
Autor: Lucas Alba, Salvador
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] In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different ...[+]
Palabras clave: Declarative languages , Logical models , Operational termination , Program analysis , Well-foundedness
Derechos de uso: Reserva de todos los derechos
Fuente:
Journal of Automated Reasoning. (issn: 0168-7433 )
DOI: 10.1007/s10817-019-09514-2
Editorial:
Springer-Verlag
Versión del editor: https://doi.org/10.1007/s10817-019-09514-2
Código del Proyecto:
info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/
info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/
info:eu-repo/grantAgreement/UPV//SP20180225/
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), Projects TIN2015-69175-C4-1-R, and GV PROMETEOII/2015/013.
Tipo: Artículo

References

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, Springer (2011)

Aguirre, L., Martí-Oliet, N., Palomino, M., Pita, I.: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. J. Automat. Reason. 60(4), 421–463 (2018)

Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA’97, LNCS, vol. 1232, pp. 157–171, Springer, Berlin (1997) [+]
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, Springer (2011)

Aguirre, L., Martí-Oliet, N., Palomino, M., Pita, I.: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. J. Automat. Reason. 60(4), 421–463 (2018)

Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA’97, LNCS, vol. 1232, pp. 157–171, Springer, Berlin (1997)

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

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

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, vol. 4350, Springer (2007)

Durán, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electron. Notes Theor. Comput. Sci. 248, 93–113 (2009)

Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. High. Order Symb. Comput. 21(1–2), 59–88 (2008)

Falke, S., Kapur, D.: Operational termination of conditional rewriting with built-in numbers and semantic data structures. Electron. Notes Theor. Comput. Sci. 237, 75–90 (2009)

Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967)

Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001)

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (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., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Proceedings of IJCAR’06, LNAI, vol. 4130, pp. 281–286 (2006)

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

Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217–273 (1992)

Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE’16, pp. 215–230 (2016)

Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)

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

Lalement, R.: Computation as Logic. Masson-Prentice Hall International, Paris (1993)

Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002)

Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA’16, LNCS, vol. 9942, pp. 1–21 (2016)

Lucas, S.: Directions of operational termination. In: Proceedings of PROLE’18. http://hdl.handle.net/11705/PROLE/2018/009 (2018). Accessed 9 Feb 2019

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.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)

Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP’14, pp. 111–122. ACM Digital Library (2014)

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

Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, London (1997)

Meseguer, J.: General logics. In: Logic Colloquium’87, pp. 275–329 (1989)

O’Donnell, M.J.: Equational Logic as a Programming Language. The MIT Press, Cambridge (1985)

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

Prawitz, D.: Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965. Reprinted by Dover Publications (2006)

Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.M.: One-path reachability logic. In: Proceedings of LICS 2013, pp. 358–367. IEEE Press (2013)

Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991)

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

Serbanuta, T., Rosu, G.: Computationally equivalent elimination of conditions. In: Proceedings of RTA’06, LNCS, vol. 4098, pp. 19–34. Springer, Berlin (2006)

Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67–69 (1949)

[-]

recommendations

 

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

Mostrar el registro completo del ítem