Sound Over-Approximation of Equational Reasoning with Variable-Preserving Rules Parameterized by Derivation Depth
Equational reasoning is one of the most intuitive and widely used types of symbolic reasoning. In this setting, the goal is to determine whether a given ground equation t=t' follows as a consequence of a set of equational axioms E using the process of replacing equals with equals. An equation t=t' i…