Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems

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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Xavier Urbain
• Keywords: Automated Reasoning, CADE 2001, Hierarchical Approach, Relative Dependency Pairs