FaCT++ is a Description Logic (DL) reasoner that implements a tableaux decision procedure for the SHOIQ DL, supporting datatypes like strings and integers. It uses various performance-enhancing optimizations, including standard techniques like absorption and model merging, as well as novel ones such as ordering heuristics and taxonomic classification. FaCT++ can be used via the DIG interface to provide reasoning services for OWL DL ontology tools. DLs are knowledge representation formalisms used as the basis for ontology languages like OWL. Efficient DL reasoners are needed due to the high worst-case complexity of the satisfiability/subsumption problem. FaCT++ is designed as a platform for experimenting with new tableaux algorithms and optimization techniques. It incorporates standard optimizations from the FaCT system and employs novel ones, including a new "ToDo list" architecture that supports complex tableaux algorithms, such as those used for OWL ontologies. FaCT++ performs tableaux reasoning by first preprocessing the knowledge base (KB) into a simplified normal form (SNF), applying optimizations like lexical normalization, absorption, and cycle elimination. It then performs classification, computing and caching the subsumption partial ordering (taxonomy) of named concepts. The system uses a KB satisfiability checker to decide subsumption problems, which is its core component and most optimized part. Optimizations include preprocessing steps like SNF translation, absorption of GCIs, and cycle elimination. Satisfiability checking optimizations include the ToDo list approach, dependency-directed backtracking, Boolean constant propagation, and semantic branching. Classification optimizations involve definitional ordering, model merging, completely defined concepts, and clustering. Future directions for FaCT++ include supporting the more expressive SROIQ DL for OWL 1.1, optimizing reasoning with nominals, and improving technological aspects like XML syntax support and parallel processing.FaCT++ is a Description Logic (DL) reasoner that implements a tableaux decision procedure for the SHOIQ DL, supporting datatypes like strings and integers. It uses various performance-enhancing optimizations, including standard techniques like absorption and model merging, as well as novel ones such as ordering heuristics and taxonomic classification. FaCT++ can be used via the DIG interface to provide reasoning services for OWL DL ontology tools. DLs are knowledge representation formalisms used as the basis for ontology languages like OWL. Efficient DL reasoners are needed due to the high worst-case complexity of the satisfiability/subsumption problem. FaCT++ is designed as a platform for experimenting with new tableaux algorithms and optimization techniques. It incorporates standard optimizations from the FaCT system and employs novel ones, including a new "ToDo list" architecture that supports complex tableaux algorithms, such as those used for OWL ontologies. FaCT++ performs tableaux reasoning by first preprocessing the knowledge base (KB) into a simplified normal form (SNF), applying optimizations like lexical normalization, absorption, and cycle elimination. It then performs classification, computing and caching the subsumption partial ordering (taxonomy) of named concepts. The system uses a KB satisfiability checker to decide subsumption problems, which is its core component and most optimized part. Optimizations include preprocessing steps like SNF translation, absorption of GCIs, and cycle elimination. Satisfiability checking optimizations include the ToDo list approach, dependency-directed backtracking, Boolean constant propagation, and semantic branching. Classification optimizations involve definitional ordering, model merging, completely defined concepts, and clustering. Future directions for FaCT++ include supporting the more expressive SROIQ DL for OWL 1.1, optimizing reasoning with nominals, and improving technological aspects like XML syntax support and parallel processing.