Complexity of Maslov's Class K-bar

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 1971. 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 solve the problem by presenting a new result: every satisfiable formula in K-bar of size n admits a finite model of size at most 2^{O(n log n)}, and hence 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, from Wrocław. [*] the formula phi, written in NNF, is in K-bar if there exists a sequence ∀x1, ...., ∀xk of universally quantified variables, not in the scope of any existential variable, such that, for every atom of phi, the sequence of its variable either i) admits a unique variable, ii) ends with an existential variable, or iii) is exactly the sequence ∀x1, ...., ∀xk. Yes, this is complicated. Don't worry, I'll give nice examples.