Design and heuristics for BDD-based automated termination verification system for rule-based programs

We present the design and heuristics for TERMINATOR/R, an expert system for automatically verifying the termination of rewrite-rule-based programs by using binary decision diagrams (BDDs) for efficient representation of provability. First, we give a recursive definition of the boolean function that computes the provability based on a partial ordering >(precedence) on the set of function symbols. Then the construction of the BDDs for this function, in which a primitive expression f>g consisting of two operation symbols f and g is associated with the logical variable x_fg, is incorporated into an incremental termination verification procedure. We conduct some experiments to see how the performance of this procedure is affected by heuristic selection of variable orderings, and show that our method and heuristics are useful