AC-complete unification and its application to theorem proving

Abstract: 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 [1, 2]. The idea is to represent complete sets of AC-unifiers by (smaller) sets of E-unifiers. Not only do 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.

References

[1]

C. Marché. Normalised rewriting and normalised completion. pages 394–403, 1994.

[2]

C. Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, 1996.

This document was translated from L^AT_EX by H^EV^EA.