On the complexity of Maslov's class $\overline{\text{K}}$
Oskar Fiuk, Emanuel Kieronski, Vincent Michielini
TL;DR
The paper determines the exact complexity of satisfiability for Maslov's class $\overline{\text{K}}$, proving an exponential-size model property and $\text{NExpTime}$-completeness via a semantic, game-theoretic approach and a novel use of paradoxical colourful tournaments. It develops satisfiability games (VER and SAT) and leverages colour-extended tournament graphs to bound model sizes, then extends these results to conjunctions ($\overline{\text{DK}}$) and to parametrised fragments with fixed numbers of universal quantifiers. The authors also present tight lower bounds, show a parametrised upper bound depending on the universal quantifier count, and apply the framework to an extended uniform one-dimensional fragment ($\forall$-UF) by reducing its satisfiability to $\overline{\text{DK}}$-satisfiability, preserving the exponential-model property. Overall, the work sharpens the complexity landscape of several decidable fragments, clarifies the boundary between elementary and non-elementary behavior, and provides practical decidability tools for related logics and description-like frameworks.
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 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.