Benchmark Analysis with FaCT

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 and the other for the logic SHIQ, both of which use optimised implementations of sound and complete tableaux algorithms. FaCT's most interesting features are its expressive logic (in particular the SHIQ reasoner), its optimised tableaux implementation (which has now become the standard for DL systems), and its CORBA based client-server architecture. 1 The FaCT System The logics implemented in FaCT are both based on ALCR+ , an extension of ALC to include transitive roles [13]. For compactness, this logic has be called S (due to its relationship with the proposition multi-modal logic S4(m) [14]). SHF extends S with a hierarchy of roles and functional roles (attributes), while SHIQ adds inverse roles and fully qualified number restrictions. The SHIQ reasoner is of particular inter...

• Type: Conference
• Year: 2000
• Where: TABLEAUX
• Authors: Ian Horrocks
• Keywords: Artificial Intelligence, Inverse Roles, Logic, TABLEAUX 2000, Transitive Roles