Maslov’s class K-bar is a fragment of First-Order Logic consisting of formulae in NNF whose variables occurring in the different atoms obey a certain pattern. It embeds many well-known fragments, such as the two-variable fragment, the Gödel fragment (∀∀∃*), some extensions of modal logic...
The satisfiability problem for K-bar (does a given formula admit a model?) was shown to be decidable by Maslov in the 60's. Yet its exact complexity has not been established so far, although we know that it is NExpTime-hard (as it captures FO2). In the talk, we complete the picture by showing the following result: every satisfiable formula in K-bar of size n admits a finite model of size at most 2^{O(n log n)}, and therefore the problem is NExpTime-complete. Our approach involves a use of satisfiability games tailored to K-bar and a novel application of paradoxical tournament graphs.

This is a joint work with Oskar Fiuk and Dr Hab Emanuel Kieroński, both from Wrocław.