TORPA: Termination of Rewriting Proved Automatically

Abstract. In this paper it is described how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method and semantic labelling can be used for automatically proving termination of an extensive class of string rewriting systems (SRSs). The tool implementing this combination of techniques is called TORPA: Termination of Rewriting Proved Automatically. All termination proofs generated by TORPA are easy to read and check, but for many of the SRSs involved finding a termination proof would be a hard job for a human. This paper contains all underlying theory, describes how the search for a termination proof is implemented, and includes many examples.

• Type: Conference
• Year: 2004
• Where: RTA
• Authors: Hans Zantema
• Keywords: Dependency Pair Method, RTA 2004, String Rewriting, Termination Proof, Theoretical Computer Science