- -

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

Ficheros en el ítem

Thumbnail
Nombre: AISC2014-ModelsFo ...
Tamaño: 441.6Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Lucas;José Meseguer ...
Tamaño: 296.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Lucas Alba, Salvador es_ES
dc.contributor.author Meseguer, José es_ES
dc.date.accessioned 2015-05-20T16:02:03Z
dc.date.available 2015-05-20T16:02:03Z
dc.date.issued 2014
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/50582
dc.description The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-13770-4_3 es_ES
dc.description.abstract 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 constraints which are often obtained. The formal treatment of such constraints in automated proofs, often using numeric interpretations and (arithmetic) constraint solving can greatly benefit from appropriate techniques to deal with the conditional (in)equations at stake. Existing results from linear algebra or real algebraic geometry are useful to deal with them but have received only scant attention to date. We investigate the definition and use of numeric models for logics and the resolution of linear and algebraic conditional constraints as unifying techniques for proving termination of declarative programs. es_ES
dc.description.sponsorship 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. es_ES
dc.language Inglés es_ES
dc.publisher Springer Verlag (Germany) es_ES
dc.relation.ispartof Artificial Intelligence and Symbolic Computation es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;8884
dc.rights Reserva de todos los derechos es_ES
dc.subject Termination es_ES
dc.subject Conditional constraints es_ES
dc.subject Program Analysis es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Models for logics and conditional constraints in automated proofs of termination es_ES
dc.type Capítulo de libro es_ES
dc.identifier.doi 10.1007/978-3-319-13770-4_3
dc.relation.projectID 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/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//BEST%2F2014%2F026/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/ 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 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion http://dx.doi.org/10.1007/978-3-319-13770-4_3 es_ES
dc.description.upvformatpinicio 9 es_ES
dc.description.upvformatpfin 20 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.senia 279090
dc.contributor.funder National Science Foundation, EEUU es_ES
dc.contributor.funder Ministerio de Economía y Competitividad es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Ministerio de Ciencia e Innovación es_ES
dc.description.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) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix Interpretations for Proving Termination of Term Rewriting. J. of Aut. Reas. 40(2-3), 195–220 (2008) es_ES
dc.description.references 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) es_ES
dc.description.references Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific (1998) es_ES
dc.description.references 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) es_ES
dc.description.references Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998) es_ES
dc.description.references Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications 39(3), 547–586 (2005) es_ES
dc.description.references Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Information Processing Letters 95, 446–453 (2005) es_ES
dc.description.references 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) es_ES
dc.description.references Lucas, S., Meseguer, J.: 2D Dependency Pairs for Proving Operational Termination of CTRSs. In: Proc. of WRLA 2014. LNCS, vol. 8663 (to appear, 2014) es_ES
dc.description.references Lucas, S., Meseguer, J., Gutiérrez, R.: Extending the 2D DP Framework for CTRSs. In: Selected papers of LOPSTR 2014. LNCS (to appear, 2015) es_ES
dc.description.references Meseguer, J.: General Logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium 1987, pp. 275–329. North-Holland (1989) es_ES
dc.description.references 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) es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (April 2002) es_ES
dc.description.references Prestel, A., Delzell, C.N.: Positive Polynomials. In: From Hilbert’s 17th Problem to Real Algebra. Springer, Berlin (2001) es_ES
dc.description.references 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) es_ES
dc.description.references Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons (1986) es_ES
dc.description.references Zantema, H.: Termination of Context-Sensitive Rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997) es_ES


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

Mostrar el registro sencillo del ítem