|
Abstract : |
Logic (DL) classier which has been implemented as a test-bed for a sound and complete tableaux satis ability/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 nite model property. Language The logics implemented in FaCT and iFaCT are both based on ALC R +, an extension of ALC to include transitive roles [Sattler, 1996]. For compactness, this logic will be called S (due to its relationship with the proposition multi-modal logic S4 (m) [Schild, 1991]). FaCT extends S with a hierarchy of roles and functional roles (attributes) to give SHF, while iFaCT adds inverse roles to give SHIF. The constructs used by the two logics are described in Figure 1, where A is an atomic concept, R and S are roles, C and D are concepts, R+ is the set of transitive role names and F is the set of functional role names (there is an additional restriction that R+ and F must be disjoint). The meaning of concepts and roles is given by an interpretation I = ( I, |
