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é . 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.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Nguyen, Linh Anh; Szałas, Andrzej: Tableaux with global caching for checking satisfiability of a knowledge base in the description logic $\mathcalSH$ (2010)