FaCT is a Description Logic classifier which has been implemented as a test-bed for a highly optimised tableaux satisfiability (subsumption) testing algorithm. The correspondence between modal and description logics also allows FaCT to be used as a theorem prover for the propositional modal logics K, KT, K4 and S4. Empirical tests have demonstrated the effectiveness of the optimised implementation and, in particular, of the dependency directed backtracking optimisation. © Springer-Verlag Berlin Heidelberg 1998.
CITATION STYLE
Horrocks, I. (1998). The FaCT system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1397 LNAI, pp. 307–312). Springer Verlag. https://doi.org/10.1007/3-540-69778-0_30
Mendeley helps you to discover research relevant for your work.