Experiments with Associative-Commutative Discrimination Nets

Abstract

We recently proposed a data structure, called associative-commutative discrimination nets, that supports efficient algorithms for (manyto-one) term matching in the presence of associative-commutative functions. In this paper we discuss the integration of such discrimination nets into an actual equational theorem prover and report on corresponding experiments. The general associativecommutative matching problem is known to be N P-complete, but can be solved in polynomial time if the given terms are linear, i.e., do not contain multiple occurrences of the same variable. We therefore have implemented a two-stage matching procedure. First we check whether a match exists for the linearized versions of the given terms (where different occurrences of the same variable are replaced by different new variables). If a match for the linearized terms does exist, we then determine whether there is also a match for the original, non-linear terms (i.e., whether the proposed substitutions for different occurrences of the same variable are consistent). Our experimental results indicate that this approach works very well in theorem proving, where most matching attempts actually fail and are filtered out during the first stage, so that the second, more expensive stage of the algorithm is only needed in comparatively few cases.