FaCT++ is the tableaux-based reasoner for expressive Description Logics (DL). It covers OWL and OWL 2 (lacks support for key constraints and some datatypes) DL-based ontology languages. It can be used as a standalone DIG reasoner, or as a back-end reasoner for the OWL API-based application. Now it is used as one of the default reasoners in the Protege4 OWL editor.
FaCT++ is an open-source software and is distpibuted under LGPL license. Development of FaCT++ is supported by a SEALIFE research project.
FaCT++ is available for download both as a binary file and as source code. To build FaCT++, you will need a C++ compiler (GNU gcc v3.3 and higher have been used successfully) and GNU make.
The FaCT++ source code and precompiled binaries (for Windows, Linux, Mac OS X) can now be found at a Google Code: http://code.google.com/p/factplusplus/