Tractable and Intractable Instances of Combination Problems for Unification And Disunification

摘要

The algorithms for combining decision procedures for (dis) unification in the union of arbitrary disjoint equational theories known from the literature generate an exponential number of 'pure' output problems over the component theories. Despite several optimization techniques, no general results are known that describe in which cases a polynomial-time combination procedure is (im) possible.