FaCT and iFaCT.

Abstract

FaCT (Fast Classification of Terminologies) is a Description Logic (DL) classifier which has been implemented as a test-bed for a sound and complete tableaux satisfiability/subsumption testing algorithm. FaCT’s novelty lies in its relatively expressive logic and its highly optimised implementation of the tableaux algorithm. iFaCT is an extension of FaCT that supports reasoning with inverse roles. The resulting logic is particularly interesting as it no longer has the finite model property.