The FaCT System

A result of my research into optimising tableaux subsumption algorithms has been the development of the FaCT system. 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 (ALC augmented with transitive roles, functional roles and a role hierarchy) and the other for the logic SHIQ (SHF augmented with inverse roles and qualified number restrictions), both of which use sound and complete tableaux algorithms.

FaCT's most interesting features are:

its expressive logic (in particular the SHIQ reasoner): SHIQ is sufficiently expressive to be used as a reasoner for the DLR logic, and hence to reason with database schemata;
its support for reasoning with arbitrary knowledge bases (i.e., those containing general concept inclusion axioms);
its optimised tableaux implementation (which has now become the standard for DL systems), and
its CORBA based client-server architecture.

Implementation and System Requirements:

FaCT is written in Common Lisp, and has been run successfully with several commercial and free lisps, including Allegro, Liquid (formerly Lucid), Lispworks and GNU. As the source code is available (under the GNU general public license), FaCT can be run on any system where a suitable Lisp is available. Binaries (executable code) are also available (in addition to the source code) for Linux and Windows systems, allowing FaCT to used without a locally available Lisp. Moreover, a FaCT server running on a suitable host machine can be used (via its CORBA interface) on any system that has network access to the server.

Availability and Usage:

The CORBA-FaCT system, a CORBA based client-server architecture for FaCT, is available for downloading. This uses a JAVA component to provide the ORB interface (we are working on a more efficient and robust native Lisp ORB version, and this should be available soon). Java version 1.2 is required for the ORB interface, but (386-Linux and Windows/NT) binaries are provided for the reasoners, so Lisp is not required.

A new FaCT DIG servlet is also available. As well as providing a lighter-weight HTTP interface, this has the advantage that, for Java applications, a direct in-memory connection (side-stepping the HTTP communication) can be used.

For Lisp hackers, the Lisp version of the FaCT system (including source code, installation instructions and documentation) is also available for downloading. The latest release includes both the SHF and SHIQ reasoners as well as a selection of interfaces, one of which will accept DLR directly.

Further Information:

Further information about FaCT, including several papers describing the algorithms and optimisation techniques used in the system, can be found via the Camelot Project home page or by contacting Ian Horrocks.

Back to Ian Horrocks' home page.

Ian Horrocks

Last modified: Tue Apr 29 21:37:56 BST 2003