Automating the Dependency Pair Method

Nao Hirokawa and Aart Middeldorp

Information and Computation 199(1,2), pp. 172 – 199, 2005.


Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area in the past few years. The dependency pair method of Arts and Giesl is one of the most popular such methods. However, there are several obstacles that hamper its automation. In this paper we present new ideas to overcome these obstacles. We provide ample numerical data supporting our ideas.


  PDF |    doi:10.1016/j.ic.2004.10.004


author = "Nao Hirokawa and Aart Middeldorp",
title = "Automating the Dependency Pair Method",
journal = "Information and Computation",
volume = 199,
number = "1,2",
pages = "172--199",
year = 2005
Nach oben scrollen