Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

RTA

2004

Springer

2004

Springer

Restrictions of rewriting can eventually achieve termination by pruning all inﬁnite rewrite sequences issued from every term. Contextsensitive 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 ﬁrst termination tool which generates term orderings based on such polynomial interpretations. These orderings can also be used, in a number of diﬀerent 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.

Related Content

Added |
02 Jul 2010 |

Updated |
02 Jul 2010 |

Type |
Conference |

Year |
2004 |

Where |
RTA |

Authors |
Salvador Lucas |

Comments (0)