Temporalising tableaux (Q1826368)

The monodic fragments of first-order temporal logic (FOTL) are obtained by restricting the application of temporal operators to formulas with at most one free variable. This paper is concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of FOTL like the two-variable fragment or the guarded fragment. A general framework is presented that shows how existing decision procedures for first-order fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented.