Labelled deduction for the guarded fragment (Q2701985)

The tableau calculus \(\text{LC}_2-\text{TAB}\) which is sound and complete with respect to local square logic is presented, where \(\text{LC}_2\) denotes the modal logic \(\text{MLR}_2\) interpreted on the class of local squares, where \(\text{MLR}_2\) is the modal logic of binary relations. The system is a labelled deduction calculus in the spirit of those for modal \textbf{S5}. This 2-dimensional modal logic allows one to simulate different other modal logic, like \textbf{K, KT, KTB} or multi-\textbf{K}. The calculus is 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 www.NEWLINENEWLINEFor the entire collection see [Zbl 0940.00024].