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

TL;DR

This paper establishes that Maslov's class ar{K} is NExpTime-complete by demonstrating its exponential-sized model property, and introduces new complexity results and a decidable extension for related logical fragments.

Contribution

It proves the exponential-sized model property for ar{K} and determines its exact complexity, also proposing a new decidable extension of the uniform one-dimensional fragment.

Findings

ar{K} has the exponential-sized model property.

The satisfiability problem for ar{K} is NExpTime-complete.

New complexity results for related logical fragments.

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.