@INPROCEEDINGS{GHS01a,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Computational space efficiency and minimal model 
 generation for guarded formulae},
 BOOKTITLE     = {International Joint Conference on Automated Reasoning IJCAR 2001: Short Papers},
 EDITOR        = {Gore{\'e}, R. and Leitsch, A. and Nipkow, T.},
 PAGES         = {34--43},
 PUBLISHER     = {Departimento di Ingegneria dell'Informazione, Universit{\'a} degli Studi di Siena},
 PADDRESS      = {Siena, Italy},
 PYEAR         = {2001},
 CADDRESS      = {Siena, Italy},
 CYEAR         = {2001},
 CMONTH        = jun # {~19--23},
 SERIES        = {Technical Report},
 VOLUME        = {DII 11/01},
 XNOTE         = {Appeared as Technical Report DII 11/01, Departimento di Ingegneria dell'Informazione, Universit{\'a} degli Studi di Siena, Italy},
 ABSTRACT      = {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.}
}