Abstract

The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved by using tree automata techniques to obtain better approximations of the dependency graph. This graph determines the ordering constraints that need to be solved in order to conclude termination. We further show that by using our approximations the dependency pair method provides a decision procedure for termination of right-ground rewrite systems.

BibTeX Entry

@inproceedings{M-IJCAR01,
 author    = "Aart Middeldorp",
 title     = "Approximating Dependency Graphs using Tree Automata
              Techniques",
 booktitle = "Proceedings of the 1st International Joint Conference on
              Automated Reasoning",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 2083,
 pages     = "593--610",
 year      = 2001,
 doi       = "10.1007/3-540-45744-5\_49"
}