Proof by Consistency
Leo Bachmair · Birkhäuser Boston eBooks · 1991
In many applications, such as algebraic data type specifications and equational programming, equations are intended to define a certain standard model, called the “initial model.” Reasoning about algebraic data types and equational programs thus requires proof methods for this initial algebra semantics. Such proof methods typically employ some induction scheme, e. g., induction on the structure of terms. We shall discuss an alternative approach—proof by consistency—that can be applied to equational theories that are presented as ground convergent rewrite systems. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.