Guarded logics : algorithms and bisimulation
Colin Hirsch, Erich Grädel · 2002
For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems.