Finitary Matching For Constructor Based Theories

Acyclic Constructor Based (ACB) theories are induced by a restricted class of equations, which can be treated as convergent rewrite systems. We claim that solving matching problems with such theories presents an interesting subclass of matching-modulo-E problems. In this paper we present a constructive matching algorithm for ACB theories, and show its termination and completeness. The comparison to the second-order matching and the rewriting modulo commutativity sheds some light on the power of ACB-matching. The easy combination of ACB matching problems is also an advantage of our approach. 1 Introduction "Extended unification" (see [3]) has been investigated for many theories. Well known positive results for associativity, commutativity [21], for boolean rings [14], or for convergent rewrite systems [10, 4] demonstrate the importance of extended unification in many application fields, like theorem proving, logic programming, etc. The congruence relations induced by equational theori..