Constrained equational reasoning
- 1 January 1989
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 382-389
- https://doi.org/10.1145/74540.74585
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: