Oskar Fiuk ; Emanuel Kieronski - Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic

lmcs:13351 - Logical Methods in Computer Science, March 17, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:25)2025
Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable LogicArticle

Authors: Oskar Fiuk ; Emanuel Kieronski

    The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime-complete satisfiability.


    Volume: Volume 21, Issue 1
    Published on: March 17, 2025
    Accepted on: February 10, 2025
    Submitted on: April 5, 2024
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 430 times.
    This article's PDF has been downloaded 168 times.