Sciweavers

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

13

CADE
2001
Springer

favoriteEmaildiscussreport

176views Logical Reasoning» more CADE 2001»

Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems

14 years 4 months ago

Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems

Download reference.kfupm.edu.sa

We propose the notion of rewriting modules in order to provide a structural and hierarchical approach of TRS. We define then relative dependency pairs built upon these modules which allow us to perform termination proofs incrementally. Important results can be expressed in that new framework (regarding -termination for instance), and with help of extendable orderings, we give effective new incremental methods for proving termination particularly suited for automation.

Xavier Urbain

Real-time Traffic

Automated Reasoning | CADE 2001 | Hierarchical Approach | Relative Dependency Pairs |

claim paper

Related Content

» Recursive Path Orderings Can Also Be Incremental

» Termination of Fair Computations in Term Rewriting

» Termination of justfair computations in term rewriting

» On Tree Automata that Certify Termination of LeftLinear Term Rewriting Systems

» Cdiprover3 A Tool for Proving Derivational Complexities of Term Rewriting Systems

» Automated Termination Proofs for Java Programs with Cyclic Data

» A3PAT an approach for certified automated termination proofs

» Signature Extensions Preserve Termination An Alternative Proof via Dependency Pairs

» The sizechange principle and dependency pairs for termination of term rewriting

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2001
Where	CADE
Authors	Xavier Urbain

Comments (0)