Hyperresolution for Guarded Formulae.

. Recently we have been investigating 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 [9]. As hyperresolution is closely related to various tableaux methods the work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clause classes solvable by hyperresolution. The guarded fragment of rst-order logic was introduced in Andreka, van Benthem and Nemeti [1, 2]. It extends the modal fragment which corresponds to basic modal logic (via the relational translation) and is an important decidable class which contains many extended modal logics and description logics. Among the most notable properties of the guarded fragment in addition to decidability are Craig interpolation, bisimulation invariance, Bet...