Showing 1–2 of 2 results for author: Fiuk, O

On the complexity of Maslov's class $\overline{\text{K}}$

Authors: Oskar Fiuk, Emanuel Kieronski, Vincent Michielini

Abstract: Maslov's class $\overline{\text{K}}$ is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that $\overline{\text{K}}$ has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments s… ▽ More Maslov's class $\overline{\text{K}}$ is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that $\overline{\text{K}}$ has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to $\overline{\text{K}}$ and a novel application of paradoxical tournament graphs. △ Less

Submitted 18 July, 2024; originally announced July 2024.

Comments: This is an extended version of the LICS'24 paper

Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic

Authors: Oskar Fiuk, Emanuel Kieronski

Abstract: 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 qua… ▽ More 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. △ Less

Submitted 14 March, 2025; v1 submitted 4 April, 2024; originally announced April 2024.

Comments: arXiv admin note: text overlap with arXiv:2310.00994

Journal ref: Logical Methods in Computer Science, Volume 21, Issue 1 (March 17, 2025) lmcs:13351