- -

Models for logics and conditional constraints in automated proofs of termination

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Models for logics and conditional constraints in automated proofs of termination

Mostrar el registro completo del ítem

Lucas Alba, S.; Meseguer, J. (2014). Models for logics and conditional constraints in automated proofs of termination. En Artificial Intelligence and Symbolic Computation. Springer Verlag (Germany). 9-20. https://doi.org/10.1007/978-3-319-13770-4_3

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

Ficheros en el ítem

Thumbnail
Nombre: AISC2014-ModelsFo ...
Tamaño: 441.6Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Lucas;José Meseguer ...
Tamaño: 296.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Models for logics and conditional constraints in automated proofs of termination
Autor: Lucas Alba, Salvador Meseguer, José
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:
Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional ...[+]
Palabras clave: Termination , Conditional constraints , Program Analysis
Derechos de uso: Reserva de todos los derechos
Fuente:
Artificial Intelligence and Symbolic Computation. (issn: 0302-9743 )
DOI: 10.1007/978-3-319-13770-4_3
Editorial:
Springer Verlag (Germany)
Versión del editor: http://dx.doi.org/10.1007/978-3-319-13770-4_3
Serie: Lecture Notes in Computer Science;8884
Código del Proyecto:
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/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/
info:eu-repo/grantAgreement/GVA//BEST%2F2014%2F026/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
Descripción: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-13770-4_3
Agradecimientos:
Developed during a sabbatical year at UIUC. Supported by projects NSF CNS13-19109, MINECO TIN2010-21062-C02-02 and TIN2013-45732-C4-1-P, and GV BEST/2014/026 and PROMETEO/2011/052.
Tipo: Capítulo de libro

References

Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving Termination Properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011)

Alarcón, B., Lucas, S., Navarro-Marset, R.: Using Matrix Interpretations over the Reals in Proofs of Termination. In: Proc. of PROLE 2009, pp. 255–264 (2009)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) [+]
Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving Termination Properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011)

Alarcón, B., Lucas, S., Navarro-Marset, R.: Using Matrix Interpretations over the Reals in Proofs of Termination. In: Proc. of PROLE 2009, pp. 255–264 (2009)

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

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

Endrullis, J., Waldmann, J., Zantema, H.: Matrix Interpretations for Proving Termination of Term Rewriting. J. of Aut. Reas. 40(2-3), 195–220 (2008)

Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal Termination. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 110–125. Springer, Heidelberg (2008)

Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific (1998)

Hudak, P., Peyton-Jones, S.J., Wadler, P.: Report on the Functional Programming Language Haskell: a non–strict, purely functional language. Sigplan Notices 27(5), 1–164 (1992)

Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998)

Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications 39(3), 547–586 (2005)

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

Lucas, S., Meseguer, J.: Proving Operational Termination of Declarative Programs in General Logics. In: Proc. of PPDP 2014, pp. 111–122. ACM Digital Library (2014)

Lucas, S., Meseguer, J.: 2D Dependency Pairs for Proving Operational Termination of CTRSs. In: Proc. of WRLA 2014. LNCS, vol. 8663 (to appear, 2014)

Lucas, S., Meseguer, J., Gutiérrez, R.: Extending the 2D DP Framework for CTRSs. In: Selected papers of LOPSTR 2014. LNCS (to appear, 2015)

Meseguer, J.: General Logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium 1987, pp. 275–329. North-Holland (1989)

Nguyen, M.T., de Schreye, D., Giesl, J., Schneider-Kamp, P.: Polytool: Polynomial interpretations as a basis for termination of logic programs. Theory and Practice of Logic Programming 11(1), 33–63 (2011)

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

Prestel, A., Delzell, C.N.: Positive Polynomials. In: From Hilbert’s 17th Problem to Real Algebra. Springer, Berlin (2001)

Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)

Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons (1986)

Zantema, H.: Termination of Context-Sensitive Rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997)

[-]

recommendations

 

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

Mostrar el registro completo del ítem