LP, the Larch Prover -- Termination

A set of rewrite rules is called terminating if each term can be reduced only a finite number of times. Generally some well-founded ordering on terms is used to establish the termination of a rewriting system.