Labelled Deduction for the Guarded Fragment
Maarten Marx, Stefan Schlobach, Szabolcs Mikulás

Abstract:
We present the tableau calculus LC_2-TAB which is sound and complete 
with respect to local square modal logic. The system is a labelled 
deduction calculus in the spirit of those for modal S5. The novelty 
here is that the calculus works in two interacting dimensions. This 
2-dimensional modal logic allows one to simulate different other modal 
logics, like K, KT, KTB or multi-K in quite an elegant way. The calculus 
is also strong enough to decide an interesting pspace complete 
sub-fragment of the guarded fragment, which is generally conceived of 
as the true modal fragment of first order logic. A PROLOG implementation 
of this calculus is available through the WWW.