Tableaux Handbook Bernhard Beckert Equality and Other Theories Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. The knowledge from a given domain (or theory) is made use of by applying efficient methods for reasoning in that domain. The general purpose foreground reasoner calls a special purpose background reasoner to handle problems from a certain theory. Theory reasoning is indispensable for automated deduction in real world domains. Efficient equality reasoning is essential, but most specifications of real world problems use other theories as well: algebraic theories in mathematical problems and specifications of abstract data types in software verification to name a few. Following the pioneering work of M. Stickel, theory reasoning methods have been described for various calculi; e.g., resolution, path resolution, the connection method, model elimination, connection tableaux, and the matrix. In this chapter, we describe how to combine background reasoners with the ground, the free variable, and the universal formula versions of semantic tableaux. All results and methods can be adapted to other tableau versions for first-order logic: calculi with signed formulae, with different $\delta$-rules, with methods for restricting the search space such as connectedness or ordering restrictions, with lemma generation, etc. Difficulties can arise with adaptations to tableau calculi for other logics, in particular if the consequence relation is affected (e.g., non-monotonic logics and linear logic); and care has to be taken if theory links or theory connections have to be considered. One main focus of this chapter is efficient equality reasoning in semantic tableaux. Equality, however, is the only theory that is discussed in detail. There is no uniform way for handling theories, which is, after all, the reason for using a background reasoner but which makes it impossible to present good background reasoners for all possible theories. The second main focus of this chapter is therefore on the interaction between foreground and background reasoners, which plays a critical role for the efficiency of the combined system.