Implementation and Evaluation of a Tableau Algorithm for the Guarded Fragment.
Jan Hladík · 2002
In this paper we present Saga, an implementation of a tableau-based Satisfiability Algorithm for the Guarded Fragment (GF ). Satisfiability for GF with finite signature is ExpTime-complete and therefore intractable in the worst case, but existing tableau-based systems for ExpTime-complete description and modal logics perform reasonably well for "realistic" knowledge bases. We implemented and evaluated several optimizations used in description logic systems, and our results show that, with an efficient combination, Saga can compete with existing highly optimized systems for description logics.