@INPROCEEDINGS{GeorgievaHustadtSchmidt00a,
AUTHOR = {Georgieva, L. and Hustadt, U. and Schmidt, R. A.},
YEAR = {2000},
TITLE = {Hyperresolution for Guarded Formulae},
EDITOR = {Baumgartner, P. and Zhang, H.},
BOOKTITLE = {Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000)},
SERIES = {Fachberichte Informatik},
VOLUME = {5/2000},
PUBLISHER = {Institut f{\"u}r Informatik, Universit{\"a}t Koblenz-Landau},
ADDRESS = {Koblenz, Germany},
PAGES = {101--112},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/GeorgievaHustadtSchmidt00a.html},
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.
}
}