# Finite Model Reasoning in Expressive Fragments of First-Order Logic

## TL;DR

This paper reviews recent advances in finite model reasoning within expressive fragments of first-order logic, focusing on decision procedures for finite satisfiability and the techniques used to handle infinity axioms.

## Contribution

It provides a comprehensive overview of decision procedures and techniques for finite satisfiability in key first-order logic fragments and their extensions.

## Key findings

- Effective decision procedures for finite satisfiability
- Techniques for handling infinity axioms
- Open research directions identified

## Abstract

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.