- -

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

Ficheros en el ítem

Thumbnail
Nombre: LucasMeseguerGutierrez ...
Tamaño: 776.2Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: LucMesGUt_The2DDe ...
Tamaño: 1.128Mb
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.contributor.author Gutiérrez Gil, Raúl es_ES
dc.date.accessioned 2021-07-21T03:30:56Z
dc.date.available 2021-07-21T03:30:56Z
dc.date.issued 2020-10 es_ES
dc.identifier.issn 0168-7433 es_ES
dc.identifier.uri http://hdl.handle.net/10251/169635
dc.description.abstract [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 behavior of the main language features (e.g., conditions in program rules) is essential. In Part I of this work, we have introduced a 2D Dependency Pair Framework for automatically proving termination properties of Conditional Term Rewriting Systems. Our framework relies on the notion of processor as the main practical device to deal with proofs of termination properties of conditional rewrite systems. Processors are used to decompose and simplify the proofs in a divide and conquer approach. With the basic proof framework defined in Part I, here we introduce new processors to further improve the abil- ity of the 2D Dependency Pair Framework to deal with proofs of termination properties of conditional rewrite systems. We also discuss relevant implementation techniques to use such processors in practice. es_ES
dc.description.sponsorship 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 developed during a sabbatical year at the UIUC. 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 Conditional term rewriting es_ES
dc.subject Dependency pairs es_ES
dc.subject Program analysis es_ES
dc.subject Operational termination es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s10817-020-09542-3 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//SP20180225/ es_ES
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/NRL//N00173-17-1-G002/ 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.; 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1007/s10817-020-09542-3 es_ES
dc.description.upvformatpinicio 1611 es_ES
dc.description.upvformatpfin 1662 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 64 es_ES
dc.description.issue 8 es_ES
dc.relation.pasarela S\401042 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder U.S. Naval Research Laboratory es_ES
dc.contributor.funder National Science Foundation, EEUU es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Universitat Politècnica de València es_ES
dc.contributor.funder Agencia Estatal de Investigación 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 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) es_ES
dc.description.references Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998) es_ES
dc.description.references Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977) 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 4350, Springer, New York (2007) es_ES
dc.description.references Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2006) es_ES
dc.description.references Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett. 9(5), 212–215 (1979) es_ES
dc.description.references 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) es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008) es_ES
dc.description.references 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) 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., 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 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 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/ es_ES
dc.description.references Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proceedings of RTA’04, LNCS, vol. 3091, pp. 249–268 (2004) es_ES
dc.description.references 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) es_ES
dc.description.references Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979) es_ES
dc.description.references 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 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.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC’14, LNAI, vol. 8884, pp. 9–20 (2014) es_ES
dc.description.references 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) 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.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Methods Program. 85(1), 67–97 (2016) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references McCune, W.: Prover9 & Mace4. http://www.cs.unm.edu/~mccune/prover9/ (2005–2010) es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002) 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 Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Proceedings of RTA-TLCA’14, LNCS, vol. f8560, pp. 456–465 (2014) es_ES
dc.description.references Sternagel, T., Middeldorp, A.: Infeasible conditional critical pairs. In: Proceedings of IWC’15, pp. 13–18 (2014) es_ES
dc.description.references Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD Thesis, RWTH Aachen, Technical Report AIB-2007-17 (2007) es_ES
dc.description.references 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) es_ES
dc.description.references Wang, H.: Logic of many-sorted theories. J. Symb. Log. 17(2), 105–116 (1952) es_ES


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

Mostrar el registro sencillo del ítem