|
Abstract : |
Abstract. This paper addresses the following combination problem: given two equational theories E and E2 whose positive theories are decidable, how can one obtoJn a decision procedure for the positive theory of E U E27 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., |
