A technique for automatically proving termination of constructor systems
Thjj Thomas Arts · 1995
A technique is described to prove termination of constructor systems (CSs) automatically. The technique consists of three major steps. First, determine the dependency pairs of a constructor system. Second, find an equational theory in which the constructor system is contained, and third, prove that no infinite chain w.r.t. the equational theory of these dependency pairs exists. The first step is easy and can be performed completely automatically. Here we first concentrate on the last step. We assume the equational theory given in the form of a complete TRS and present several general criteria on the syntax of the dependency pairs to prove that no infinite chain can exist with respect to the given equational theory. For these criteria no semantic unification is needed and they can be performed completely automatically. Second we demonstrate a technique to find a complete TRS automatically in case the CS that has to be proved terminating is of a special form. We combine all techniques to...