FaCT++

FaCT++ is a high-performance, C++ based Description Logic reasoner designed for OWL DL ontologies.

FaCT++ serves as a next-generation inference engine for the Semantic Web, implementing highly optimized tableaux algorithms to handle SHOIQ(D) expressivity. Developed at the University of Manchester, it functions as a core plugin for the Protégé ontology editor and supports the DIG interface for cross-platform integration. By utilizing C++ instead of the original Lisp codebase, FaCT++ delivers significant memory efficiency and processing speed for complex classification tasks (subsumption and satisfiability) within large-scale knowledge bases.

https://owl.cs.manchester.ac.uk/tools/factplusplus/