Update: Nov 22, 2011

WFLP 2011 Paper

On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs

Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe
In Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2011),
Vol. 6816 of Lecture Notes in Computer Science, pp. 138-155, July 2011.
In this paper, we propose methods for proving termination of constrained term rewriting systems, where constraints are interpreted by built-in semantics given by users, and rewrite rules are assumed to be sound for the interpretation. To this end, we extend the dependency pair framework for proving termination of unconstrained term rewriting systems to constrained term rewriting systems. Moreover, we extend the dependency pair framework so that dependency pair processors take a subgraph of the dependency graph as input and they output a finite set of graphs which can be obtained by eliminating nodes and/or edges from the input graph.
[LNCS] [full version (pdf)]

Sakai Lab. Graduate School of Informatics Dept. of Information Engineering Graduate School/School of Engineering Nagoya University
Produced by N.Nishida (nishida @ i.nagoya-u.ac.jp)