@INPROCEEDINGS{GeorgievaHustadtSchmidt01,
AUTHOR = {Georgieva, L. and Hustadt, U. and Schmidt, R. A.},
YEAR = {2001},
TITLE = {Computational Space Efficiency and Minimal Model Generation for Guarded Formulae},
EDITOR = {???},
BOOKTITLE = {Proceedings of LPAR'01},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {????},
PUBLISHER = {Springer},
PAGES = {???--???},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/GeorgievaHustadtSchmidt01.html},
ABSTRACT = {This paper describes a number of hyperresolution-based decision
procedures for a subfragment of the guarded fragment. We first present
a polynomial space decision procedure of optimal worst-case space and
time complexity for the fragment under consideration. We then
consider minimal model generation procedures which construct all and
only minimal Herbrand models for guarded formulae. These procedures are
based on hyperresolution, (complement) splitting and either model
constraint propagation or local minimality tests. All the procedures
have concrete application domains and 
are relevant for multi-modal and description logics that can be
embedded into the considered fragment.  
}
}