L. Georgieva U. Hustadt, R. A. Schmidt (2001): ``Computational space efficiency and minimal model generation for guarded formulae'' In R. Gore, A. Leitsch, and T. Nipkow, IJCAR 2001: Short Papers, pp. 34-43.
Abstract, BibTeX, PDF.

This paper addresses two issues. First, it presents an efficient hyperresolution-based decision procedure for subfragments of the guareded fragment which requires polynomial space and secondly it describes a minimal model generation procedure which constructs all and only minimal Herbrand models for guarded formulae. Both procedures have concrete application domains, i.e. they are relevant for many multi-modal and descriptions logics that can be embedded into the guarded fragment. The space optimal decision procedure effectively corresponds to tableaux-based polynomial space algorithms for testing the concept satisfiability of description logics. It is motivated by the trace technique, however it does not use blocking. The minimal Herbrand model generation procedure is based on hyperresolution and complement splitting. We study the properties of the procedure and show that is sound and complete.