Searcharxiv⌕ Search

subject

cs.LO

cs.LO: explore 40 source-linked works published from 2026 to 2026, with original documents and citations.

This collection is a preview while coverage and quality are evaluated.

Search within this collection

Coverage and selection

Includes records with this source-supplied label or an explicit phrase match in their metadata. Matches indicate a mention, not proof that a paper uses a method or tests a material. Source versions are consolidated by DOI.

Sources: arxiv. Collection updated 2026-09-14. Counts describe this index, not the complete source archives.

arXiv2026

Redundancy rules for MaxSAT

The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et$.$al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et$.$al'22, Berg et$.$al'23, Bonacina et$.$al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et$.$al'22]. Moreover, they are simpler and weaker than [Berg et$.$al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et$.$al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $PHP^{m}_{n}$ falsifies at least $m-n$ clauses. We conclude by discussing the integration of our rules with the MaxSAT resolution proof system, which is a commonly studied proof system for MaxSAT.

cs.LO↗
arXiv2026

The Price of Remembering: A Calibrated Energy Law for Computation

Where does a computer's energy go? Mostly into keeping, not into computing. A bit held in fast storage draws power for every second it stays there, and it costs energy again each time it moves between storage levels. We call the first cost \emph{rent} and the second \emph{fare}, and we state one law: the energy of a computation is at least its operations, plus rent on every live bit for as long as it lives, plus fare on every bit moved. The model under the law prices control as well as data. There is no free clock, and any unpriced register would make the theorems false. One lemma does most of the work: every use of a value is paid for by rent, by fare, or by computing the value again. Three things follow. Exact attention brings every past token back for every new one, so its energy grows with the square of the context length, while a recurrent model with a fixed state grows linearly. The square is a theorem for machines that never re-read past tokens. Under a stated serving hypothesis it is the fare on every past token, which passes the model's own arithmetic near ten thousand tokens, the point where long-context serving becomes bandwidth-bound today. Known bounds on memory over time become joule floors: on any sequential machine with volatile working storage, sorting $n$ items pays rent proportional to $n^2/\log n$ bit-steps on most inputs, and the bound for scrypt makes every password guess cost joules that no amount of parallel hardware reduces.

cs.PF↗
arXiv2026

Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support

We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping Theorem (OST) in the form of a specific precondition. This precondition requires the existence of an integrable dominating function for the martingale expression, which implies uniform integrability; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the runtime of a linear loop, then we can automatically synthesise polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to have unbounded support, which is a novel contribution to the field.

cs.LO↗
arXiv2026

Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking

Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a particularly important technique. However, there is a well-known scalability issue due to state-space explosion, especially when verifying complex properties. To mitigate this issue, we propose specification-guided path shortcutting for probabilistic systems, focusing on Markov chains (MCs) and $ω$-regular properties. The key idea is that, when the verified property is fixed, certain sequences of transitions in an MC can be replaced with a single transition without changing the satisfaction probability, and thus, we can reduce the state space of the MC. We implement the proposed path shortcutting and evaluate its contribution to the performance of probabilistic model checking, using Storm as the baseline model checker. The results suggest that our approach often outperforms the baseline, particularly on benchmark instances with complex specifications.

cs.LO↗
arXiv2026

Collatz conjecture becomes theorem

The Collatz hypothesis is a theorem of the algorithmic theory of natural numbers. We prove the (algorithmic) formula that expresses the halting property of Collatz algorithm. The observation that Collatz's theorem cannot be proved in any elementary number theory completes the main result.

math.GM↗
arXiv2026

Categorical algebra of conditional probability

In the field of categorical probability, one uses concepts and techniques from category theory, such as monads and monoidal categories, to study the structures of probability and statistics. In this paper, we connect some ideas from categorical algebra, namely weakly cartesian functors and natural transformations, to the idea of conditioning in probability theory, using Markov categories and probability monads. First of all, we show that under some conditions, the monad associated to a Markov category with conditionals has a weakly cartesian functor and weakly cartesian multiplication. In particular, we show that this is the case for the Giry monad on standard Borel spaces. We then connect this theory to existing results on statistical experiments. We show that for deterministic statistical experiments, the so-called standard measure construction (which can be seen as a generalization of the ``hypernormalizations'' introduced by Jacobs) satisfies a universal property, allowing an equivalent definition which does not rely on the existence of conditionals.

math.CT↗
arXiv2026

Quantified propositional calculi and narrow implicit proofs

In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.

cs.LO↗
arXiv2026

Factorized Boolean representations for efficient quantum synthesis

Quantum algorithms promise advantages beyond classical reach, but running them on error-corrected hardware requires translating Boolean specifications into reversible circuits, and the resources that translation demands determine what is executable. Established methods minimize a Boolean expression and map it to a circuit, assuming the minimized form is best. Here we show that minimized expressions retain algebraic structure minimization cannot reach, arising from containment and complementary-polarity relationships among their terms, and that extracting it yields circuits cheaper to execute despite having more operations. The decisive quantity is not a circuit's operation count but the control count of its widest operation, a superlinear cost; extracting shared factors trades a few wide operations for many narrow ones and reduces qubit count. Across benchmarks and oracles from quantum search and factoring algorithms, at the representation level the transformation never increases either cost measure, a guarantee from its construction. Translation to an executable circuit returns part of that advantage, since auxiliary lines must be uncomputed, yet the factorized circuit still left a leading circuit-level optimizer reaching lower final counts, and faster, than unaided. The representation of a computation is therefore itself a resource, optimizable before compilation and distinct from both logic minimization and circuit-level optimization.

quant-ph↗
arXiv2026

Modalities in non-classical variations of $\mathsf{S4}$

A classical result in modal logic states that $\mathsf{S4}$ has $14$ modalities, that is, every sequence of negations, boxes, and diamonds is equivalent to one in a set of $14$ such sequences. We study analogous results for the non-classical analogues $\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{GS4}$, and $\mathsf{GS4^c}$ of $\mathsf{S4}$. First, we show that, while all these logics have finitely many $\{\Box,\Diamond\}$- and $\{\neg,\Box\}$-modalities, the logic $\mathsf{CS4}$ has infinitely many $\{\neg,\Diamond\}$-modalities. Second, we show that $\mathsf{IS4}$ and $\mathsf{GS4}$ have finitely many $\{\neg,\Diamond\}$-modalities, but they have infinitely many $\{\neg,\Box,\Diamond\}$-modalities. At last, we show that $\mathsf{GS4^c}$ has finitely many $\{\neg,\Box,\Diamond\}$-modalities.

math.LO↗
arXiv2026

On Synthesis of Metric Interval Temporal Logics

Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle \emph{precise} passive learning for an expressive timed logic, \emph{Metric Interval Temporal Logic} (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.

cs.LO↗
arXiv2026

On Good-for-MDPs Automata

Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games (GFG) automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof. We also compare the succinctness of GFM automata with other types of automata with restricted nondeterminism. The first natural comparison point are GFG automata. Deterministic automata are GFG, and GFG automata are GFM, but not vice versa. This raises the question of how these classes relate in terms of succinctness. GFG automata are known to be exponentially more succinct than deterministic automata, but the gap between GFM and GFG automata as well as the gap between ordinary nondeterministic automata and those that are GFM have been open. We establish that these gaps are exponential, and sharpen this result by showing that the latter gap remains exponential when restricting the nondeterministic automata to separating safety or unambiguous reachability automata.

cs.FL↗
arXiv2026

A categorical formulation of Kraus' paradox

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT↗
arXiv2026

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

This paper investigates $\exists\mathbb{R}(r^{\mathbb{Z}})$, that is the extension of the existential theory of the reals by an additional unary predicate $r^{\mathbb{Z}}$ for the integer powers of a fixed computable real number $r > 0$. If all we have access to is a Turing machine computing $r$, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. $r$ is known to be transcendental, or 2. $r$ is a root of some given integer polynomial (that is, $r$ is algebraic). In other words, knowing the algebraicity of $r$ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that $r$ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of $\exists\mathbb{R}(r^{\mathbb{Z}})$ is 1. in NEXPTIME if $r$ is a natural number, 2. in EXPSPACE if $r$ is an algebraic number, and 3. in 3EXP if $r$ belongs to a family of transcendental numbers including $π$ and Euler's $e$. As a by-product of our results, we are able to remove the appeal to Schanuel's conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler's $e$ and the aversion factor is a fixed algebraic number, the problem is in EXP.

cs.LO↗
arXiv2026

Proof-Carrying Analytic Approximation: Local-to-Global Evidence Transport at Encoding Cost

Under quasi-uniform refinement, bounded local-encoding hypotheses, and local $W^{r,2}$ approximation of order $r\ge 2$ in a rational piecewise-polynomial presentation of $W^{1,2}(0,1)$, carrying the complete proof genealogy up to the level required by an accuracy $\varepsilon$ costs the same asymptotic bit order as the finest-level conventional coefficient encoding. If $B_n=Θ(M_nβ_n)$ denotes that level-$n$ encoding size, our compiler transports supplied local approximation and overlap witnesses through exact partition-of-unity synthesis and geometric refinement to a represented limit with total certificate size $O(B_{m(\varepsilon)})$, where $m(\varepsilon)=O(\log(1/\varepsilon)/(r-1))$. The construction makes no oracle query to an independently supplied semantic target name ($Q_{\rm target}=0$). When $β_n=O(n+1)$, this becomes $O(\varepsilon^{-1/(r-1)}(1+\log(1/\varepsilon)))$. The surrounding framework is intentionally separated from this resource theorem. Every real computable Banach presentation admits a uniformly computable linear isometric embedding into standard computable $C([0,1])$, with computable inverse on its represented range. Complete metric evidence with rational strict slack collapses extensionally to the represented analytic metric once effective names are available, while chosen evidence transformations retain construction history and resource information. For the Lipschitz grammar used here, qualitative evidence-local lifting is canonical; the nontrivial question is therefore which evidence is retained and at what cost.

math.FA↗
arXiv2026

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.

cs.PL↗
arXiv2026

Essential Unitarity for Higher-Order Quantum Computation

We develop a boundary-centric semantic framework for higher-order quantum computation, building on the Kelly-Laplaza description of compact closure and Abramsky's execution account. In the semantic carrier Perm(C), morphisms are complex-linear combinations of polarized boundary linkings, composed by execution. Finite-family addresses provide coherent control over finite-level quantum registers (qudits) while retaining the multiplicative boundary structure. We identify essential unitarity, a boundary condition extending ordinary unitarity to higher-order interfaces. On positive qudit registers it coincides with ordinary matrix unitarity; at higher order it expresses preservation of information across the full polarized boundary. We define a unit-free coherent quantum core generated by multiplicative wiring, unitary gates on positive qudit registers, and contextual coherent control, and prove that every one of its morphisms is essentially unitary. The framework realizes an applied coherent quantum switch and the unitary stages of equal-ratio one-slot supermap dilations with explicit memory. An extended abstract of this work was accepted for QPL 2026 and is forthcoming in its proceedings.

quant-ph↗
arXiv2026

A homotopy-type-theoretic generalization of neurosymbolic inference

A wide range of neurosymbolic (NeSy) systems compute one functional: a belief-weighted sum of a logical quantity over a space of $σ$-structures, of which weighted model counting, fuzzy logic, and probabilistic logic are special cases. This account is built on sets, and a set deliberately forgets two things that are important for NeSy: when two $σ$-structures are the same up to a symmetry of the theory, and how many distinct proofs witness a query. Types, in the sense of homotopy type theory, preserve this information and turn the functional into a belief-weighted homotopy cardinality, a notion of size that counts each object in inverse proportion to its symmetries. We develop the framework from scratch for NeSy systems, prove a conservativity theorem that recovers the classical functional when symmetries are trivial, and show that the symmetry our framework exposes is exactly the one behind reasoning shortcuts. The payoff is concrete: the shortcut-aware concept posterior that recent methods reach by ensembling or expressive density estimation is the only symmetry-invariant point of the confusion-set simplex, computable in closed form by averaging a single model over the symmetry group. On MNIST reasoning-shortcut benchmarks this single-model wrapper is better calibrated than a diversity-trained ensemble, while leaving label accuracy and identifiable concepts untouched. Code is freely available at https://github.com/bio-ontology-research-group/hott-nesy.

cs.AI↗
arXiv2026

Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked. To realize this possibility, we introduce Prove2Me (https://prove2.me), an open collaborative platform for formalizing mathematics. Users launch formalization "missions", to which AI agents contribute formal proofs toward completion. We designed mechanisms and a specialized harness in Prove2Me that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results. In doing so, Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent.

cs.AI↗
Compare source metadata on this page
WorkPublishedSource identifierSource
Redundancy rules for MaxSAT2026-09-022511.14657arxiv
The Price of Remembering: A Calibrated Energy Law for Computation2026-09-022609.00744arxiv
Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support2026-09-022609.02446arxiv
Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking2026-09-022609.02457arxiv
Collatz conjecture becomes theorem2026-09-012310.13035arxiv
Categorical algebra of conditional probability2026-09-012502.14941arxiv
Quantified propositional calculi and narrow implicit proofs2026-09-012606.10535arxiv
Factorized Boolean representations for efficient quantum synthesis2026-09-012608.27430arxiv
Modalities in non-classical variations of $\mathsf{S4}$2026-09-012609.00736arxiv
On Synthesis of Metric Interval Temporal Logics2026-09-012609.01032arxiv
On Good-for-MDPs Automata2026-08-312202.07629arxiv
A categorical formulation of Kraus' paradox2026-08-312403.17961arxiv
On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number2026-08-312502.02220arxiv
Proof-Carrying Analytic Approximation: Local-to-Global Evidence Transport at Encoding Cost2026-08-312506.22693arxiv
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT2026-08-312601.09986arxiv
Essential Unitarity for Higher-Order Quantum Computation2026-08-312606.04080arxiv
A homotopy-type-theoretic generalization of neurosymbolic inference2026-08-312606.17851arxiv
Prove2Me: An Open Collaborative Platform for Scaling Math Formalization2026-08-312608.28433arxiv

These are bibliographic comparisons, not experimental rankings. Follow the original document for methods and conditions.