Sciweavers

Share
TABLEAUX
2000
Springer

Benchmark Analysis with FaCT

10 years 3 months ago
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...
Ian Horrocks
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TABLEAUX
Authors Ian Horrocks
Comments (0)
books