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.
The authors thank Peter Baumgartner for drawing our attention to Niemelä’s work and raising the question of the computational
complexity of minimal model generation. The work of the first and third authors is supported by EPSRC Research Grant GR/M36700.