We present the SAT-Tableau Calculus, a novel calculus for Description Logic (DL) reasoning. It achieves the integration of a plethora of known SAT solvers into tableau-based DL reasoning. Our calculus can be understood as a SAT-Modulo-Theories approach that is based on a specific theory-reasoning component. The theory reasoner maintains a finite representation of a (possibly infinite) Kripke-structure and guides the generation of this structure by systematic interaction with a SAT solver. The approach essentially improves on previous work on using specific SAT solvers for DL reasoning in various significant ways. Most importantly, we extend the type of SAT solvers that can be used during the DL reasoning process, the expressiveness of DLs that can be handled, the reasoning tasks that can be supported by the approach and the way heuristic search can be performed in implementations. We consider the SAT-Tableau Calculus as a first step towards a new understanding of tableau-based methods for DLs, as a tool for comparing different known inference systems for DL reasoning, and, finally, as the basis for novel tableau-based inference procedures for DLs that may outperform existing systems on specific problem sets.