Pith. sign in

REVIEW 2 major objections 4 minor 1 cited by

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions

T0 review · 2 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that monodic guarded and two-variable counting fragments of first-order modal logic remain decidable when non-rigid constants, definite descriptions, and counting are added, with tight complexity bounds.

desk verdict Strong and genuinely new decidability results for monodic modal fragments with non-rigid constants and counting, but the C2 upper bound rests on a sketched Lemma 26 that needs to be filled in before the paper is complete. read the letter →

arxiv 2509.08165 v1 pith:DCXO4UVW submitted 2025-09-09 cs.LO math.LO

Alessandro Artale , Christopher Hampson , Roman Kontchakov , Andrea Mazzullo , Frank Wolter This is my paper · ORCID
classification cs.LOmath.LO MSC 03B4503B2503B7068Q15
keywords first-ordermodallogicmonodicfragmentnon-rigidconstantsdefinitedescriptionscountingquantifiersguardedtwo-variablequasimodels
topics P versus NP
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to show that three features usually blamed for undecidability in first-order modal logic—non-rigid constants, definite descriptions, and counting quantifiers—can be added to monodic fragments without destroying decidability. It establishes that validity in the monodic guarded fragment and in the monodic two-variable fragment with counting is decidable over K_n and S5_n frames, with tight 2ExpTime and coNExpTime bounds respectively. The proof works by replacing models with finite "weak quasimodels": multisets of types and runs that record how many individuals realise each type at each world. A sympathetic reader cares because these features are exactly what make modal logic useful for representing names, descriptions, and numerical information in philosophy and knowledge representation.

What carries the argument

Weak quasimodel: a finite tree-shaped Kripke frame in which each world is labelled by a multiset of types (Boolean-saturated sets of one-variable subformulas), and domain elements are represented as multisets of weak runs—functions from upward-closed sets of worlds to types that satisfy coherence but not necessarily saturation. A prototype function p(w,t) marks one saturated run of each type at each world; this lets the construction keep finitely many worlds by allowing the remaining runs to be unsaturated, then "repairs" them by duplicating witness worlds (Lemmas 13-14). For the counting fragment, weak runs are further replaced by local links between quasistates satisfying linear equations,

What would settle it

Apply the Lemma 26 procedure to a small C2 sentence whose types are known; if any solution to the produced Diophantine system fails to correspond to a realisable quasistate, the coNExpTime upper-bound proof for the counting fragment collapses.

Watch

Extended reading notes

Core claim

The central claim is that satisfiability of Q=21MLc sentences in the monodic guarded fragment GF=21MLc over K_n and S5_n is 2ExpTime-complete (Theorem 21), and in the monodic two-variable counting fragment C2_21MLc is coNExpTime-complete (Theorem 27), with the same bounds for constant and expanding domains. The technical content is an equivalence: a sentence is satisfiable iff there exists a weak quasimodel of at most exponential size (Lemmas 13 and 14), where quasistates are multisets of types and domain elements are multisets of runs, with a prototype function witnessing saturation. Counting and equality are handled by the multiplicities, and the existing decision procedures for the underl

Load-bearing premise

The upper bounds for the counting and temporal results rest on two delegated technical steps—an exponential-time linear-equation encoding of counting-fragment quasistates and a reduction from temporal to transitive-closure modal logics—that the paper sketches rather than proves in full.

Editorial extensions

If this is right

  • Validity in the monodic guarded fragment with non-rigid constants, equality, and closed definite descriptions is 2ExpTime-complete on K_n and S5_n, matching the non-modal guarded fragment's complexity.
  • Validity in the monodic two-variable fragment with counting is coNExpTime-complete on K_n and S5_n, again matching its non-modal base.
  • Over finite acyclic frames with expanding domains, the transitive-closure extension of these monodic fragments is decidable; the one-variable case is Ackermann-hard.
  • The one-variable fragment is coNExpTime-complete for constant domains but PSpace-complete for expanding domains on K_n.
  • These decidability results transfer to monodic temporal logics over finite strict linear orders with expanding domains for the guarded and counting fragments.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The weak-quasimodel method should transfer to other decidable first-order fragments with a monotone finite-model property, such as guarded negation or fluted fragments; testing that would require proving an analogue of Lemma 20 for those fragments.
  • The PSpace versus coNExpTime gap between expanding and constant domains in the one-variable fragment suggests that expanding-domain semantics can systematically lower complexity elsewhere; the paper does not investigate whether GF or C2 exhibit a similar gap.
  • Because Lemma 26 is the only non-elementary-looking step in the C2 upper bound, a simpler or fully constructive proof of that lemma would likely give a more modular route to complexity results for other counting extensions.
  • The decidability boundary for transitive-closure modal logic appears to be the absence of infinite ascending chains; extending the Kf*_n decidability argument to arbitrary K*_n frames would require a well-quasi-ordering argument that the paper's Dickson's Lemma technique does not provide.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper studies monodic fragments of first-order modal logic with non-rigid constants, definite descriptions, equality, and counting (NRDC features) over K_n and S5_n, and over transitive-closure/temporal frames. It develops a quantitative quasimodel technique in which quasistates are multisets of types, runs are multisets, and a prototype function supplies local saturation witnesses. The main positive results are: Q1=MLc validity is coNExpTime-complete on K_n and S5_n with constant domains (Theorem 19), GF=21MLc validity is 2ExpTime-complete on K_n and S5_n in both constant and expanding domains (Theorem 21), C2_21MLc validity is coNExpTime-complete (Theorem 27), expanding-domain Q1=MLc validity on K_n is PSpace-complete (Theorem 41), and Kf*_n validity for C2_21MLc and GF=21MLc with expanding domains is decidable (Theorem 37), with a transfer to finite linear temporal frames (Theorem 44). The paper also records several undecidability results, including global consequence over K_n/S5_n and Ackermann-hardness for transitive-closure variants.

Significance. If the technical results are correct, this is a substantial contribution: it shows that NRDC features, which cause undecidability in several one-variable first-order modal/temporal logics, can still be handled in the monodic fragments over K_n and S5_n by means of counting-aware weak quasimodels. The quasimodel equivalence proofs (Lemmas 9, 13, 14, 22) and the guarded-fragment upper-bound argument are detailed and largely self-contained modulo standard GF results. The paper is also honest in marking its sketches. However, the central coNExpTime upper bound for C2_21MLc depends on Lemma 26, whose proof is only a two-item sketch, and the temporal-to-modal transfer depends on Lemma 43, whose proof is a one-sentence citation. Until those are supplied, the corresponding theorems should be treated as conditional.

major comments (2)
  1. [Section 7.3, Lemma 26] This lemma is load-bearing for the coNExpTime upper bound in Theorem 27 and, through Theorem 6(c), for the expanding-domain version as well. The proof is explicitly a sketch with two observations. Observation (2) is exactly the delicate step: expressing 'our' types as disjunctions of [8]'s star-types and then eliminating the star-type variables from the [8] systems. No argument is given that the elimination preserves linearity of the resulting constraints, keeps coefficients within double exponential size, preserves the exponential bound on the number of equation sets, or yields exponential-time membership in C. Observation (1) only asserts that small models are handled by 'new sets of equations' without defining them. Since Theorem 27's upper bound depends entirely on this lemma, the proof is incomplete. Please provide a full construction, or state and prove a precise theorem from [8] t
  2. [Section 9, Lemma 43] The proof of this lemma is a single sentence: it is 'not trivial' but can be done by adapting [4, Theorem 6.24]. The lemma is used to transfer the LTL lower bounds to K*_n and Kf*_n and to derive Theorem 44 from Theorem 37. The cited theorem concerns product modal logics and does not, as cited, cover definite descriptions, partial designators, or counting. The reduction must be stated in enough detail to verify that it preserves validity in both directions for the NRDC languages in question. As written, the transfer is not verifiable and the lower-bound/decidability conclusions that rely on it are unsupported.
minor comments (4)
  1. [Section 5, Lemma 13] The proof begins with a quasimodel Q=(F,q,R,p), but quasimodels were defined in Section 4 as triples (F,q,R) without a prototype function. This is harmless—one can choose p(w,t) arbitrarily for each (w,t) with q(w,t)>0—but the definition should be aligned or the choice of p should be stated.
  2. [Section 7.2, Theorem 21 proof] The proof says 'so O' is a quasimodel' after checking realisability of the q'(w). The object constructed is a weak quasimodel; to obtain a genuine quasimodel one must invoke Lemma 14. Please add the missing sentence (and correct 'O'' to 'Q'').
  3. [Section 7.3] Typo: 'countring' should be 'counting' in the sentence introducing the need for a more subtle combination with the upper bound proofs.
  4. [Section 8.2, Lemma 39 / Small Non-Root rule] In condition (a) of the Small Non-Root construction, 'ρ(w)∈q(w)' appears to be a typo for 'ρ(w)∈q'(w)'; otherwise the condition would keep all prototypes and defeat the purpose of the reduction.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: proofs are self-contained via quasimodels; self-citations and deferred lemmas are external or non-load-bearing.

full rationale

The central decidability and complexity results are built from explicit quasimodel/weak-quasimodel representation lemmas (Lemmas 9, 13, 14, 16, 17, 22, 23) that are proved in the paper, and the target validity problems are reduced to the existence of such quasimodels rather than assumed. No equation is defined in terms of the result it proves, and no fitted data are relabeled as predictions. The paper does contain self-citations: [41,42] are credited as the source of ideas ('This article significantly extends ideas first developed by the authors in the context of modal and temporal description logics'), and some lower bounds are transferred via [13,45], which include the authors. However, these are externally published, independently checkable results and are not used as the sole justification for the paper's main upper bounds. The most fragile step, Lemma 26, is explicitly deferred to Pratt-Hartmann's external monograph [8] ('The proof of this lemma is based on [8, Sections 8.4 and 8.5] and is rather cumbersome, but straightforward in principle'); although this is a missing-proof/correctness risk in this submission, it is not a circularity because the cited source is not the present paper or a self-authored uniqueness theorem. Similarly, Lemma 43 is described as 'adapting in a straightforward way the reduction given in the proof of [4, Theorem 6.24]', an independent published result. Overall, the derivation chain does not reduce to its own inputs; the observed self-citations are minor and non-load-bearing.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numerical parameters are fitted to data; the paper is a pure decidability-proof contribution. Weak quasimodels, multisets of runs, links, and surrogates are defined proof devices, not empirical entities requiring external falsifiable evidence. The central results rest on standard theorems in finite model theory and modal logic, which are cited explicitly.

assumptions (5)
  • standard math Dickson's Lemma: every bad sequence of multisets over finite types is finite.
    Used in Theorem 34 to bound lengths of paths in weak quasimodels for transitive-closure logics (Section 8.1).
  • standard math The guarded fragment of first-order logic has a double-exponential finite model property (Bárány, Gottlob, Otto).
    Used in Lemma 20(2) and Lemma 35 to bound quasistate multiplicities for the guarded fragment.
  • standard math C2, the two-variable fragment with counting, has a NExpTime satisfiability procedure with solution bounds representable by linear extended-Diophantine equations (Pratt-Hartmann).
    Used in Lemma 26 and Theorem 27 for the coNExpTime upper bound of C2_21MLc. This is the main external anchor for the counting-fragment result.
  • domain assumption Standard Kripke semantics with expanding or constant domains, with non-rigid and possibly non-designating constants and definite descriptions (Section 2.1).
    The entire paper is about these semantics; all results are relative to them.
  • domain assumption Monodicity: modal operators apply only to formulas with at most one free variable (Section 2.2).
    This restriction defines the fragments under investigation and is necessary for the quasimodel technique.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions." pith.science (2026). https://pith.science/paper/DCXO4UVW

@misc{pith2026250908165,
  author       = {Pith},
  title        = {Pith review of: Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DCXO4UVW}},
  note         = {Machine review of arXiv:2509.08165}
}
abstract

While modal extensions of decidable fragments of first-order logic are usually undecidable, their monodic counterparts, in which formulas in the scope of modal operators have at most one free variable, are typically decidable. This only holds, however, under the provision that non-rigid constants, definite descriptions and non-trivial counting are not admitted. Indeed, several monodic fragments having at least one of these features are known to be undecidable. We investigate these features systematically and show that fundamental monodic fragments such as the two-variable fragment with counting and the guarded fragment of standard first-order modal logics $\mathbf{K}_{n}$ and $\mathbf{S5}_{n}$ are decidable. Tight complexity bounds are established as well. Under the expanding-domain semantics, we show decidability of the basic modal logic extended with the transitive closure operator on finite acyclic frames; this logic, however, is Ackermann-hard.

Figures

Figures reproduced from arXiv: 2509.08165 by the authors.

Figure 1
Figure 1. An interpretation satisfying φ in Example 7. 4. Quasimodels for Q= ✷1 MLc In this section we present a straightforward generalisation of the standard quasimodel technique (see, e.g., [4]) to the languages with constants, equality and/or counting quantifiers. For every monodic formula of the form ✸aψ(x) with one free variable x, we reserve a unary predicate R✸aψ(x), and, for every monodic sentence of the form ✸aψ, a … view at source ↗
Figure 2
Figure 2. A quasimodel for the interpretation in Fig. 1. [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗
Figure 3
Figure 3. (a) A weak quasimodel in Example 12 and (b) its saturated quasimodel [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: An example of a tree-shaped S5n frame. witness w ∈ W such that u˜Raw and ψ ∈ p(u˜, t)(w). By construction, we have w = u˜aw, for some w. Consider v = ua(w, σ), where σ ∈ Rep(u˜) swaps τu(ρ, ℓ) with (p(u˜, t), 0). By definition, we have v˜ = w, uR′ av and ρ ′ (v) = σ(τu…
Figure 5
Figure 5. Figure 5: Replacing ρ0 with ρ ′ 0 and the ρ0↓u to satisfy (†∞): types with infinite multiplicity are white circles, types with finite multiplicity are grey circles. (†∞) for all ρ ∈ Rw with ρ /∈ p(w), if ρ /∈ fin(w), then ρ /∈ fin(v), for all v ∈ W↓w. We prove (†∞) by induction …
Figure 6
Figure 6. Figure 6: Drop interval operation on quasimodels in the proof of Lemma 36. [PITH_FULL_IMAGE:figures/full_fig_p045_6.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Fusions of One-Variable First-Order Modal Logics

    cs.LO 2026-03 conditional novelty 8.0 of 10

    Fusing one-variable first-order modal logics preserves completeness and decidability without equality, but adding equality and non-rigid constants can make fusions undecidable.

Reference graph

Works this paper leans on

74 extracted references · 74 canonical work pages · cited by 1 Pith paper

  1. [8]

    Pratt-Hartmann, Fragments of first-order logic, Vol

    I. Pratt-Hartmann, Fragments of first-order logic, Vol. 56, Oxford Univer- sity Press, 2023

    work page 2023

  2. [1]

    Börger, E

    E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997

    work page 1997

  3. [2]

    S. A. Kripke, The undecidability of monadic modal quantification theory, Mathematical Logic Quarterly 8 (2) (1962) 113–116

    work page 1962

  4. [3]

    M. N. Rybakov, D. Shkatov, Variations on the Kripke trick, Studia Logica 113 (1) (2025) 1–48

    work page 2025

  5. [4]

    D.M.Gabbay, A.Kurucz, F.Wolter, M.Zakharyaschev, Many-dimensional Modal Logics: Theory and Applications, North Holland Publishing Com- pany, 2003. 52

    work page 2003

  6. [5]

    Braüner, S

    T. Braüner, S. Ghilardi, First-order Modal Logic, in: Handbook of Modal Logic, Elsevier, 2007, pp. 549–620

    work page 2007

  7. [6]

    M. N. Rybakov, D. Shkatov, Undecidability of first-order modal and intu- itionistic logics with two variables and one monadic predicate letter, Studia Logica 107 (4) (2019) 695–717

    work page 2019

  8. [7]

    M. N. Rybakov, Predicate counterparts of modal logics of provability: High undecidabilityandKripkeincompleteness, LogicJournaloftheIGPL32(3) (2024) 465–492

    work page 2024

Show all 74 references
  1. [9]

    Wolter, M

    F. Wolter, M. Zakharyaschev, Decidable fragments of first-order modal logics, J. Symb. Log. 66 (3) (2001) 1415–1438

    2001

  2. [10]

    I. M. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of decidable fragments of first-order lin- ear temporal logics, in: Proc. of the 10th Int. Symposium on Temporal Representation and Reasoning and of the 4th Int. Conf. on Te...

    2003

  3. [11]

    I. M. Hodkinson, Complexity of monodic guarded fragments over linear and real time, Ann. Pure Appl. Log. 138 (1-3) (2006) 94–125

    2006

  4. [12]

    Degtyarev, M

    A. Degtyarev, M. Fisher, A. Lisitsa, Equality and monodic first-order tem- poral logic, Studia Logica 72 (2) (2002) 147–156

    2002

  5. [13]

    Hampson, A

    C. Hampson, A. Kurucz, Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting, ACM Trans. Comput. Log. 16 (3) (2015) 27:1–27:36

    2015

  6. [14]

    Hampson, A

    C. Hampson, A. Kurucz, On modal products with the logic of ‘elsewhere’, in: Proc.ofthe9thConf.onAdvancesinModalLogic(AiML2012), College Publications, 2012, pp. 339–347

    2012

  7. [15]

    Linsky (Ed.), Reference and Modality, Oxford University Press, 1971

    L. Linsky (Ed.), Reference and Modality, Oxford University Press, 1971

    1971

  8. [16]

    LaPorte, Rigid designation and theoretical identities, Oxford University Press, 2012

    J. LaPorte, Rigid designation and theoretical identities, Oxford University Press, 2012

    2012

  9. [17]

    Martí, Reference and theories of reference, in: The Cambridge Hand- book of the Philosophy of Language, Cambridge University Press, 2021, pp

    G. Martí, Reference and theories of reference, in: The Cambridge Hand- book of the Philosophy of Language, Cambridge University Press, 2021, pp. 233–248

    2021

  10. [18]

    Kürbis, A binary quantifier for definite descriptions for cut free free logics, Studia Logica 110 (1) (2022) 219–239

    N. Kürbis, A binary quantifier for definite descriptions for cut free free logics, Studia Logica 110 (1) (2022) 219–239

    2022

  11. [19]

    Indrzejczak, Russellian definite description theory — a proof theoretic approach, Rev

    A. Indrzejczak, Russellian definite description theory — a proof theoretic approach, Rev. Symb. Log. 16 (2) (2023) 624–649. 53

    2023

  12. [20]

    Petrukhin, A binary quantifier for definite descriptions in Nelsonian free logic, in: Proc

    Y. Petrukhin, A binary quantifier for definite descriptions in Nelsonian free logic, in: Proc. of the 11th Int. Conf. on Non-Classical Logics. Theory and Applications (NCL 2024), Vol. 415 of EPTCS, 2024, pp. 5–15

    2024

  13. [21]

    Artale, A

    A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On free description logics with definite descriptions, in: Proc. of the 33rd Int. Workshop on Description Logics(DL-20), Vol.2663ofCEURWorkshopProceedings, CEUR-WS.org, 2020

    2020

  14. [22]

    Neuhaus, O

    F. Neuhaus, O. Kutz, G. Righetti, Free description logic for ontologists, in: Proc. of the Joint Ontology Workshops (JOWO-20), Vol. 2708 of CEUR Workshop Proceedings, CEUR-WS.org, 2020

    2020

  15. [23]

    Artale, A

    A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On free description logics with definite descriptions, in: Proc. of the 18th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2021), 2021, pp. 63–73

    2021

  16. [24]

    Indrzejczak, Existence, definedness and definite descriptions in hybrid modal logic, in: Proc

    A. Indrzejczak, Existence, definedness and definite descriptions in hybrid modal logic, in: Proc. of the 13th Conf. on Advances in Modal Logic (AiML 2020), College Publications, 2020, pp. 349–368

    2020

  17. [25]

    Orlandelli, Labelled calculi for quantified modal logics with definite de- scriptions, J

    E. Orlandelli, Labelled calculi for quantified modal logics with definite de- scriptions, J. Log. Comput. 31 (3) (2021) 923–946

    2021

  18. [26]

    P. A. Walega, M. Zawidzki, Hybrid modal operators for definite descrip- tions, in: Proc. of the 18th European Conf. on Logics in Artificial Intelli- gence (JELIA 2023), Vol. 14281 of LNCS, Springer, 2023, pp. 712–726

    2023

  19. [27]

    P. A. Walega, Expressive power of definite descriptions in modal logics, in: Proc. of the 21st Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2024), 2024, pp. 687–696

    2024

  20. [28]

    K. J. J. Hintikka, Knowledge and belief: An introduction to the logic of the two notions, Cornell University Press, 1962

    1962

  21. [29]

    Lomuscio, M

    A. Lomuscio, M. Colombetti, QLB: A quantified logic for belief, in: Proc. of the ECAI’96 Workshop on Agent Theories, Architectures, and Languages (ATAL), Vol. 1193, Springer, 1996, pp. 71–85

    1996

  22. [30]

    Belardinelli, A

    F. Belardinelli, A. Lomuscio, Quantified epistemic logics for reasoning about knowledge in multi-agent systems, Artif. Intell. 173 (9-10) (2009) 982–1013

    2009

  23. [31]

    Wolter, First order common knowledge logics, Studia Logica 65 (2) (2000) 249–271

    F. Wolter, First order common knowledge logics, Studia Logica 65 (2) (2000) 249–271

    2000

  24. [32]

    An EATCS Series, Springer, 2008

    F.Kröger, S.Merz, TemporalLogicandStateSystems, TextsinTheoretical Computer Science. An EATCS Series, Springer, 2008

    2008

  25. [33]

    Indrzejczak, M

    A. Indrzejczak, M. Zawidzki, Definite descriptions and hybrid tense logic, Synthese 202 (3) (2023) 98. 54

    2023

  26. [34]

    Geatti, A

    L. Geatti, A. Gianola, N. Gigante, Linear temporal logic modulo theories over finite traces, in: Proc. of the 31st Int. Joint Conf. on Artificial Intelli- gence (IJCAI 2022), ijcai.org, 2022, pp. 2641–2647

    2022

  27. [35]

    of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), IEEE Computer Society, 1997, pp

    E.Grädel, M.Otto, E.Rosen, Two-variablelogicwithcountingisdecidable, in: Proc. of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), IEEE Computer Society, 1997, pp. 306–317

    1997

  28. [36]

    Pratt-Hartmann, Complexity of the two-variable fragment with counting quantifiers, J

    I. Pratt-Hartmann, Complexity of the two-variable fragment with counting quantifiers, J. Log. Lang. Inf. 14 (3) (2005) 369–395

    2005

  29. [37]

    Pratt-Hartmann, Data-complexity of the two-variable fragment with counting quantifiers, Inf

    I. Pratt-Hartmann, Data-complexity of the two-variable fragment with counting quantifiers, Inf. Comput. 207 (8) (2009) 867–888

    2009

  30. [38]

    Andréka, I

    H. Andréka, I. Németi, J. van Benthem, Modal languages and bounded fragments of predicate logic, J. Philosophical Logic 27 (3) (1998) 217–274

    1998

  31. [39]

    Grädel, On the restraining power of guards, J

    E. Grädel, On the restraining power of guards, J. Symb. Log. 64 (4) (1999) 1719–1742

    1999

  32. [40]

    Bárány, G

    V. Bárány, G. Gottlob, M. Otto, Querying the guarded fragment, Logical Methods in Computer Science 10 (2) (2014)

    2014

  33. [41]

    Artale, R

    A. Artale, R. Kontchakov, A. Mazzullo, F. Wolter, Non-rigid designators in modal and temporal free description logics, in: Proc. of the 21st Int. Conf. on Principles of Knowledge Representation and Reasoning (KR-2024), IJ- CAI Inc., 2024, pp. 82–93

    2024

  34. [42]

    Artale, R

    A. Artale, R. Kontchakov, A. Mazzullo, F. Wolter, An update on non-rigid designators in modalised description logics (extended abstract), in: Proc. of the 37th Int. Workshop on Description Logics (DL 2024), Vol. 3739 of CEUR Workshop Proceedings, CEUR-WS.org, 2024

    2024

  35. [43]

    Fitting, R

    M. Fitting, R. L. Mendelsohn, First-order Modal Logic, Springer Science & Business Media, 2012

    2012

  36. [44]

    Marx, Complexity of products of modal logics, J

    M. Marx, Complexity of products of modal logics, J. Log. Comput. 9 (2) (1999) 197–214

    1999

  37. [45]

    Gabelaia, A

    D. Gabelaia, A. Kurucz, F. Wolter, M. Zakharyaschev, Non-primitive re- cursive decidability of products of modal logics with expanding domains, Ann. Pure Appl. Log. 142 (1-3) (2006) 245–268

    2006

  38. [46]

    Hampson, Decidable first-order modal logics with counting quantifiers, in: Proc

    C. Hampson, Decidable first-order modal logics with counting quantifiers, in: Proc. of the 11th Conf. on Advances in Modal Logic (AiML 2016), College Publications, 2016, pp. 382–400

    2016

  39. [47]

    Gargov, V

    G. Gargov, V. Goranko, Modal logic with names, J. Philos. Log. 22 (6) (1993) 607–636. 55

    1993

  40. [48]

    Lasaruk, T

    A. Lasaruk, T. Sturm, Effective quantifier elimination for Presburger Arith- metic with infinity, in: Proc. of the 11th Int. Workshop on Computer Al- gebra in Scientific Computing (CASC 2009), Vol. 5743 of LNCS, Springer, 2009, pp. 195–212

    2009

  41. [49]

    M. J. Fischer, R. E. Ladner, Propositional modal logic of programs (ex- tended abstract), in: Proc. of the 9th Annual ACM Symposium on Theory of Computing (SToC’77), ACM, 1977, pp. 286–294

    1977

  42. [50]

    Schmitz, P

    S. Schmitz, P. Schnoebelen, Multiply-recursive upper bounds with Hig- man’s lemma, in: Proc. of the 38th Int. Colloquium on Automata, Lan- guages and Programming (ICALP 2011), Part II, Vol. 6756 of LNCS, Springer, 2011, pp. 441–452

    2011

  43. [51]

    Figueira, S

    D. Figueira, S. Figueira, S. Schmitz, P. Schnoebelen, Ackermannian and primitive-recursive bounds with Dickson’s lemma, in: Proc. of the 26th AnnualIEEESymposiumonLogicinComputerScience(LICS2011), IEEE Computer Society, 2011, pp. 269–278

    2011

  44. [52]

    Spaan, Complexity of modal logics, Ph.D

    E. Spaan, Complexity of modal logics, Ph.D. thesis, University of Amster- dam (1993)

    1993

  45. [53]

    Blackburn, M

    P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001

    2001

  46. [54]

    Degtyarev, M

    A. Degtyarev, M. Fisher, B. Konev, Monodic temporal resolution, ACM Trans. Comput. Log. 7 (1) (2006) 108–150

    2006

  47. [55]

    Kourtis, C

    G. Kourtis, C. Dixon, M. Fisher, Monodic fragments of probabilistic first- order temporal logic with bounded semantics, Theoretical Computer Sci- ence 1046 (2025) 115319

    2025

  48. [56]

    Semantic properties, decidable fragments, and applications, ACM Trans

    A.Artale, A.Mazzullo, A.Ozaki, First-ordertemporallogiconfinitetraces. Semantic properties, decidable fragments, and applications, ACM Trans. Computat. Log. 25 (2) (2024) 1–43

    2024

  49. [57]

    Konev, F

    B. Konev, F. Wolter, M. Zakharyaschev, Temporal logics over transitive states, in: Proc. of the 20th Int. Conf. on Automated Deduction (CADE- 20), Vol. 3632 of LNCS, Springer, 2005, pp. 182–203

    2005

  50. [58]

    Bárány, M

    V. Bárány, M. Benedikt, B. ten Cate, Some model theory of guarded nega- tion, J. Symb. Log. 83 (4) (2018) 1307–1344

    2018

  51. [59]

    Pratt-Hartmann, L

    I. Pratt-Hartmann, L. Tendera, The fluted fragment with transitive rela- tions, Ann. Pure Appl. Log. 173 (1) (2022) 103042

    2022

  52. [60]

    Pratt-Hartmann, L

    I. Pratt-Hartmann, L. Tendera, Adding transitivity and counting to the fluted fragment, in: Proc. of 31st EACSL Annual Conf. on Computer Sci- ence Logic (CSL 2023), Vol. 252 of LIPIcs, Schloss Dagstuhl - Leibniz- Zentrum für Informatik, 2023, pp. 32:1–32:22. 56

    2023

  53. [61]

    C. Lutz, F. Wolter, M. Zakharyaschev, Temporal description logics: A survey, in: Proc. of the 15th Int. Symposium on Temporal Representation and Reasoning (TIME-08), IEEE Computer Society, 2008, pp. 3–14

    2008

  54. [62]

    Baader, S

    F. Baader, S. Ghilardi, C. Lutz, LTL over description logic axioms, ACM Trans. Comput. Log. 13 (3) (2012)

    2012

  55. [63]

    Artale, R

    A. Artale, R. Kontchakov, V. Ryzhikov, M. Zakharyaschev, A cookbook for temporal conceptual data modelling with description logics, ACM Trans. Comput. Log. 15 (3) (2014) 25:1–25:50

    2014

  56. [64]

    Baader, S

    F. Baader, S. Borgwardt, P. Koopmann, A. Ozaki, V. Thost, Metric tem- poral description logics with interval-rigid names, ACM Trans. Comput. Log. 21 (4) (2020) 1–46

    2020

  57. [65]

    Artale, R

    A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Za- kharyaschev, Ontology-mediated query answering over temporal data: A survey (invited talk), in: Proc. of the 24th Int. Symposium on Temporal Representation and Reasoning (TIME 2017), Vol. 90 of LIPIcs, Schl...

    2017

  58. [66]

    Cuenca Grau, I

    B. Cuenca Grau, I. Horrocks, O. Kutz, U. Sattler, Will my ontologies fit together?, in: Proc. of the 2006 Int. Workshop on Description Logics (DL2006), Vol. 189 of CEUR Workshop Proceedings, CEUR-WS.org, 2006

    2006

  59. [67]

    M. Liu, A. Padmanabha, R. Ramanujam, Y. Wang, Are bundles good deals for first-order modal logic?, Inf. Comput. 293 (2023) 105062

    2023

  60. [68]

    M. Liu, A. Padmanabha, R. Ramanujam, Y. Wang, Generalized bundled fragments for first-order modal logic, in: Proc. of the 47th Int. Symposium on Mathematical Foundations of Computer Science (MFCS 2022), Vol. 241 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 202...

    2022

  61. [69]

    Fitting, L

    M. Fitting, L. Thalmann, A. Voronkov, Term-Modal Logics, Studia Logica 69 (1) (2001) 133–169

    2001

  62. [70]

    Kooi, Dynamic term-modal logic, in: Proc

    B. Kooi, Dynamic term-modal logic, in: Proc. of the Workshop on Logic, Rationality and Interaction, College Publications, 2008, pp. 173–185

    2008

  63. [71]

    Corsi, E

    G. Corsi, E. Orlandelli, Free quantified epistemic logics, Studia Logica 101 (6) (2013) 1159–1183

    2013

  64. [72]

    A. O. Liberman, A. Achen, R. K. Rendsvig, Dynamic term-modal logics for first-order epistemic planning, Artif. Intell. 286 (2020) 103305

    2020

  65. [73]

    Y. Wang, Y. Wei, J. Seligman, Quantifier-free epistemic term-modal logic with assignment operator, Ann. Pure Appl. Log. 173 (3) (2022) 103071

    2022

  66. [74]

    Padmanabha, R

    A. Padmanabha, R. Ramanujam, A decidable fragment of first order modal logic: Two variable term modal logic, ACM Trans. Comput. Log. 24 (4) (2023) 29:1–29:38. 57

    2023

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.