Journal of Logic and Computation, Volume 10, Issue 1, pp. 105135: Abstract.
Tractable and intractable instances of combination problems for unification and disunificationKU Schulz Oettingenstr. 67, 80538 München, Germany, Email: schulz@cis.unimuenchen.de
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 polynomialtime combination procedure is (im)possible. In the first part of this paper we characterize a large class of equational theories E where Eunification with free function symbols is NPhard and where a polynomialtime optimization of the combination algorithm is impossible (unless P = NP). This supports the conjecture that for the theories in this class there is no polynomialtime algorithm for combining Eunification with constants with free unification. In the second part of the paper we introduce another class of equational theories where (dis)unification algorithms can be combined deterministically and in polynomial time. Under reasonable assumptions on the form of the given unification procedure, each unitary, regular and collapsefree equational theory with a polynomialtime unification algorithm belongs to this class. Keywords: Combination problems, equational unification, equational disunification, NPhardness, polynomial combination algorithms, deterministic combination algorithms
