This paper provides a comprehensive system description of FaCT++, a Description Logic (DL) reasoner designed for efficient reasoning in expressive DLs such as SHOTQ, which is closely aligned with the OWL ontology language. FaCT++ employs a tableaux decision procedure and includes a wide range of performance-enhancing optimizations, both standard and novel. The system supports additional data types like strings and integers and can be integrated with ontology engineering tools through the DIG interface. The paper introduces the background of Description Logics and their importance in ontology languages, emphasizing the need for efficient DL reasoners due to the increasing complexity and size of ontologies. FaCT++ is designed to handle complex tableaux algorithms and offers a "ToDo list" architecture that facilitates heuristic optimizations. Key optimizations in FaCT++ include preprocessing techniques such as lexical normalization, simplification, absorption, and cycle elimination, which help in early inconsistency detection and simplifying concept expressions. Satisfiability checking optimizations like dependency-directed backtracking, Boolean constant propagation, semantic branching, and ordering heuristics further enhance performance. Classification optimizations focus on reducing the number of subsumption tests through definitional ordering, model merging, and techniques for completely defined concepts and clustering. The authors discuss future directions, including support for more expressive DLs like SHOIQ needed for OWL 1.1, optimized reasoning with nominals, and technological improvements such as direct support for OWL's XML syntax and parallelization of the reasoning process.This paper provides a comprehensive system description of FaCT++, a Description Logic (DL) reasoner designed for efficient reasoning in expressive DLs such as SHOTQ, which is closely aligned with the OWL ontology language. FaCT++ employs a tableaux decision procedure and includes a wide range of performance-enhancing optimizations, both standard and novel. The system supports additional data types like strings and integers and can be integrated with ontology engineering tools through the DIG interface. The paper introduces the background of Description Logics and their importance in ontology languages, emphasizing the need for efficient DL reasoners due to the increasing complexity and size of ontologies. FaCT++ is designed to handle complex tableaux algorithms and offers a "ToDo list" architecture that facilitates heuristic optimizations. Key optimizations in FaCT++ include preprocessing techniques such as lexical normalization, simplification, absorption, and cycle elimination, which help in early inconsistency detection and simplifying concept expressions. Satisfiability checking optimizations like dependency-directed backtracking, Boolean constant propagation, semantic branching, and ordering heuristics further enhance performance. Classification optimizations focus on reducing the number of subsumption tests through definitional ordering, model merging, and techniques for completely defined concepts and clustering. The authors discuss future directions, including support for more expressive DLs like SHOIQ needed for OWL 1.1, optimized reasoning with nominals, and technological improvements such as direct support for OWL's XML syntax and parallelization of the reasoning process.