Finite Model Reasoning in Expressive Fragments of First-Order Logic

Lidia Tendera
(Opole University)

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.

Invited Presentation in Sujata Ghosh and R. Ramanujam: Proceedings of the Ninth Workshop on Methods for Modalities (M4M9 2017), Indian Institute of Technology, Kanpur, India, 8th to 10th January 2017, Electronic Proceedings in Theoretical Computer Science 243, pp. 43–57.
Published: 6th March 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.243.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org