description logic reasoner for the semantic web

 FaCT++ is a DL reasoner. It supports OWL DL as well as the forthcoming
 standard OWL 1.1. FaCT++ is implemented in C++ and uses optimised
 tableaux algorithms. The tool is probably best known for its
 compatibility with the tool Protege that helps to formally represent
 semantics.