Maslov's class K is an expressive fragment of First-Order Logic that embeds modal logic and many description logics, including ℒ . It is known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that 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 K and a novel application of paradoxical tournament graphs.
Basic modal logic and many standard description logics (DLs), including ℒ , embed into First-Order Logic, FO, via the so-called standard translation. In contrast to robust decidability of satisfiability of DLs, the satisfiability problem for full FO is undecidable. Therefore, a considerable efort has been made to identify fragments of FO which still embed standard DLs, but have decidable satisfiability. Studying such fragments may help us to understand good computational and model-theoretic properties of DLs, and find their attractive extensions, e.g., admitting relations of arity greater than two.
The list of known decidable fragments that appeared in this line of research includes the
two-variable fragment, FO2 [1, 2], the guarded fragment, GF [3, 4], the unary negation fragment,
UNFO [5], the guarded negation fragment, GNFO [
In contrast to all the other fragments mentioned above, satisfiability of K is not yet fully understood. Maslov proved the decidability of the validity problem for K, which is equivalent to the satisfiability problem for K, using his own approach, which he called the inverse method. There were a few subsequent works [16, 17, 18], whose authors reproved this result by means of the resolution method; all of them work directly with K. None of these works, however, studied the complexity of its satisfiability. While a closer inspection of the resolution-based procedure in [17] seems to allow one to extract some elementary upper bound on the complexity of the satisfiability problem for K, it would not be easy to get anything better than doubly exponential. This would still leave a gap, as the best lower bound inherited from the fragments embeddable in K is NExpTime-hardness.
In our paper we add the main missing brick to the understanding of K by showing that its satisfiability problem is NExpTime-complete. We will do it by showing:
Theorem 1. Every satisfiable formula in K admits a finite model of size 2 (| |·log | |). Hence, the satisfiability problem for
K is NExpTime-complete.
We consider signatures with relational symbols of arbitrary arity and constants, but no function symbols of arity greater than 0. Equalities are not allowed as they lead to undecidability [20]. Let be a sentence in negation normal form, and let (¯) be one of its atoms. The -prefix of (¯) is the sequence of quantifiers in binding the variables of (¯). For instance, if is the sentence ∃. the atom (, ∀ . ∃.
(, ) ∧ (, , , ) is the sequence “ .
), with being a constant symbol, then the -prefix of ∃ ∀ ”, while that of the atom (, , , ) is “ . ∃ ”. An ∀ atom without variables (e.g. stating only about constants) has the empty -prefix.
The class K consists of the sentences
which are in negation normal form and in which there exist universally quantified variables 1, . . . , , called special variables, none of which lying within the scope of any existential quantifier, such that each atom of has a -prefix of one of the following shapes: (i) a -prefix of length at most 1, (ii) a -prefix ending with an existential quantifier, (iii) or exactly the sequence “ ∀ 1 . . . ∀ ”.
While we require the formula to be in negation normal form, we allow ourselves to use implications, provided that their left-hand sides do not contain any quantifiers.
convention, the following formula co_authors is in K: ∀ 1, 2, 3.︀[ scientist( 1) ∧ scientist( 2) ∧ scientist( 3) ∧ co_authors( 1, 2, 3)︀]
→ ∃. article( ) ∧ written_by(, 1, 2, 3).
Indeed, the co_authors-prefixes of the diferent atoms are: the singleton sequences “ the conditions are met, with 1, 2, 3 being the special variables. “∀ 3” and “∃ ”; the sequence “∀ 1. ∀ 2. ∀ 3. ∃ ”, which ends with an existential quantifier; and the universal sequence “∀ 1. ∀ 2. ∀ 3”. There is no existential quantifier binding the , so all ∀ 1”, “∀ 2”, Another example marriage demonstrates the possibility of using quantifier alternation: ∀ℎ,.
husband_and_wife(ℎ, ) → ∃. problem( ) ∧ ∀. date( ) → ∃ ′. date( ′) ∧ later_than( ′, ) ∧ occurs_to_at(, ℎ, , ′).
On the contrary, an example of a property not expressible in K is transitivity. In particular, in the formula ∀, , . could work as the set of special variables.
︀[ (, ) ∧ (, )
︀] → (, ), one cannot find a subset of variables that
Turning to relation between K and DLs, we need to remark, that actually the standard ︀⋀ ∀. ∃
. indeed get sentences in K. translation of,instaoy,Fℒ O2, and then write the FO2 formula in its Scott normal form: ∀, . into FO does not land directly in K. To embed ℒ translate ℒ in K, we first 0(, ) ∧ (,
). One can verify that after renaming the variables in the ∀∃-conjuncts we Additional DL features that translate to K this way include Boolean combinations of roles, inversions, role restrictions and positive occurrences of role compositions [13].
In addition to DLs, the class K embeds, either syntactically or via simple reductions preserving satisfiability, many known decidable fragments of First-Order Logic, including the monadic class [21], the Ackermann fragment [22] and its generalised version [23], the Gödel class [24], the two-variable fragment [1] and Class 2.4 from [25] (which we will call K-Skolem class). Even more formalisms, for example the uniform one-dimensional fragment [10] or its variation with alternation of quantifiers in blocks [ 26], are captured by the class DK of conjunctions of
remaining results are as follows: Our main result is Theorem 1: the class K possesses the exponential-sized model property, and hence its satisfiability problem is
NExpTime-complete. In addition, it establishes NExpTimecompleteness of two subfragments of K studied in the literature, whose complexity has not been known so far: the Generalised Ackermann Class (without equality) and the K-Skolem class, the latter being the intersection of K and the prefix-class * * (the Skolem class). The matching NExpTime-hardness lower bound holds already for the subclass ∀∀∃ of the latter [27]. Our ∀ ∃ (A) We show that our upper bound on the size of minimal models (and hence also on the complexity) for K transfers to DK, the class of conjunctions of K-sentences. (B) We show that this upper bound is essentially optimal by supplying a family of tight examples, contained already in K-Skolem: we construct a sequence ( ) ∈N of satisfiable sentences such that each has size linear in and its models have size at least 2Ω( ·log ). We can construct such sentences even without constants and with just one existential quantifier. (C) We show that satisfiable sentences in K have models of size 2 (| |), under the assumption that the number of universal quantifiers is bounded; this in particular applies to the Gödel class admitting two universal quantifiers. (D) We propose a novel generalisation of the uniform one-dimensional fragment of First-Order Logic [10]: the ∀-uniform fragment. We show an eficient satisfiability preserving translation to DK, and this way we obtain the exponential-sized model property and NExpTime-completeness of the new fragment.
In contrast to the previous works on K, which approached the problem syntactically, we do it semantically. Let us give a taste of our ideas here; the details can be found in [19].
In our small model construction, a crucial role is played by paradoxical tournament graphs. Let us recall that a directed graph without self-loops is a tournament if it contains exactly one directed arc between every pair of vertices, and a tournament is -paradoxical if, for every subset of vertices
of cardinality at most , there is a vertex dominating , that is sending arcs to all elements of . It is a classical result by Erdős that such tournaments of size ( 2·2 ) exist [28]. Inspired by this classical result, we introduce a variant of tournament graphs with colours of vertices and of arcs.
Let us now explain how we employ such tournaments. Suppose that we want to check the satisfiability of a ︀[ ¬ ( 1, 2) ∨ ¬
K-sentence : ∀ 1, 2.∃. 1 ∧ 2 ∧ 3, where 1 is [︀ ¬ ( 1, 2) ∨ ¬ ︀] ( 2, 1) ∧ ( 1, 2)︀] , saying that is antisymmetric (thus also irreflexive) and disjoint from ; 2 is ( 1, 2) → ︀[ (, 1) ∧ (,
2)︀] , stating that each two elements 1, 2, connected via , share a common predecessor via for 1 and via for 2; and 3 is ¬ ( 1) ↔ ( ), are coloured by : requiring that 1 and disagree on .
We consider a tournament =(, →{, ¬ }
), where arcs are coloured by : . We construct a model A over the domain : →{ 1, 2} and vertices (i) For each ∈ , if its colour via is , we set A |= ( ). (ii) For each , (iii) For each , ∈ , if (, ) is an arc in with colour 1 via , we set A |= (, ).
∈ , if (, ) is an arc in with colour 2 via , we set A |= (, ). (iv) Every other atom of A is set to be false.
Now, imagine that our tournament
has the following paradoxical-like property: for any diferent 1, 2 in and any colour in {, ¬ }, there exists another vertex in such that its colour via is , and there are arcs (, 1), (, 2) in with 1, 2 being their respective colours via . In this case, A indeed becomes a model of . In particular, A |= ∃. 1, 2 with = ¬
existence of (, 1) ∧ (, 2) ∧ (¬ ( 1) ↔ ( )) for any 1 ̸= 2, as the described property applied to if ( 1) = and =
otherwise, gives us an appropriate witness . The satisfying this property follows from our work.
In the general case, we propose a game-theoretic view for the problem: with every K-sentence we associate a satisfiability game , between two players, named Eloisa and Abelard. It resembles a classical verification game , but with the structure not being explicitly given; instead players construct it during the play. We show that Eloisa has a winning strategy if is satisfiable. In establishing the “only if” direction, a crucial role is played by the aforementioned paradoxical tournaments: colours of arcs are variables of , and colours of vertices are certain positions from the game, corresponding to partial structures constructed by players. The core of the model is the tournament, and the atoms are specified in accordance with the colours, similarly as in our example above.
Acknowledgments. The first and second authors were supported by Polish National Science Center grant No. 2021/41/B/ST6/00996. The third author was supported by the ERC grant INFSYS, agreement no. 950398. The authors thank Warren Goldfarb, Ullrich Hustadt and Harry R. Lewis for some helpful comments on their work. [1] D. Scott, A decision method for validity of sentences in two variables, Journal Symbolic
Logic 27 (1962) 477. [2] E. Grädel, P. Kolaitis, M. Y. Vardi, On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic 3 (1997) 53–69. doi:10.2307/421196. [3] H. Andréka, J. van Benthem, I. Németi, Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic 27 (1998) 217–274. doi:10.1023/A:1004275029985. [4] E. Grädel,
On the restraining power of guards, J. Symb. Log. 64 (1999) 1719–1742. 1145/2701414. of Philosophy, volume III, 1969, pp. 57–62.
84 (2019) 1020–1048. doi:10.1017/JSL.2019.33. [5] B. ten Cate, L. Segoufin,
Unary negation, Logical Methods in Comp. Sc. 9 (2013). [7] W. V. Quine, On the limits of decision, in: Proceedings of the 14th International Congress [8] I. Pratt-Hartmann, W. Szwast, L. Tendera, The fluted fragment revisited, J. Symb. Log. [9] B. Bednarczyk, D. Kojelis, I. Pratt-Hartmann, On the limits of decision: the adjacent fragment of first-order logic, in: 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, volume 261 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, pp. 111:1–111:21. doi:10.4230/LIPICS.ICALP.2023.111. [10] L. Hella, A. Kuusisto, One-dimensional fragment of first-order logic, in: Proceedings of
Advances in Modal Logic, 2014, 2014, pp. 274–293. [11] E. Kieronski, A. Kuusisto, Complexity and expressivity of uniform one-dimensional fragment with equality, in: Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Proceedings, Part I, volume 8634 of Lecture Notes in Computer [12] A. Kuusisto,
On the uniform one-dimensional fragment, in: Proceedings of the 29th
International Workshop on Description Logics, 2016. [13] U. Hustadt, R. A. Schmidt, L. Georgieva, A survey of decidable first-order fragments and description logics, Journal of Relational Methods in Computer Science 1 (2004) 2004. [14] S. J. Maslov, The inverse method for establishing deducibility for logical calculi, The
Calculi of Symbolic Logic I: Proceedings of the Steklov Institute of Mathematics 98 (1971). [15] E. Börger, E. Grädel, Y. Gurevich, The classical decision problem, Perspectives in Mathematical Logic, Springer, 1997. [16] C. G. Fermüller, A. Leitsch, T. Tammet, N. K. Zamov, Resolution Methods for the Decision Problem, volume 679 of Lecture Notes in Computer Science, Springer, 1993. doi:10.1007/3-540-56732-1. [17] U. Hustadt, R. A. Schmidt, Maslov’s class K revisited, in: Automated Deduction - CADE16, 16th International Conference on Automated Deduction 1999, Proceedings, volume 1632 of Lecture Notes in Computer Science, Springer, 1999, pp. 172–186. doi:10.1007/ 3-540-48660-7\_12. [18] C. G. Fermüller, A. Leitsch, U. Hustadt, T. Tammet, Resolution decision procedures, in: J. A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning (in 2 volumes), Elsevier and MIT Press, 2001, pp. 1791–1849. doi:10.1016/B978-044450813-3/50027-8. [19] O. Fiuk, E. Kieronski, V. Michielini, On the complexity of Maslov class K, in: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, 2024, pp. 1–14. doi:10.1145/3661814.3662097. [20] W. D. Goldfarb, The unsolvability of the Gödel class with identity, J. Symb. Logic 49 (1984) 1237–1252. doi:10.2307/2274274. [21] L. Löwenheim, Über möglichkeiten im relativkalkül, Mathematische Annalen 76 (1915) 447–470. [22] W. Ackermann, Über die erfüllbarkeit gewisser zählausdrücke, Mathematische Annalen 100 (1928) 638–649. doi:10.1007/BF01448869. [23] M. Voigt, Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates, Ph.D. thesis, Universität des Saarlandes, Saarbrücken, Germany, 2019. [24] K. Gödel, Zum entscheidungsproblem des logischen funktionenkalkuils, Monatshefte fur
Mathematik und Physik 40 (1933) 433–443. [25] B. Draben, W. D. Goldfarb, The Decision Problem: Solvable Classes of Quantificational
Formulas, Addison-Wesly, 1979. [26] E. Kieronski, A uniform one-dimensional fragment with alternation of quantifiers, in: Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, volume 390 of EPTCS, 2023, pp. 1–15. doi:10.4204/ EPTCS.390.1. [27] M. Fürer, The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems), in: Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium “Rekursive Kombinatorik” 1983, volume 171 of Lecture Notes in Computer Science, Springer, 1983, pp. 312–319. doi:10.1007/ 3-540-13331-3\_48. [28] P. Erdös, On a problem in graph theory, The Mathematical Gazette 47 (1963) 220 – 223.