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:
Implementation and System
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:
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 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'
Last modified: Tue Apr 29 21:37:56 BST