<?xml version="1.0" encoding="UTF-8"?>
<rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom" xmlns:slash="http://purl.org/rss/1.0/modules/slash/">
  <channel>
    <title>Logical Methods in Computer Science</title>
    <description>Logical Methods in Computer Science: latest publications</description>
    <image>
      <url>https://lmcs.episciences.org/logos/logo-lmcs-small.svg</url>
      <title>Logical Methods in Computer Science</title>
      <link>https://lmcs.episciences.org</link>
    </image>
    <pubDate>Sun, 21 Jun 2026 06:21:18 +0000</pubDate>
    <generator>Episciences</generator>
    <link>https://lmcs.episciences.org</link>
    <author>Logical Methods in Computer Science</author>
    <dc:creator>Logical Methods in Computer Science</dc:creator>
    <atom:link rel="self" type="application/rss+xml" href="https://api.episciences.org/api/feed/rss/lmcs"/>
    <atom:link rel="hub" href="https://pubsubhubbub.appspot.com/"/>
    <item>
      <title>Hofmann-Streicher lifting of fibred categories</title>
      <description><![CDATA[In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe from the category of sets into the category of set-valued presheaves on a small category. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the categorical nerve, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, the categorical nerve's functorial action on the universal small discrete fibration gives the generic family of the universe's Hofmann-Streicher lifting. Inspired by Awodey's analysis, we define a relative version of Hofmann-Streicher lifting in terms of the right pseudo-adjoint to the 2-functor given by postcomposition with a fibration. Finally, we construct a new 2-bifibration of fibrations in which the opcartesian and cartesian lifts arise from these pseudo-adjunctions.]]></description>
      <pubDate>Wed, 17 Jun 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:30)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:30)2026</guid>
      <author>Slattery, Andrew</author>
      <author>Sterling, Jonathan</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Category Theory]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Slattery, Andrew</dc:creator>
      <dc:creator>Sterling, Jonathan</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Automating Boundary Filling in Cubical Type Theories</title>
      <description><![CDATA[When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical type theory provides computational support for HITs and univalence. A difficulty when working in cubical type theory is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries.  We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case-Kan solving is even undecidable-so we focus on heuristics that perform well on practical examples. Our language encompasses different variations of cubical type theory which differ in their "contortion theory", i.e., the class of contortions they support. We provide a solver for the contortion problem for the most complex contortion theories currently being researched, the Dedekind and De Morgan contortions, by utilizing a reformulation of contortions in terms of poset maps. We solve Kan problems using constraint satisfaction programming, which is applicable independently of the underlying contortion theory. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve many goals a user of cubical type theory might face. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks.]]></description>
      <pubDate>Mon, 15 Jun 2026 22:52:03 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:28)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:28)2026</guid>
      <author>Doré, Maximilian</author>
      <author>Cavallo, Evan</author>
      <author>Mörtberg, Anders</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Doré, Maximilian</dc:creator>
      <dc:creator>Cavallo, Evan</dc:creator>
      <dc:creator>Mörtberg, Anders</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Work-Efficient Query Evaluation in Constant Time with PRAMs</title>
      <description><![CDATA[The article studies query evaluation in parallel constant time in the CRCW PRAM model. While it is well-known that all relational algebra queries can be evaluated in constant time on an appropriate CRCW PRAM model, this article is interested in the efficiency of evaluation algorithms, that is, in the number of processors or, asymptotically equivalent, in the work. Naive evaluation in the parallel setting results in huge (polynomial) bounds on the work of such algorithms and in presentations of the result sets that can be extremely scattered in memory. The article discusses some obstacles for constant-time PRAM query evaluation. It presents algorithms for relational operators and explores three settings, in which efficient sequential query evaluation algorithms exist: acyclic queries, semijoin algebra queries, and join queries -- the latter in the worst-case optimal framework. Under mild assumptions -- that data values are numbers of polynomial size in the size of the database or that the relations of the database are suitably sorted -- constant-time algorithms are presented that are weakly work-efficient in the sense that work $\mathcal{O}(T^{1+\varepsilon})$ can be achieved, for every $\varepsilon>0$, compared to the time $T$ of an optimal sequential algorithm. Important tools are the algorithms for approximate prefix sums and compaction from Goldberg and Zwick (1995).]]></description>
      <pubDate>Fri, 12 Jun 2026 21:03:19 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:27)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:27)2026</guid>
      <author>Keppeler, Jens</author>
      <author>Schwentick, Thomas</author>
      <author>Spinrath, Christopher</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Databases]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Keppeler, Jens</dc:creator>
      <dc:creator>Schwentick, Thomas</dc:creator>
      <dc:creator>Spinrath, Christopher</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>First Order Logic on Pathwidth Revisited Again</title>
      <description><![CDATA[Courcelle's celebrated theorem states that all MSO-expressible properties can be decided in linear time on graphs of bounded treewidth. Unfortunately, the hidden constant implied by this theorem is a tower of exponentials whose height increases with each quantifier alternation in the formula. More devastatingly, this cannot be improved, under standard assumptions, even if we consider the much more restricted problem of deciding FO-expressible properties on trees.   In this paper we revisit this well-studied topic and identify a natural special case where the dependence of Courcelle's theorem can, in fact, be improved. Specifically, we show that all FO-expressible properties can be decided with an elementary dependence on the input formula, if the input graph has bounded pathwidth (rather than treewidth). This is a rare example of treewidth and pathwidth having different complexity behaviors. Our result is also in sharp contrast with MSO logic on graphs of bounded pathwidth, where it is known that the dependence has to be non-elementary, under standard assumptions. Our work builds upon, and generalizes, a corresponding meta-theorem by Gajarský and Hliněný for the more restricted class of graphs of bounded tree-depth.]]></description>
      <pubDate>Thu, 11 Jun 2026 18:24:17 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:26)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:26)2026</guid>
      <author>Lampis, Michael</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Data Structures and Algorithms]]></category>
      <category><![CDATA[Computational Complexity]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Lampis, Michael</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Univalent Enriched Categories and the Enriched Rezk Completion</title>
      <description><![CDATA[Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.]]></description>
      <pubDate>Tue, 02 Jun 2026 14:57:07 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:25)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:25)2026</guid>
      <author>van der Weide, Niels</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Category Theory]]></category>
      <dc:creator>van der Weide, Niels</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>An automata-based approach for synchronizable mailbox communication</title>
      <description><![CDATA[We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.]]></description>
      <pubDate>Wed, 27 May 2026 17:34:29 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:24)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:24)2026</guid>
      <author>Delpy, Romain</author>
      <author>Muscholl, Anca</author>
      <author>Sutre, Grégoire</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Formal Languages and Automata Theory]]></category>
      <dc:creator>Delpy, Romain</dc:creator>
      <dc:creator>Muscholl, Anca</dc:creator>
      <dc:creator>Sutre, Grégoire</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic</title>
      <description><![CDATA[Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.]]></description>
      <pubDate>Mon, 25 May 2026 11:43:07 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:22)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:22)2026</guid>
      <author>Ito, Sohei</author>
      <author>Tatsuta, Makoto</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Ito, Sohei</dc:creator>
      <dc:creator>Tatsuta, Makoto</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Extended Resolution Clause Learning via Dual Implication Points</title>
      <description><![CDATA[We present a new extended resolution clause learning (ERCL) algorithm, implemented as part of a conflict-driven clause-learning (CDCL) SAT solver, wherein new variables are dynamically introduced as definitions for {\it Dual Implication Points} (DIPs) in the implication graph constructed by the solver at runtime. DIPs are generalizations of unique implication points and can be informally viewed as a pair of dominator nodes, from the decision variable at the highest decision level to the conflict node, in an implication graph. We perform extensive experimental evaluation to establish the efficacy of our ERCL method, implemented as part of the MapleLCM SAT solver and dubbed xMapleLCM, against several leading solvers including the baseline MapleLCM, as well as CDCL solvers such as Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL, the winner of SAT Competition 2023. We show that xMapleLCM outperforms these solvers on Tseitin and XORified formulas. We further compare xMapleLCM with GlucoseER, a system that implements extended resolution in a different way, and provide a detailed comparative analysis of their performance.]]></description>
      <pubDate>Mon, 25 May 2026 11:41:42 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:23)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:23)2026</guid>
      <author>Buss, Sam</author>
      <author>Chung, Jonathan</author>
      <author>Ganesh, Vijay</author>
      <author>Oliveras, Albert</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Buss, Sam</dc:creator>
      <dc:creator>Chung, Jonathan</dc:creator>
      <dc:creator>Ganesh, Vijay</dc:creator>
      <dc:creator>Oliveras, Albert</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Epistemic Skills: Reasoning about Knowledge and Oblivion</title>
      <description><![CDATA[This paper presents a class of epistemic logics that captures the dynamics of acquiring knowledge and descending into oblivion, while incorporating concepts of group knowledge. The approach is grounded in a system of weighted models, introducing an ``epistemic skills'' metric to represent the epistemic capacities tied to knowledge updates. Within this framework, knowledge acquisition is modeled as a process of upskilling, whereas oblivion is represented as a consequence of downskilling. The framework further enables exploration of ``knowability'' and ``forgettability,'' defined as the potential to gain knowledge through upskilling and to lapse into oblivion through downskilling, respectively. Additionally, it supports a detailed analysis of the distinctions between epistemic de re and de dicto expressions. The computational complexity of the model checking and satisfiability problems is examined, offering insights into their theoretical foundations and practical implications.]]></description>
      <pubDate>Mon, 25 May 2026 11:39:31 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:21)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:21)2026</guid>
      <author>Liang, Xiaolong</author>
      <author>Wáng, Yì N.</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Artificial Intelligence]]></category>
      <category><![CDATA[Computational Complexity]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Liang, Xiaolong</dc:creator>
      <dc:creator>Wáng, Yì N.</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>A Resolution-Based Interactive Proof System for UNSAT</title>
      <description><![CDATA[Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless NP=coNP), and at recent SAT competitions the largest certificates of unsatisfiability are starting to reach terabyte size. This puts limits to the development of SAT-solving services in which a client with limited computational power sends a formula to a solver running on a powerful server, which returns a certificate to be checked by the client.   Recently, Couillard et al. have suggested to replace certificates with interactive proof systems based on the IP=PSPACE theorem. They have presented an interactive protocol between a prover and a verifier for an extension of QBF. The overall running time of the protocol is linear in the time needed by a standard BDD-based algorithm, and the time invested by the verifier is polynomial in the size of the formula. (So, in particular, the verifier never has to read or process exponentially long certificates). We call such an interactive protocol competitive with the BDD algorithm for solving QBF.   While BDD algorithms are state-of-the-art for certain classes of QBF instances, no modern (UN)SAT solver is based on BDDs. For this reason, we initiate the study of interactive certification for more practical SAT algorithms. In particular, we address the question whether interactive protocols can be competitive with some variant of resolution. We present two contributions. First, we prove a theorem that reduces the problem of finding competitive interactive protocols to finding an arithmetisation of formulas satisfying certain commutativity properties. (Arithmetisation is the fundamental technique underlying the IP=PSPACE theorem.) Then, we apply the theorem to give the first interactive protocol for the Davis-Putnam resolution procedure. We also report on an implementation and give some experimental results.]]></description>
      <pubDate>Fri, 22 May 2026 16:25:32 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:17)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:17)2026</guid>
      <author>Czerner, Philipp</author>
      <author>Esparza, Javier</author>
      <author>Krasotin, Valentin</author>
      <author>Krauss, Adrian</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[F.1.2; F.4.1]]></category>
      <dc:creator>Czerner, Philipp</dc:creator>
      <dc:creator>Esparza, Javier</dc:creator>
      <dc:creator>Krasotin, Valentin</dc:creator>
      <dc:creator>Krauss, Adrian</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems</title>
      <description><![CDATA[Finite-horizon probabilistic multiagent concurrent game systems, also known as finite multiplayer stochastic games, are a well-studied model in computer science due to their ability to represent a wide range of real-world scenarios involving strategic interactions among agents over a finite amount of iterations (given by the finite-horizon). The analysis of these games typically focuses on evaluating (verifying) and computing (synthesizing/realizing) which strategy profiles (functions that represent the behavior of each agent) qualify as equilibria. The two most prominent equilibrium concepts are the Nash equilibrium and the subgame perfect equilibrium, with the latter considered a conceptual refinement of the former. Computing these equilibria from scratch is, however, often computationally infeasible. Therefore, recent attention has shifted to the verification problem, where a given strategy profile must be evaluated to determine whether it satisfies equilibrium conditions. In this paper, we demonstrate that the verification problem for subgame perfect equilibria lies in PSPACE, while for Nash equilibria, it is EXPTIME-complete. This is a highly counterintuitive result since subgame perfect equilibria are often seen as a strict strengthening of Nash equilibria and are intuitively seen as more complicated.]]></description>
      <pubDate>Wed, 20 May 2026 22:36:43 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:19)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:19)2026</guid>
      <author>Rajasekaran, Senthil</author>
      <author>Vardi, Moshe Y.</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Computer Science and Game Theory]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Rajasekaran, Senthil</dc:creator>
      <dc:creator>Vardi, Moshe Y.</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms</title>
      <description><![CDATA[We report on recent advances in rule-based graph programming, which allow us to match the time complexity of some fundamental imperative graph algorithms. In general, achieving the time complexity of graph algorithms implemented in conventional languages using a rule-based graph-transformation language is challenging due to the cost of graph matching. Previous work demonstrated that with rooted rules, certain algorithms can be implemented in the graph programming language GP 2 such that their runtime matches the time complexity of imperative implementations. However, this required input graphs to have a bounded node degree and (for some algorithms) to be connected. In this paper, we overcome these limitations by enhancing the graph data structure generated by the GP 2 compiler and exploiting the new structure in programs. We present three case studies: the first program checks whether input graphs are connected, the second program checks whether input graphs are acyclic, and the third program solves the single-source shortest-paths problem for graphs with integer edge-weights. The first two programs run in linear time on (possibly disconnected) input graphs with arbitrary node degrees. The third program runs in time $O(nm)$ on arbitrary input graphs, matching the time complexity of imperative implementations of the Bellman-Ford algorithm. For each program, we formally prove its correctness and time complexity, and provide runtime experiments on various graph classes.]]></description>
      <pubDate>Wed, 20 May 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:20)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:20)2026</guid>
      <author>Alaoui, Ziad Ismaili</author>
      <author>Plump, Detlef</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Programming Languages]]></category>
      <category><![CDATA[Performance]]></category>
      <dc:creator>Alaoui, Ziad Ismaili</dc:creator>
      <dc:creator>Plump, Detlef</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Prover-Adversary games for systems over (non-deterministic) branching programs</title>
      <description><![CDATA[We introduce Pudlak-Buss style Prover-Adversary games to characterise proof systems reasoning over deterministic branching programs (BPs) and non-deterministic branching programs (NBPs). Our starting points are the proof systems eLDT and eLNDT, for BPs and NBPs respectively, previously introduced by Buss, Das and Knop. We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsenyi theorem that coNL = NL. Thanks to the techniques developed, we further obtain a proof complexity theoretic version of Immerman-Szelepcsenyi, showing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.]]></description>
      <pubDate>Wed, 20 May 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:18)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:18)2026</guid>
      <author>Das, Anupam</author>
      <author>Delkos, Avgerinos</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Computational Complexity]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Logic]]></category>
      <dc:creator>Das, Anupam</dc:creator>
      <dc:creator>Delkos, Avgerinos</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Deterministic Suffix-reading Automata</title>
      <description><![CDATA[We introduce deterministic suffix-reading automata (DSA), a new automaton model over finite words. Transitions in a DSA are labeled with words. From a state, a DSA triggers an outgoing transition on seeing a word ending with the transition's label. Therefore, rather than moving along an input word letter by letter, a DSA can jump along blocks of letters, with each block ending in a suitable suffix. This feature allows DSAs to recognize regular languages more concisely, compared to DFAs. In this work, we focus on questions around finding a minimal DSA for a regular language. In this context, the number of states is not a faithful measure of the size of a DSA, since the transition-labels contain strings of arbitrary length. Hence, we consider total-size (number of states + number of edges + total length of transition-labels) as the size measure of DSAs.   We start by formally defining the model and providing a DSA-to-DFA conversion that allows to compare the expressiveness and succinctness of DSA with related automata models. Our main technical contribution is a method to derive DSAs from a given DFA: a DFA-to-DSA conversion. We make a surprising observation that the smallest DSA derived from the canonical DFA of a regular language L need not be a minimal DSA for L. This observation leads to a fundamental bottleneck in deriving a minimal DSA for a regular language. In fact, we prove that given a DFA and a number k, the problem of deciding if there exists an equivalent DSA of total-size atmost k is NP-complete.]]></description>
      <pubDate>Thu, 07 May 2026 10:39:47 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:16)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:16)2026</guid>
      <author>Keerthan, R</author>
      <author>Srivathsan, B</author>
      <author>Venkatesh, R</author>
      <author>Verma, Sagar</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Formal Languages and Automata Theory]]></category>
      <category><![CDATA[68Q45]]></category>
      <category><![CDATA[F.1.1]]></category>
      <dc:creator>Keerthan, R</dc:creator>
      <dc:creator>Srivathsan, B</dc:creator>
      <dc:creator>Venkatesh, R</dc:creator>
      <dc:creator>Verma, Sagar</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>On $NP \cap coNP$ proof complexity generators</title>
      <description><![CDATA[Motivated by the theory of proof complexity generators we consider the following $Σ^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $π$ of a disjunction $\bigvee_i α_i$, no two $α_i$ having an atom in common, find $i$ such that $α_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$ is not solvable in the student-teacher model with a $p$-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies $NP \neq coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.]]></description>
      <pubDate>Wed, 06 May 2026 13:43:20 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:14)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:14)2026</guid>
      <author>Krajicek, Jan</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Computational Complexity]]></category>
      <category><![CDATA[Logic]]></category>
      <dc:creator>Krajicek, Jan</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent</title>
      <description><![CDATA[We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. Many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems. Going further, we compare and contrast these graph embedded systems with several notions and properties already known in the protocol analysis literature. Finally, we provide several combination results, both for the combination of multiple contracting convergent systems, and then for the combination of contracting convergent systems with particular permutative equational theories.]]></description>
      <pubDate>Wed, 06 May 2026 13:41:49 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:15)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:15)2026</guid>
      <author>Bunch, Carter</author>
      <author>Satterfield, Saraid Dwyer</author>
      <author>Erbatur, Serdar</author>
      <author>Marshall, Andrew M.</author>
      <author>Ringeissen, Christophe</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Bunch, Carter</dc:creator>
      <dc:creator>Satterfield, Saraid Dwyer</dc:creator>
      <dc:creator>Erbatur, Serdar</dc:creator>
      <dc:creator>Marshall, Andrew M.</dc:creator>
      <dc:creator>Ringeissen, Christophe</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Empirical Measures and Strong Laws of Large Numbers in Categorical Probability</title>
      <description><![CDATA[The Glivenko--Cantelli theorem is a uniform version of the strong law of large numbers. It states that for every IID sequence of random variables, the empirical measure converges to the underlying distribution (in the sense of uniform convergence of the CDF). In this work, we provide tools to study such limits of empirical measures in categorical probability. We propose two axioms, namely permutation invariance and empirical adequacy, that a morphism of type $X^{\mathbb{N}} \to X$ should satisfy to be interpretable as taking an infinite sequence as input and producing a sample from its empirical measure as output. Since not all sequences have a well-defined empirical measure, such \emph{empirical sampling morphisms} live in quasi-Markov categories, which, unlike Markov categories, allow for partial morphisms.  Given an empirical sampling morphism and a few other properties, we prove representability as well as abstract versions of the de Finetti theorem, the Glivenko--Cantelli theorem and the strong law of large numbers.  We provide several concrete constructions of empirical sampling morphisms as partially defined Markov kernels on standard Borel spaces. Instantiating our abstract results then recovers the standard Glivenko--Cantelli theorem and the strong law of large numbers for random variables with finite first moment. Our work thus provides a joint proof of these two theorems in conjunction with the de Finetti theorem from first principles.]]></description>
      <pubDate>Tue, 05 May 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:13)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:13)2026</guid>
      <author>Fritz, Tobias</author>
      <author>Gonda, Tomáš</author>
      <author>Lorenzin, Antonio</author>
      <author>Perrone, Paolo</author>
      <author>Mohammed, Areeb Shah</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Probability]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Category Theory]]></category>
      <category><![CDATA[Statistics Theory]]></category>
      <dc:creator>Fritz, Tobias</dc:creator>
      <dc:creator>Gonda, Tomáš</dc:creator>
      <dc:creator>Lorenzin, Antonio</dc:creator>
      <dc:creator>Perrone, Paolo</dc:creator>
      <dc:creator>Mohammed, Areeb Shah</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Pebble Games and Algebraic Proof Systems</title>
      <description><![CDATA[Analyzing refutations of the well known 0pebbling formulas Peb$(G)$ we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG $G$ with a single sink, if there is a Monomial Calculus refutation for Peb$(G)$ having simultaneously degree $s$ and size $t$ then there is a black pebbling strategy on $G$ with space $s$ and time $t+s$. Also if there is a black pebbling strategy for $G$ with space $s$ and time $t$ it is possible to extract from it a MC refutation for Peb$(G)$ having simultaneously degree $s$ and size $ts$. These results are analogous to those proven in {deRezende et al.21} for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC.  We also notice that for any directed acyclic graph $G$ the space needed in a pebbling strategy on $G$, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb$(G)$ in each of the algebraic proof systems NS, MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.]]></description>
      <pubDate>Fri, 01 May 2026 18:31:43 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:12)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:12)2026</guid>
      <author>Jaser, Lisa-Marie</author>
      <author>Toran, Jacobo</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Jaser, Lisa-Marie</dc:creator>
      <dc:creator>Toran, Jacobo</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata</title>
      <description><![CDATA[Ensuring the correctness of critical real-time systems, involving concurrent behaviours and timing requirements, is crucial. Timed automata extend finite-state automata with clocks, compared in guards and invariants with integer constants. Parametric timed automata (PTAs) extend timed automata with timing parameters. Parameter synthesis aims at computing dense sets of valuations for the timing parameters, guaranteeing a good behaviour. However, in most cases, the emptiness problem for reachability (i.e., the emptiness of the parameter valuations set for which some location is reachable) is undecidable for PTAs and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of symbolic sets of valuations containing not only all the integer points ensuring reachability, but also all the (non-necessarily integer) convex combinations of these integer points, for general PTAs with a bounded parameter domain. We also propose two further algorithms synthesizing parameter valuations guaranteeing unavoidability, and preservation of the untimed behaviour w.r.t. a reference parameter valuation, respectively. Our algorithms terminate and can output sets of valuations arbitrarily close to the complete result. We demonstrate their applicability and efficiency using the tools Roméo and IMITATOR on several benchmarks.]]></description>
      <pubDate>Wed, 29 Apr 2026 20:37:02 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:11)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:11)2026</guid>
      <author>André, Étienne</author>
      <author>Lime, Didier</author>
      <author>Roux, Olivier H.</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>André, Étienne</dc:creator>
      <dc:creator>Lime, Didier</dc:creator>
      <dc:creator>Roux, Olivier H.</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Positionality in $Σ_0^2$ and a completeness result</title>
      <description><![CDATA[We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in $Σ_0^2$ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Bchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023].   We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective $W$ which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective $W'$ which is equivalent to $W$ over finite game graphs and positional over arbitrary game graphs.]]></description>
      <pubDate>Wed, 29 Apr 2026 20:35:50 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:10)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:10)2026</guid>
      <author>Ohlmann, Pierre</author>
      <author>Skrzypczak, Michał</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Ohlmann, Pierre</dc:creator>
      <dc:creator>Skrzypczak, Michał</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Tighter Bounds for Query Answering with Guarded TGDs</title>
      <description><![CDATA[We consider the complexity of the open-world query answering problem, where we wish to determine certain answers to conjunctive queries over incomplete datasets specified by an initial set of facts and a set of guarded TGDs. This problem has been well-studied in the literature and is decidable but with a high complexity, namely, it is 2EXPTIME complete. Further, the complexity shrinks by one exponential when the arity is fixed.  We show in this paper how we can obtain better complexity bounds when considering separately the arity of the guard atom and that of the additional atoms, called the side signature. Our results make use of the technique of linearizing guarded TGDs, introduced in Gottlob, Manna, and Pieris. Specifically, we present a variant of the linearization process, making use of a restricted version of the chase that we recently introduced. Our results imply that open-world query answering with guarded TGDs can be solved in EXPTIME with arbitrary-arity guard relations if we simply bound the arity of the side signature; and that the complexity drops to NP if we fix the side signature and bound the width of the dependencies.]]></description>
      <pubDate>Tue, 21 Apr 2026 21:01:56 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:8)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:8)2026</guid>
      <author>Amarilli, Antoine</author>
      <author>Benedikt, Michael</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Amarilli, Antoine</dc:creator>
      <dc:creator>Benedikt, Michael</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Direct Access for Answers to Conjunctive Queries with Aggregation</title>
      <description><![CDATA[We study the fine-grained complexity of conjunctive queries with grouping and aggregation. For common aggregate functions (e.g., min, max, count, sum), such a query can be phrased as an ordinary conjunctive query over a database annotated with a suitable commutative semiring. We investigate the ability to evaluate such queries by constructing in loglinear time a data structure that provides logarithmic-time direct access to the answers ordered by a given lexicographic order. This task is nontrivial since the number of answers might be larger than loglinear in the size of the input, so the data structure needs to provide a compact representation of the space of answers. In the absence of aggregation and annotation, past research established a sufficient tractability condition on queries and orders. For queries without self-joins, this condition is not just sufficient, but also necessary (under conventional lower-bound assumptions in fine-grained complexity).  We show that all past results continue to hold for annotated databases, assuming that the annotation itself does not participate in the lexicographic order. Yet, past algorithms do not apply to the count-distinct aggregation, which has no efficient representation as a commutative semiring; for this aggregation, we establish the corresponding tractability condition. We then show how the complexity of the problem changes when we include the aggregate and annotation value in the order. We also study the impact of having all relations but one annotated by the multiplicative identity (one), as happens when we translate aggregate queries into semiring annotations, and having a semiring with an idempotent addition, such as the case of min, max, and count-distinct over a logarithmic-size domain.]]></description>
      <pubDate>Tue, 21 Apr 2026 21:00:43 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:9)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:9)2026</guid>
      <author>Eldar, Idan</author>
      <author>Carmeli, Nofar</author>
      <author>Kimelfeld, Benny</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Databases]]></category>
      <category><![CDATA[Data Structures and Algorithms]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Eldar, Idan</dc:creator>
      <dc:creator>Carmeli, Nofar</dc:creator>
      <dc:creator>Kimelfeld, Benny</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>A Scalable Game-Theoretic Approach for Selecting Security Controls from Standardized Catalogues</title>
      <description><![CDATA[Selecting the combination of security controls that will most effectively protect a system's assets is a difficult task. If the wrong controls are selected, the system may be left vulnerable to cyber-attacks that can impact the confidentiality, integrity, and availability of critical data and services. In practical settings, as standardized control catalogues can be quite large, it is not possible to select and implement every control possible. Instead, considerations, such as budget, effectiveness, and dependencies among various controls, must be considered to choose a combination of security controls that best achieve a set of system security objectives. In this paper, we present a game-theoretic approach for selecting effective combinations of security controls based on expected attacker profiles and a set budget. The control selection problem is set up as a two-person zero-sum one-shot game. Valid control combinations for selection are generated using an algebraic formalism to account for dependencies among selected controls. Using a software tool, we apply the approach on a fictional Canadian military system with Canada's standardized control catalogue, ITSG-33. Through this case study, we demonstrate the approach's scalability to assist in selecting an effective set of security controls for large systems. The results illustrate how a security analyst can use the proposed approach and supporting tool to guide and support decision-making in the control selection activity when developing secure systems of all sizes.]]></description>
      <pubDate>Sat, 18 Apr 2026 07:55:42 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:7)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:7)2026</guid>
      <author>Léveillé, Dylan</author>
      <author>Jaskolka, Jason</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Software Engineering]]></category>
      <dc:creator>Léveillé, Dylan</dc:creator>
      <dc:creator>Jaskolka, Jason</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity</title>
      <description><![CDATA[A central computational task in database theory, finite model theory, and computer science at large is the evaluation of a first-order sentence on a finite structure. In the context of this task, the \emph{width} of a sentence, defined as the maximum number of free variables over all subformulas, has been established as a crucial measure, where minimizing width of a sentence (while retaining logical equivalence) is considered highly desirable. An undecidability result rules out the possibility of an algorithm that, given a first-order sentence, returns a logically equivalent sentence of minimum width; this result motivates the study of width minimization via syntactic rewriting rules, which is this article's focus. For a number of common rewriting rules (which are known to preserve logical equivalence), including rules that allow for the movement of quantifiers, we present an algorithm that, given a positive first-order sentence $ϕ$, outputs the minimum-width sentence obtainable from $ϕ$ via application of these rules. We thus obtain a complete algorithmic understanding of width minimization up to the studied rules; this result is the first one -- of which we are aware -- that establishes this type of understanding in such a general setting. Our result builds on the theory of term rewriting and establishes an interface among this theory, query evaluation, and structural decomposition theory.]]></description>
      <pubDate>Sat, 18 Apr 2026 07:54:54 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:6)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:6)2026</guid>
      <author>Chen, Hubie</author>
      <author>Mengel, Stefan</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Databases]]></category>
      <dc:creator>Chen, Hubie</dc:creator>
      <dc:creator>Mengel, Stefan</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Expressivity of AuDaLa: Turing Completeness and Possible Extensions</title>
      <description><![CDATA[AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously. Considering the paradigm and the design choices of AuDaLa, it is interesting to determine the expressivity of the language. In this paper, we implement Turing machines in AuDaLa and prove that implementation correct. This proves that AuDaLa is Turing complete, giving an initial indication of AuDaLa's expressivity. Additionally, we give examples of how to add extensions to AuDaLa to increase its practical expressivity and to better match conventional parallel languages, allowing for a more straightforward and performant implementation of algorithms.]]></description>
      <pubDate>Thu, 16 Apr 2026 18:00:51 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:5)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:5)2026</guid>
      <author>Franken, Tom T. P.</author>
      <author>Neele, Thomas</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Programming Languages]]></category>
      <dc:creator>Franken, Tom T. P.</dc:creator>
      <dc:creator>Neele, Thomas</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Quantitative Verification with Neural Networks</title>
      <description><![CDATA[We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tight and sound bounds for the probability that a stochastic process hits a target condition within finite time. This problem subsumes a variety of quantitative verification questions, from the reachability and safety analysis of discrete-time stochastic dynamical models, to the study of assertion-violation and termination analysis of probabilistic programs. We rely on neural networks to represent supermartingale certificates that yield such probability bounds, which we compute using a counterexample-guided inductive synthesis loop: we train the neural certificate while tightening the probability bound over samples of the state space using stochastic optimisation, and then we formally check the certificate's validity over every possible state using satisfiability modulo theories; if we receive a counterexample, we add it to our set of samples and repeat the loop until validity is confirmed. We demonstrate on a diverse set of benchmarks that, thanks to the expressive power of neural networks, our method yields smaller or comparable probability bounds than existing symbolic methods in all cases, and that our approach succeeds on models that are entirely beyond the reach of such alternative techniques.]]></description>
      <pubDate>Wed, 15 Apr 2026 10:33:12 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:4)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:4)2026</guid>
      <author>Abate, Alessandro</author>
      <author>Edwards, Alec</author>
      <author>Giacobbe, Mirco</author>
      <author>Punchihewa, Hashan</author>
      <author>Roy, Diptarko</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[Programming Languages]]></category>
      <category><![CDATA[Systems and Control]]></category>
      <category><![CDATA[F.3.1; D.2.4]]></category>
      <dc:creator>Abate, Alessandro</dc:creator>
      <dc:creator>Edwards, Alec</dc:creator>
      <dc:creator>Giacobbe, Mirco</dc:creator>
      <dc:creator>Punchihewa, Hashan</dc:creator>
      <dc:creator>Roy, Diptarko</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>One is all you need: Second-order Unification without First-order Variables</title>
      <description><![CDATA[We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable is allowed, and (ii) first-order variables do not occur. We study an equational variant of SOGU where the signature contains \textit{associative} binary function symbols (ASOGU) and show that Hilbert's 10$^{th}$ problem is reducible to ASOGU unifiability, thus proving undecidability. Our reduction provides a new lower bound for the undecidability of second-order unification, as previous results required first-order variable occurrences, multiple second-order variables, and/or equational theories involving \textit{length-reducing} rewrite systems. Furthermore, our reduction holds even in the case when associativity of the binary function symbol is restricted to \emph{power associative}, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a single constant.]]></description>
      <pubDate>Thu, 09 Apr 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:3)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:3)2026</guid>
      <author>Cerna, David M.</author>
      <author>Parsert, Julian</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Cerna, David M.</dc:creator>
      <dc:creator>Parsert, Julian</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Prime Factorization in Models of PV$_1$</title>
      <description><![CDATA[Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two $n$-bit primes, we show that the bounded arithmetic theory $\text{PV}_1$, even when augmented by the sharply bounded choice scheme $BB(Σ^b_0)$, cannot prove that every number has some prime divisor. By the completeness theorem, it follows that under this assumption there is a model $M$ of $\text{PV}_1$ that contains a nonstandard number $m$ which has no prime factorization.]]></description>
      <pubDate>Tue, 07 Apr 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:1)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:1)2026</guid>
      <author>Ježil, Ondřej</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Ježil, Ondřej</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Machine Space I: Weak exponentials and quantification over compact spaces</title>
      <description><![CDATA[Topology may be interpreted as the study of verifiability, where opens correspond to semi-decidable properties. In this paper we make a distinction between verifiable properties themselves and processes which carry out the verification procedure. The former are simply opens, while we call the latter \emph{machines}. Given a frame presentation $\mathcal{O} X = \langle G \mid R\rangle$ we construct a space of machines $Σ^{Σ^G}$ whose points are given by formal combinations of basic machines corresponding to generators in $G$. This comes equipped with an `evaluation' map making it a weak exponential with base $Σ$ and exponent $X$. When it exists, the true exponential $Σ^X$ occurs as a retract of machine space. We argue this helps explain why some spaces are exponentiable and others not. We then use machine space to study compactness by giving a purely topological version of Escardó's algorithm for universal quantification over compact spaces in finite time. Finally, we relate our study of machine space to domain theory and domain embeddings.]]></description>
      <pubDate>Tue, 07 Apr 2026 00:00:00 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(2:2)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(2:2)2026</guid>
      <author>Faul, Peter F.</author>
      <author>Manuell, Graham</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[General Topology]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <dc:creator>Faul, Peter F.</dc:creator>
      <dc:creator>Manuell, Graham</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
    <item>
      <title>Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion</title>
      <description><![CDATA[The synthesis of reactive systems aims for the automated construction of strategies for systems that interact with their environment. Whereas the synthesis approach has the potential to change the development of reactive systems significantly due to the avoidance of manual implementation, it still suffers from a lack of efficient synthesis algorithms for many application scenarios. The translation of the system specification into an automaton that allows for strategy construction (if a winning strategy exists) is nonelementary in the length of the specification in S1S and doubly exponential for LTL, raising the need of highly specialized algorithms. In this article, we present an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotonicity property of specifications. For this, we introduce window counting constraints that allow for step-wise refinement or abstraction of specifications. In an iterative synthesis procedure, those window counting constraints are used to construct automata representing over- or under-approximations (depending on the counting constraint) of constraint-compliant behavior. Analysis results on winning regions of previous iterations are used to reduce the size of the next automaton, leading to an overall reduction of the state space explosion extent. We present the implementation results of the iterated synthesis for a zero-sum game setting as proof of concept. Furthermore, we discuss the current limitations of the approach in a zero-sum setting and sketch future work in non-zero-sum settings.]]></description>
      <pubDate>Tue, 31 Mar 2026 11:55:54 +0000</pubDate>
      <link>https://doi.org/10.46298/lmcs-22(1:29)2026</link>
      <guid>https://doi.org/10.46298/lmcs-22(1:29)2026</guid>
      <author>Feeken, Linda</author>
      <author>Fränzle, Martin</author>
      <category><![CDATA[Logical Methods in Computer Science]]></category>
      <category><![CDATA[Logic in Computer Science]]></category>
      <category><![CDATA[93B50]]></category>
      <dc:creator>Feeken, Linda</dc:creator>
      <dc:creator>Fränzle, Martin</dc:creator>
      <slash:comments>0</slash:comments>
    </item>
  </channel>
</rss>
