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.