Proving Termination of Integer Term Rewriting

Date Added: May 2009
Format: PDF

Recently, techniques and tools from term rewriting have been successfully applied to prove termination automatically for different programming languages. The advantage of rewrite techniques is that they are very powerful for algorithms on user-defined data structures, since they can automatically generate suitable well-founded orders comparing arbitrary forms of terms. But in contrast to techniques for termination of imperative programs, the drawback of rewrite techniques is that they do not support data structures like integer numbers which are pre-defined in almost all programming languages.