@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@LPAR2001,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Computational space efficiency and minimal model generation
 for guarded formulae},
 BOOKTITLE     = {Proceedings of the 8th International Conference on Logic for 
 Programming, Artificial Intelligence, and Reasoning (LPAR 2001)
 [Havana, Cuba, 3-7 December 2001]},
 YEAR          = {2001},
 EDITOR        = {Nieuwenhuis, R. and Voronkov, A.},
 PAGES         = {85-99},
 PUBLISHER     = {Springer},
 PYEAR         = {2001},
 CADDRESS      = {Havana, Cuba},
 CYEAR         = {2001},
 CMONTH        = dec # {~3-7},
 SERIES        = {LNAI},
 VOLUME        = {2250},
 ISBN          = {3-540-42957-3},
 URL           = {Georgieva+Hustadt+Schmidt@LPAR2001.pdf},
 ABSTRACT      = {This paper investigates the use of hyperresolution as 
 a decision procedure and model builder for guarded formulae.
 In general hyperresolution is not a decision procedure for the entire
 guarded fragment. However we show that there are natural fragments which 
 can be decided by hyperresolution.
 In particular, we prove decidability of hyperresolution with or without
 splitting for the fragment GF1- and point out several ways of
 extending this fragment without loosing decidability.
 As hyperresolution is closely related to various tableaux methods
 the present work is also relevant for tableaux methods.
 We compare our approach to hypertableaux, and 
 mention the relationship to other clausal classes which are
 decidable by hyperresolution.}
}