Sciweavers

Share
RTA
2004
Springer

TORPA: Termination of Rewriting Proved Automatically

10 years 3 months ago
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.
Hans Zantema
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where RTA
Authors Hans Zantema
Comments (0)
books