This paper addresses the following combination problem: given two equational theories E_1 and E_2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of E_1 ∪ E_2? For theories over disjoint signatures, this problem was solved by Baader and Schulz in 1995. This paper is a first step towards extending this result to the case of theories sharing constructors. Since there is a close connection between positive theories and unification problems, this also extends to the non-disjoint case the work on combining decision procedures for unification modulo equational theories.
展开▼
