Maslov's class K with Equivalence

Maslov's class K is a decidable fragment of equality-free first-order logic. It subsumes numerous classical decidable fragments, including the equality-free monadic fragment, the equality-free two-variable fragment, and the Gödel class. Introduced over 50 years ago, the class K has been studied in automated deduction, primarily through resolution-based methods. Despite this long history, the precise complexity of the satisfiability problem for K remained open until recently, when NExpTime-completeness was finally established. The two main contributions of this work are as follows. 1. The recent proofs of NExpTime-completeness and the finite model property for K are highly non-trivial and technically sophisticated. We present considerably simpler proofs of both results. Our approach combines a novel reduction from K to the class of solvable Skolem sentences with a randomised construction of finite models. 2. We introduce the class K+E by allowing sentences in K to contain one distinguished binary predicate E whose interpretation is constrained to be an equivalence relation. By leveraging our approach to this extended class, we prove that K+E has the finite model property and that its satisfiability problem is 2-NExpTime-complete.