Associative-commutative matching via bipartite graph matching

We consider the problem of term matching where some subset of the function symbols are associative-commutative. Our approach is to build a hierarchy of bipartite graph matching problems which encodes all the possible solutions of subproblems. Sets of solutions to the graph matching problems which are consistent on variable assignments give rise to what we refer to as semi-pure AC systems in which assignments for every variable occurring under a free function symbol in the pattern are known. These semi-pure AC systems are then solved by an exhaustive search to find complete matching substitutions. We give a number of refinements which considerably cut down the search space at all stages in the algorithm leading to efficient solution of non-pathological problem instances.