Proving Termination of Context-Sensitive Rewriting with MU-TERM | Zendy

Beatriz Alarcón | Zendy; Raúl Gutiérrez | Zendy; J.L. Iborra | Zendy; Salvador Lucas | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Proving Termination of Context-Sensitive Rewriting with MU-TERM

Author(s) -

Beatriz Alarcón,

Raúl Gutiérrez,

J.L. Iborra,

Salvador Lucas

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2007.05.041

Subject(s) - rewriting , term (time) , mathematical proof , programming language , computer science , context (archaeology) , confluence , mathematics , physics , quantum mechanics , biology , paleontology , geometry

Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. Proving termination of CSR is an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. The new version of MU-TERM which we present here implements all currently known techniques. Furthermore, we show how to combine them to furnish MU-TERM with an expert which is able to automatically perform the termination proofs. Finally, we provide a first experimental evaluation of the tool

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research