=Paper=
{{Paper
|id=Vol-3739/abstract-11
|storemode=property
|title=On the Complexity of Maslov’s Class K (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-3739/abstract-11.pdf
|volume=Vol-3739
|authors=Oskar Fiuk,Emanuel Kieroński,Vincent Michielini
|dblpUrl=https://dblp.org/rec/conf/dlog/FiukKM24
}}
==On the Complexity of Maslov’s Class K (Extended Abstract)==
https://ceur-ws.org/Vol-3739/abstract-11.pdf
On the Complexity of Maslov’s Class K
(Extended Abstract)
Oskar Fiuk1 , Emanuel Kieroński1 and Vincent Michielini2
1
University of Wrocław, Institute of Computer Science, Wrocław, Poland
2
University of Warsaw, Faculty of Mathematics, Informatics, and Mechanics, Warsaw, Poland
Abstract
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.
Keywords
satisfiability problem, finite model property, Maslov’s class K, paradoxical tournaments
1. Introduction
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 effort 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 [6], the fluted fragment, FF [7, 8], its
generalisation the adjacent fragment, AF [9], and the uniform one-dimensional fragment, UF1
[10, 11, 12]. A survey [13] puts in this context also Maslov’s class K [14].1
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:
DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway
$ 307023@uwr.edu.pl (O. Fiuk); emanuel.kieronski@cs.uni.wroc.pl (E. Kieroński); michielini@mimuw.edu.pl
(V. Michielini)
0009-0006-1312-4899 (O. Fiuk); 0000-0002-8538-8221 (E. Kieroński); 0000-0002-1413-9316 (V. Michielini)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC
BY 4.0).
1
The reader should not confuse the class K with another class, called just the Maslov class (see, e.g. [15]).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
Theorem 1. Every satisfiable formula 𝜙 in K admits a finite model of size 2𝒪(|𝜙|·log |𝜙|) . Hence,
the satisfiability problem for K is NExpTime-complete.
For an extended version of this work see [19].
2. Maslov’s Class K and its relation to other logics
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 ∃𝑥. ∀𝑦. ∃𝑧. 𝑅(𝑥, 𝑦) ∧ 𝑇 (𝑐, 𝑦, 𝑧, 𝑦), with 𝑐 being a constant symbol, then the 𝜙-prefix of
the atom 𝑅(𝑥, 𝑦) is the sequence “∃𝑥. ∀𝑦”, 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. With this
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 different atoms are: the singleton sequences “∀𝑠1 ”, “∀𝑠2 ”,
“∀𝑠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
the conditions are met, with 𝑠1 , 𝑠2 , 𝑠3 being the special variables.
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 ∀𝑥, 𝑦, 𝑧. 𝑇 (𝑥, 𝑦) ∧ 𝑇 (𝑦, 𝑧) → 𝑇 (𝑥, 𝑧), one cannot find a subset of variables that
could work as the set of special variables.
Turning to relation between K and DLs, we need to remark, that actually the standard
translation of, say, 𝒜ℒ𝒞 into FO does not land directly in K. To embed 𝒜ℒ𝒞 in K, we first
translate 𝒜ℒ𝒞 into FO2 , and then write the FO2 formula in its Scott normal form: ∀𝑥, 𝑦. 𝜙0 (𝑥, 𝑦)∧
𝑖 ∀𝑥.∃𝑦. 𝜙𝑖 (𝑥, 𝑦). One can verify that after renaming the variables in the ∀∃-conjuncts we
⋀︀
indeed get sentences in K.
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
K-sentences, also known to be decidable [17].
3. Our results
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 NExpTime-
completeness 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
remaining results are as follows:
(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 efficient satisfiability preserving translation to
DK, and this way we obtain the exponential-sized model property and NExpTime-completeness
of the new fragment.
4. Proof strategy
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 K-sentence
]︀
𝜙: ∀𝑥1 , 𝑥2 .∃𝑦. 𝜓1 ∧ 𝜓2 ∧ 𝜓 3 , where 𝜓1 is ¬𝑅(𝑥 1 , 𝑥2 ) ∨ ¬𝑅(𝑥 2 , 𝑥1 ) ∧
¬𝑅(𝑥1 , 𝑥2 ) ∨ ¬𝑆(𝑥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 ) ↔ 𝑈 (𝑦),
requiring that 𝑥1 and 𝑦 disagree on 𝑈 .
We consider a tournament 𝒯 =(𝑉, 𝐸), where arcs are coloured by 𝜆 : 𝐸→{𝑥1 , 𝑥2 } and vertices
are coloured by 𝜇 : 𝑉 →{𝑈, ¬𝑈 }. We construct a model A over the domain 𝑉 :
(i) For each 𝑎 ∈ 𝑉 , if its colour via 𝜇 is 𝑈 , we set A |= 𝑈 (𝑎).
(ii) For each 𝑎, 𝑏 ∈ 𝑉 , if (𝑎, 𝑏) is an arc in 𝐸 with colour 𝑥1 via 𝜆, we set A |= 𝑅(𝑎, 𝑏).
(iii) For each 𝑎, 𝑏 ∈ 𝑉 , 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
different 𝑣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 ) ∧ (¬𝑈 (𝑣1 ) ↔ 𝑈 (𝑦)) for any 𝑣1 ̸= 𝑣2 , as the described property applied to
𝑣1 , 𝑣2 with 𝑐 = ¬𝑈 if 𝜇(𝑣1 ) = 𝑈 and 𝑐 = 𝑈 otherwise, gives us an appropriate witness 𝑤. The
existence of 𝒯 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 iff 𝜙 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.
References
[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.
doi:10.2307/2586808.
[5] B. ten Cate, L. Segoufin, Unary negation, Logical Methods in Comp. Sc. 9 (2013).
doi:10.2168/LMCS-9(3:25)2013.
[6] V. Bárány, B. ten Cate, L. Segoufin, Guarded negation, J. ACM 62 (2015) 22. doi:10.
1145/2701414.
[7] W. V. Quine, On the limits of decision, in: Proceedings of the 14th International Congress
of Philosophy, volume III, 1969, pp. 57–62.
[8] I. Pratt-Hartmann, W. Szwast, L. Tendera, The fluted fragment revisited, J. Symb. Log.
84 (2019) 1020–1048. doi:10.1017/JSL.2019.33.
[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
Science, 2014, pp. 365–376. doi:10.1007/978-3-662-44522-8\_31.
[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 Mathe-
matical 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 - CADE-
16, 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.