Affiliations: Institute of Informatics, University of Warsaw, Banacha
2, 02-097 Warsaw, Poland. [email protected]
Note: [] Address for correspondence: L.A. Nguyen, Institute of
Informatics, University ofWarsaw, Banacha 2, 02-097 Warsaw, Poland
Abstract: We report on our implementation of a tableau prover for the
description logic ALC, which is based on the EXPTIME tableau algorithm using
global caching for ALC that was developed jointly by us and Goré [9]. The
prover, called TGC for "Tableaux with Global Caching",
checks satisfiability of a set of concepts w.r.t. a set of global assumptions
by constructing an and-or graph, using tableau rules for expanding nodes. We
have implemented for TGC a special set of optimizations which co-operates very
well with global caching and various search strategies. The test results on the
test set T98-sat of DL'98 Systems Comparison indicate that TGC is
an efficient prover for ALC. This suggests that global caching together with
the set of optimizations used for TGC is worth implementing and experimenting
also for other modal/description logics.
Keywords: automated reasoning, tableaux, description logic, global caching, optimizations
