An Effcient Tableau Prover using Global Caching for the Description Logic ALC. 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é [10]. 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 effcient 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.