FaCT (Fast Classification of Terminologies) is a Description Logic (DL) classifier that can also be used for modal logic satisfiability testing. The FaCT system includes two reasoners, one for the logic \(\mathcal{SHF}\) and the other for the logic \(\mathcal{SHIQ}\), both of which use optimised implementations of sound and complete tableaux algorithms. FaCT’s most interesting features are its expressive logic (in particular the \(\mathcal{SHIQ}\) reasoner), its optimised tableaux implementation (which has now become the standard for DL systems), and its CORBA based client-server architecture.