AC-complete Unification and its Application to Theorem Proving


The inefficiency of AC-completion is mainly due to the doubly exponential number of AC-unifiers and thereby of critical pairs generated. We present AC-complete E-unification, a new technique whose goal is to reduce the number of AC-critical pairs inferred by performing unification in a extension E of AC (e.g. ACU, Abelian groups, Boolean rings, ...) in the process of normalized completion. The idea is to represent complete sets of AC-unifiers by (smaller) sets of E-unifiers. Not only the theories E used for unification have exponentially fewer most general unifiers than AC, but one can remove from a complete set of E-unifiers those solutions which have no E-instance which is an AC-unifier.

First, we define AC-complete E-unification and describe its fundamental properties. We show how AC-complete E-unification can be done in the elementary case, and how the known combination techniques for unification algorithms can be reused for our purposes. Finally, we give some evidence of the kind of speedup that can be obtained by presenting some experiments with the CiME theorem prover.

full paper