Optimizing terminological reasoning for expressive description logics

Tableau algorithms are currently the most widely used and empirically the fastest algorithms for reasoning in expressive description logics, including the important description logics SHIQ and SHOIQAchieving a high level of performance on terminological reasoning in expressive description logics when using tableau-based algorithms requires the incorporation of a wide variety of optimizations. The description logic system FaCT++ implements a wide variety of such optimizations, some present in other reasoners and some novel or refined in FaCT++.