Constrained equational reasoning

摘要

We describe and give the foundation for constrained equational reasoning. Equational reasoning is based on replacement of equal by equal and these replacements use substitutions determined as solutions of equations. Constrained equational reasoning takes advantage from the information contained into the equation itself to develop equational reasoning, avoids instantiations as much as possible and solve constraints as late as possible. For theories like associativity-commutativity this can lead to a considerable reduction of the substitution computation overhead, bringing some problems, untractable in practice, to the realm of computational reality.