Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories

This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theoriesE₁∪E₂provided that matching algorithms are known in both theoriesE₁andE₂. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms (with linear constant restriction) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.