• MU-TERM: A tool for proving te...

Result: MU-TERM: A tool for proving termination of context-sensitive rewriting

Title:
MU-TERM: A tool for proving termination of context-sensitive rewriting
Authors:
LUCAS, Salvador
Source:
RTA 2004 : rewriting techniques and applications (Aachen, 3-5 June 2004)Lecture notes in computer science. :200-209
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 16 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Problème terminaison, Termination problem, Problema terminación, Relation ordre, Ordering, Relación orden, Remplacement, Replacement, Reemplazo, Réécriture, Rewriting, Reescritura, Sensibilité contexte, Context aware, Sensibilidad contexto
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
DSIC, Universidad Politécnica de Valencia, Camino de Vera s/n, 46022 Valencia, Spain
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=15851911
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15851911
Database:
PASCAL Archive

Further Information

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.