Combination of Matching Algorithms

摘要: This paper addresses the problem of systematically building a matching algorithm for union two disjoint equational theories. The question is under which conditions algorithms in single theories are sufficient to obtain combination? In general, blind use combination techniques introduces unification. Two different restrictions considered order reduce this unification matching. First, we show that combining (with linear constant restriction) always solving pure fragment combined problems. Second, present complete largest class where not needed, including collapse-free regular and