2026-07-21T20:02:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23539 2025-10-02T12:58:11Z ddc:004 open_access

Positive and Monotone Fragments of FO and LTL Iosti, Simon Kuperberg, Denis Moreau, Quentin Positive logic LTL separation first-order monotone We study the positive logic FO^+ on finite words, and its fragments, pursuing and refining the work initiated in [Denis Kuperberg, 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO^+ is equivalent to LTL^+, and its two-variable fragment FO^{2+} with (resp. without) successor available is equivalent to UTL^+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO^+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO^+-definable, refining the example from [Denis Kuperberg, 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO²-definable. Finally, we provide a new example distinguishing the positive and monotone versions of FO² without quantifier alternation. This does not rely on a variant of the previously known counter-example, and witnesses a new phenomenon. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simon Iosti and Denis Kuperberg and Quentin Moreau 2025 Is Part Of LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2025.162 urn:nbn:de:0030-drops-235398 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.162 eng https://creativecommons.org/licenses/by/4.0/legalcode