Tools for proving inductive equalities, relative completeness, and ω-completeness

AbstractInductive theorems are properties valid in the initial algebra. A now popular tool for proving them in equational theories or abstract data types is based on proof by consistency. This method uses a completion procedure and requires two essential properties of the specification, namely relative completeness and ω-completeness. This paper investigates ways of proving them. For the first one, the complement algorithm is presented. It is based on unification and computation of coverings and complements. For the second one, a technique based on discrimination of pairs of normal forms is explained and illustrated through examples