  Over the past two decades several fragments of first-order logic have been
identified and shown to have good computational and algorithmic properties, to
a great extent as a result of appropriately describing the image of the
standard translation of modal logic to first-order logic. This applies most
notably to the guarded fragment, where quantifiers are appropriately
relativized by atoms, and the fragment defined by restricting the number of
variables to two. The aim of this talk is to review recent work concerning
these fragments and their popular extensions. When presenting the material
special attention is given to decision procedures for the finite satisfiability
problems, as many of the fragments discussed contain infinity axioms. We
highlight most effective techniques used in this context, their advantages and
limitations. We also mention a few open directions of study.
