Termination of Rewriting with and Automated Synthesis of Forbidden Patterns

We introduce a modified version of the well-known dependency pair framework that is suitable for the termination analysis of rewriting under forbidden pattern restrictions. By attaching contexts to dependency pairs that represent the calling contexts of the corresponding recursive function calls, it...

Full description

Bibliographic Details
Main Authors: Bernhard Gramlich, Felix Schernhammer
Format: Article
Language:English
Published: Open Publishing Association 2010-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1012.5562v1