The [[FaCT]] System

A result of IanHorrocks' research into optimising tableaux subsumption algorithms has been the development of the [[FaCT]] system. [[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 SHF (ALC augmented with transitive roles, functional roles and a role hierarchy) and the other for the logic SHIQ (SHF augmented with inverse roles and qualified number restrictions), both of which use sound and complete tableaux algorithms.

see: http://www.cs.man.ac.uk/~horrocks/FaCT/