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 SHOIQ. Achieving 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++. © 2007 Springer Science+Business Media B.V.
- Description logic
- Reasoning systems