LP, the Larch Prover -- Normalization

A term is said to be normalized, or in normal form, with respect to a set of rewrite rules if none of those rules can be applied to the term. The command show normal-form displays the normal form of a term with respect to the active rewrite rules in LP's logical system. See also the normalize command.

If the rewriting system is not guaranteed to terminate (e.g., if the user oriented an equation into a rewrite rule manually), the normal form computation may not terminate. When the rewriting system is not known to terminate, LP stops the rewriting process and issues a warning after a very large number of rewrites during a normal form computation. See the rewriting-limit setting.

If the rewriting system is not confluent, a term may have more than one normal form.

LP uses normalization as a method of forward and backward inference.