Wies, ThomasPiskac, RuzicaKuncak, Viktor2009-05-092009-05-092009-05-092009https://infoscience.epfl.ch/handle/20.500.14299/38842We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas obtained by applying propositional operations to quantified formulas belonging to several expressive decidable logics.text::report