Tableau algorithms are currently the most widely used and empirically the fastest algorithms for reasoning in expressive description logics, including the important description logics SHIQ\mathcal{SHIQ} and SHOIQ\mathcal{SHOIQ}. Achieving a high level of performance on terminological reasoning in expressive description logics when using tableau-based algorithms requires the incorporation of a wide variety of optimizations. The description logic system FaCT++ implements a wide variety of such optimizations, some present in other reasoners and some novel or refined in FaCT++.