- -

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

Ficheros en el ítem

Thumbnail
Nombre: Lucas - Using ...
Tamaño: 727.4Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Lucas_UsingWellFo ...
Tamaño: 772.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Lucas Alba, Salvador es_ES
dc.date.accessioned 2021-07-21T03:31:22Z
dc.date.available 2021-07-21T03:31:22Z
dc.date.issued 2020-02 es_ES
dc.identifier.issn 0168-7433 es_ES
dc.identifier.uri http://hdl.handle.net/10251/169643
dc.description.abstract [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 levels by means of well- founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools. es_ES
dc.description.sponsorship Partially supported by the EU (FEDER), Projects TIN2015-69175-C4-1-R, and GV PROMETEOII/2015/013. es_ES
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation.ispartof Journal of Automated Reasoning es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Declarative languages es_ES
dc.subject Logical models es_ES
dc.subject Operational termination es_ES
dc.subject Program analysis es_ES
dc.subject Well-foundedness es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Using Well-Founded Relations for Proving Operational Termination es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s10817-019-09514-2 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//SP20180225/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/ es_ES
dc.relation.projectID 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/ 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. (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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1007/s10817-019-09514-2 es_ES
dc.description.upvformatpinicio 167 es_ES
dc.description.upvformatpfin 195 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 64 es_ES
dc.description.issue 2 es_ES
dc.relation.pasarela S\393626 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Ministerio de Economía y Competitividad es_ES
dc.contributor.funder Agencia Estatal de Investigación es_ES
dc.contributor.funder Universitat Politècnica de València es_ES
dc.description.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) es_ES
dc.description.references 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) es_ES
dc.description.references Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA’97, LNCS, vol. 1232, pp. 157–171, Springer, Berlin (1997) es_ES
dc.description.references Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000) es_ES
dc.description.references Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967) es_ES
dc.description.references Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001) es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87, LNCS, vol. 250, pp. 1–22 (1987) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993) es_ES
dc.description.references Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proceedings of RTA 2009, LNCS, vol. 5595, pp. 295–304 (2009) es_ES
dc.description.references Lalement, R.: Computation as Logic. Masson-Prentice Hall International, Paris (1993) es_ES
dc.description.references Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002) es_ES
dc.description.references 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) es_ES
dc.description.references Lucas, S.: Directions of operational termination. In: Proceedings of PROLE’18. http://hdl.handle.net/11705/PROLE/2018/009 (2018). Accessed 9 Feb 2019 es_ES
dc.description.references Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018) es_ES
dc.description.references Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018) es_ES
dc.description.references Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005) es_ES
dc.description.references Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017) es_ES
dc.description.references 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) es_ES
dc.description.references McCune, W.: Prover9 & Mace4. http://www.cs.unm.edu/~mccune/prover9/ (2005–2010). Accessed 9 Feb 2019 es_ES
dc.description.references Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, London (1997) es_ES
dc.description.references Meseguer, J.: General logics. In: Logic Colloquium’87, pp. 275–329 (1989) es_ES
dc.description.references O’Donnell, M.J.: Equational Logic as a Programming Language. The MIT Press, Cambridge (1985) es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002) es_ES
dc.description.references Prawitz, D.: Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965. Reprinted by Dover Publications (2006) es_ES
dc.description.references Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.M.: One-path reachability logic. In: Proceedings of LICS 2013, pp. 358–367. IEEE Press (2013) es_ES
dc.description.references Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991) es_ES
dc.description.references Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659–688 (2010) es_ES
dc.description.references Serbanuta, T., Rosu, G.: Computationally equivalent elimination of conditions. In: Proceedings of RTA’06, LNCS, vol. 4098, pp. 19–34. Springer, Berlin (2006) es_ES
dc.description.references 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) es_ES


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

Mostrar el registro sencillo del ítem