MU-TERM
mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting. Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. Context-sensitive rewriting (CSR) is an example of such a restriction. In CSR, the replacements in some arguments of the function symbols are permanently forbidden. This paper describes mu-term, a tool which can be used to automatically prove termination of CSR. The tool implements the generation of the appropriate orderings for proving termination of CSR by means of polynomial interpretations over the rational numbers. In fact, mu-term is the first termination tool which generates term orderings based on such polynomial interpretations. These orderings can also be used, in a number of different ways, for proving termination of ordinary rewriting. Proofs of termination of CSR are also possible via existing transformations to TRSs (without any replacement restriction) which are also implemented in mu-term.
Keywords for this software
References in zbMATH (referenced in 32 articles , 1 standard article )
Showing results 1 to 20 of 32.
Sorted by year (- Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
- Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
- Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)
- Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
- Meseguer, José: Twenty years of rewriting logic (2012)
- Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador; Navarro-Marset, Rafael: Proving termination properties with mu-term (2011)
- Endrullis, Jörg; Hendriks, Dimitri: Lazy productivity via termination (2011)
- Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Context-sensitive dependency pairs (2010)
- Gutiérrez, Raúl; Lucas, Salvador: Proving termination in the context-sensitive dependency pair framework (2010)
- Iborra, José; Nishida, Naoki; Vidal, Germán: Goal-directed and relative dependency pairs for proving the termination of narrowing (2010)
- Lucas, Salvador: From matrix interpretations over the rationals to matrix interpretations over the naturals (2010)
- Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications (2010)
- Schernhammer, Felix; Gramlich, Bernhard: Characterizing and proving operational termination of deterministic conditional term rewriting systems (2010)
- Alarcón, Beatriz; Lucas, Salvador: Using context-sensitive rewriting for proving innermost termination of rewriting (2009)
- Borralleras, Cristina; Lucas, Salvador; Navarro-Marset, Rafael; Rodríguez-Carbonell, Enric; Rubio, Albert: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic (2009)
- Durán, Francisco; Lucas, Salvador; Meseguer, José: Methods for proving termination of rewriting-based programming languages by transformation (2009)
- Durán, Francisco; Lucas, Salvador; Meseguer, José; Gutiérrez, Francisco: Web services and interoperability for the Maude termination tool (2009)
- Lucas, Salvador; Meseguer, José: Operational termination of membership equational programs: the order-sorted way (2009)
- Alpuente, María; Escobar, Santiago; Iborra, José: Termination of narrowing using dependency pairs (2008)
- Durán, Francisco; Lucas, Salvador; Marché, Claude; Meseguer, José; Urbain, Xavier: Proving operational termination of membership equational programs (2008)
Further publications can be found at: http://users.dsic.upv.es/~slucas/csr/termination/muterm/#References