arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

New this week

New in cs.LO Logic in Computer Science

40 papers in cs.LO from 6 November to 12 November 2026.

Includes papers cross-listed here; the counts on the field chips are by primary category.

More fields

Whole archives

showing 1–25 of 40, newest first RSS

Graded Intersection Types

Rémy Cerda, Ugo Dal Lago

cs.LO · · cited 0× · arXiv ↗ · more like this ·

We introduce graded intersection types, in which arrow domains are multisets of types with coefficients in a semiring. Boolean and natural number grades recover idempotent and non-idempotent intersection types. We give algebraic conditions on the semiring for subject reduction and expansion in finite systems and in locally finite systems with guarded infinite types. We construct a lifting to multisets of grades corresponding, in this general setting, to lifting the idempotent system to the non-idempotent one. We recall the main existing operational characterisations from the literature, and show some general extensions.

Mathematical foundations for symmetric programming and reasoning

Ohad Kammar, Matija Pretnar

cs.PL · · cited 0× · arXiv ↗ · more like this ·

We develop a mathematical abstraction for uniformly exploiting symmetries in programming and reasoning based on the mathematical proof principle `without-loss-of-generality' (w.l.o.g.). Given: group actions that describe symmetries of the input and the output; and a canoniser, which captures how arbitrary inputs get sent to canonical ones, our construction extends any function from the canonical inputs to the whole domain. We characterise the conditions on the canonisers which guarantee that the construction gives the unique equivariant (i.e. symmetry-preserving) extension. Furthermore, we adapt the construction to a dependently-typed setting, where it captures traditional symmetric w.l.o.g. arguments via the Curry-Howard correspondence. Finally, we extend the construction to algebraic data types, where the symmetries of the constructors both uniquely determine the symmetries of the…

Strategic disclosure and epistemic manipulation in extensive games

Sergei Artemov, Benjamin Prud'homme

cs.LO · · cited 0× · arXiv ↗ · more like this ·

In many strategic settings, agents can influence opponents by selectively disclosing truthful information about their own future actions. We introduce a game-theoretic framework to model this phenomenon. As a case study, we consider a two-player, alternating-move epistemic game in which Player A evaluates actions under a conservative maximin rule, while Player B-the manipulator-leverages this behavior by strategically revealing commitments. We prove that the manipulator can implement every inducible outcome using at most n disclosures in a binary game of depth 2n with n decisions per player. This establishes a sharp contrast between the game tree's exponential size and the linear amount of information required to control the outcome, highlighting a general mechanism by which limited information can exert disproportionate strategic influence.

LLM-Assisted Verification in Dafny

Wieger Wesselink, Kees Huizing, Huub van de Wetering

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Formal verification of complex algorithms requires expertise in program specification, invariant construction, mathematical proof, and the management of automated theorem provers. Although large language models (LLMs) can generate program code and proof fragments, reliably developing complete machine-checked verifications remains challenging: it requires an iterative process of constructing and validating specifications and invariants, building proofs, diagnosing solver failures, and optimizing verification performance. This paper presents a systematic ten-step workflow for LLM-assisted verification of scientific algorithms using the Dafny verification system. The workflow integrates algorithm formalization, contract development, empirical invariant validation, proof construction, bottleneck profiling, and resource-driven proof optimization. We applied the workflow using Antrhopic's…

Selective Chaining of Parameterised Boolean Equation Systems

Jore J. Booy, Tim A. C. Willemse

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Parameterised Boolean Equations Systems (PBESs) are used to verify properties of formal industrial models. We introduce a technique called selective chaining to simplify these PBESs by unfolding specific predicate variable instances when the unfolding results in a PBES that is likely to be simpler. For determining the latter we propose a set of heuristics. We show the formal correctness of the chaining operator and provide theoretical upper bounds using relevancy graphs on the size of the verification problem after chaining. Lastly, we study the effectiveness of our heuristics, showing that selective chaining can reduce memory usage and yield significant speed-ups solving PBESs that encode model checking problems for complex industrial systems.

Propositional Dynamic Logic without tests does not have Craig Interpolation

Malvin Gattinger

cs.LO · · cited 0× · arXiv ↗ · more like this ·

It was shown recently by Borzechowski et al. (2026) that Propositional Dynamic Logic (PDL) has Craig Interpolation. Whether test-free PDL, i.e. PDL without the `?' operator, has interpolation remained open. Here we answer this question in the negative with a counterexample: a test-free PDL validity for which no test-free interpolant exists. The validity only uses one atomic program and the Kleene star, so it implies that the basic modal logic K extended with the reflexive transitive closure does not have interpolation, as previously shown by Studer (2009). The example was originally obtained using LLMs and Lean. We describe our methodology and provide links to all prompts, LLM output summaries as well as the Lean proof.

Tracking relevance syntactically: A nested approach to weak relevant logic

Fabio De Martin Polo, Han Gao

cs.LO · · cited 0× · arXiv ↗ · more like this ·

The variable-sharing property (VSP) is regarded as a key feature of relevant logics, while the Craig interpolation property (CIP), formulated with respect to relevant implication, implies the VSP in constant-free propositional languages. However, to the best of our knowledge, no constant-free distributive relevant logic has previously been shown to enjoy the CIP. This absence of positive results has contributed to a widespread impression among relevant logicians that relevance and Craig interpolation are incompatible. In this work, we address this tension by proving that the negation-free fragment of base relevant logic B, denoted B+, enjoys both properties. Our proof is purely syntactic and is based on a novel nested sequent calculus featuring binary relevant blocks as primitive structural constructs. Unlike conventional nested sequent calculi, where unary nesting reflects the binary…

Sound Automatic Lock Placement for Concurrent Programs with Pointers

Nicolas Waldburger, Florian Faissole, Ryo Okabe +1 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

We propose a lightweight method for automatic lock placement in concurrent POSIX programs with explicit pointer manipulation, such as C programs. Given a program that lacks sufficient user-placed mutexes, or contains none at all, our method introduces new mutexes to prevent data races. The method is formally proven to guarantee the absence of data races and mainly consists of three steps. The first step performs lockset analysis and may-happen-in-parallel analysis. The second step conducts a concurrent points-to analysis derived from a Steensgaard-like procedural analysis, where per-thread points-to graphs are unified using a special completion rule. The final step places locks to prevent data races while respecting a lock ordering to avoid deadlocks. In addition, user-annotated critical sections are protected through insertion of dedicated locks. Since lock placement is a complex and…

Strong Lyndon Interpolation for Multi-Modal Logics with Converses: A Constructive Approach with Tree Sequents

Tim S. Lyon

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Grammar logics with converses are multi-modal logics that generalize tense logics and whose frame conditions are determined by context-free production rules. We study the strong Lyndon interpolation property (strong LIP) for these logics, which requires interpolants to respect both the polarities of propositional atoms and the indices of modalities. We show that the strong LIP properly strengthens the Lyndon interpolation property over grammar logics, since it fails for certain grammar logics with bridge axioms, i.e., path axioms relating modalities with distinct indices. We then prove that every bridge-free grammar logic, possibly extended with seriality axioms, has the strong LIP. This class includes the multi-modal tense logics obtained by imposing any combination of seriality, reflexivity, transitivity, symmetry, and Euclideanity on each pair of converse modalities. Our proof is…

The Tiglath Pileser principle and models of persuasion

Willem Conradie, Krishna Manoorkar, Alessandra Palmigiano +2 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

This paper develops a formal framework for analysing how agents extract reliable information from narratives and communicative interactions involving strategic deception. Building on Rubinstein and Glazer's models of persuasion, we introduce Tiglath-Pileser relations, a generalization of codex-based guidance relations, to formalize Baruch Halpern's Tiglath-Pileser principle: despite systematic bias, reported claims must retain a connection to the truth. We analyse these relations set-theoretically and axiomatically, identifying conditions for their successful application in persuasion. Our dynamic approach examines how such relations are formed, revised, and strategically manipulated, extending existing models beyond one-shot interactions. Two case studies, including a formal reconstruction of Halpern's interpretation of the biblical account of King David, illustrate the framework's…

Does a Self-Learning Migration Agent Learn? An Audited Evaluation of Evidence-Graded Experience Memory for Oracle-to-PostgreSQL Migration

Oleg Grynets, Vasyl Lyashkevych, Valeriia Oliferuk +3 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Do large language model (LLM) migration agents learn from accumulated experience, or do apparent gains reflect retrieval and reference reuse? We evaluate an evidence-graded agent for Oracle-to-PostgreSQL migration across four studies. On 1,833 documentation-derived source-reference pairs, persistent memory improved reference conformity (RC) over a no-memory baseline by 0.015 [0.004, 0.025], while policy adaptation added no gain (-0.004 [-0.010, 0.001]). An audit found that 264 of 367 held-out units (72%) shared a PostgreSQL reference with training, and the memory effect on the 103 leak-free units fell to 0.002 [-0.008, 0.011]. A model-free nearest-target copy baseline scored RC 0.222, outperforming all LLM systems (at most 0.163). A reference-grouped split reduced copying to 0.119; a rerun on 374 units in 118 independent target groups found no statistically distinguishable memory effect…

The multiplicative complexity of the three-bit low-half multiplier

Bshara Alhodali, Gregory Morse

cs.CC · · cited 0× · arXiv ↗ · more like this ·

We prove that the multiplicative complexity of the three-bit low-half multiplier is six, giving a structural, enumeration-free lower-bound proof valid against unrestricted nonlinear reuse in Boolean XOR-AND circuits. The value was previously established by SAT searches of the second author. An explicit six-AND circuit supplies the upper bound. The lower bound combines derivatives, quadratic products, complementary minors, and extraction modulo a Boolean ideal. Independent finite checks accompany the arguments. $\mathrm{MC}(M_3)=6$ is fully formalized in Lean 4. The kernel-checked proof uses only the axioms propext, Classical.choice and Quot.sound.

k-partite quantum homomorphisms

Amin Karamlou

quant-ph · · cited 0× · arXiv ↗ · more like this ·

$k$-partite XOR games and linear binary constraint system (BCS) games arise from systems of linear equations over $\mathbb{Z}_2$, providing distinct quantum relaxations of the same classical constraint satisfaction problem (CSP). Linear BCS games have been generalised to synchronous homomorphism games on arbitrary relational structures, with compositional semantics provided by the quantum monad. We introduce $k$-partite homomorphism games, extending $k$-XOR games from linear systems to arbitrary relational structures. This yields a framework for studying multipartite quantum CSPs and quantum homomorphisms. We characterise perfect strategies in both the tensor-product and commuting-operator models as Kleisli morphisms of suitable state-dependent graded quantum monads on a category of $k$-partite relational structures. We then study quantum advantage in the pseudotelepathic sense: the…

Bug Finding With Agentic Symbolic Execution

George Granberry, Wolfgang Ahrendt, Andy Gordon +1 more

cs.SE · · cited 0× · arXiv ↗ · more like this ·

Symbolic execution, in tools such as CrossHair for Python, is a powerful technique for finding bugs, but two barriers hinder its adoption: the human effort of annotating code with assertions, and the need to model the execution environment outside Python, such as an external database. To overcome both, we design an agentic harness that orchestrates the symbolic execution tool CrossHair together with an AI coding agent. Without human intervention, it instruments a repository with assertions, synthesizes a constraint-aware symbolic environment for the database, runs symbolic execution, and constructs a concrete test as evidence for each bug it reports. We evaluate our harness on 1,156,044 lines of Python code over 11 popular open-source Python web applications (Zulip, NetBox, Apache Superset, and others). With the synthesized environment, CrossHair executes 81% of the 5,406 contracted…

Typed Knowledge over Constructive Institutions: A Proof-Relevant Type Theory for Verified Science

Hans-Martin Will

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Mathematical proof assistants such as Coq, Agda, and Lean 4 build proof irrelevance into definitional conversion ($p \equiv q$ for $p, q : P$ with $P : Prop$), erasing which derivation established a theorem. While natural for mathematics over fixed axioms, judgmental proof irrelevance is incompatible with verified scientific stores, which must inspect and compare independent derivations of the same claim to assess consilience and compute counterfactual retractions when an assay, reagent, or model is invalidated. Moreover, combining definitional proof irrelevance with subsingleton elimination breaks strong normalization and renders algorithmic conversion non-transitive. We present the type-theoretic and institutional foundations of Eigenius, a verified knowledge substrate for science. First, we formulate a dependent kernel with cumulative universes ($Prop, Set, Type_k$), impredicative…

A Multi-Prover Interactive Protocol for Certification of Resolution Refutations

Philipp Czerner, Adrian Krauss, Josia Pietsch +1 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

A resolution refutation of a SAT-formula $φ$ is an independently checkable certificate proving that $φ$ is unsatisfiable. However, the refutations of $φ$ can be exponentially larger than $φ$. So, a verifier needs worst-case exponential time in the size of $φ$ to check their correctness. We present ResCertify, an interactive probabilistic protocol in which the verifier interacts with multiple independent, untrusted provers (MIP) to check the refutation with very low probability of error. The verifier runs in linear time in the size of $φ$. The provers require time $\mathcal{O}(n \cdot |Φ|)$, where $Φ$ is the resolution refutation and $n$ is the number of variables of $φ$. If they can be trusted to act as a multilinear oracle on certain queries, a single prover suffices, and the runtime can be improved to $\mathcal{O}(|Φ|)$. Finally, while the focus of our work is theoretical, we also…

Exploring 3-CNF Formulas Generated From Partial Steiner Triple Systems

Wyatt Olson, Jared Soundy, J. Z. Schroeder

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Steiner triple systems (STS) and subsets of these known as partial STS (PSTS) are combinatorial objects that have received substantial interest from mathematicians since their introduction in 1847. Over the last three decades, (P)STS have found applications in diverse fields ranging from digital circuit testing to wireless transmission. Perhaps unsurprisingly, the triple in (P)STS allows for a mapping to 3-conjunctive normal form (3-CNF) formulas, the Boolean formula used as input to 3-SAT. Prompted by this ready conversion of (P)STS to 3-CNF formulas and numerous real-world applications of (P)STS, we explore the intersection of (P)STS with 3-SAT and its counting version \#3-SAT. We explain the properties of (P)STS-generated 3-CNF formulas in terms familiar to the SAT community and experimentally compare them against randomly-generated 3-CNF formulas. We find that PSTS-3-CNF formulas…

A minimal intuitionistic public announcement logic

Philippe Balbiani, Hans van Ditmarsch, Cigdem Gencer +1 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

We introduce intuitionistic public announcement logics Lmin and Lequ determined by classes of birelational frames where the intuitionistic preorder and the modal accessibility relation do not need to satisfy the confluence conditions traditionally considered within the framework of IPAL. Our logics can be seen as generalisations of IPAL seeing that their language is based on a binary epistemic modality of "relativised knowledge" that allows us to define valid reduction axioms. Our main results are the soundness and completeness of Lmin with respect to the class of all birelational frames and the soundness and completeness of Lequ with respect to the class of all birelational frames where the modal accessibility relation is an equivalence relation.

Complexity of Deciding Existence of Maltsev Polymorphisms of Finite Relational Structures

Dejan Delic, Ali Syed

cs.CC · · cited 0× · arXiv ↗ · more like this ·

In this article, we show that the problem of deciding whether a finite relational structure $\mathbf{A}$ admits a Maltsev polymorphism is a computational problem, which can be solved in polynomial time. We provide a proof of this result by reducing the problem to deciding whether a binary relational structure, associated with $\mathbf{A}$ admits such a polymorphism. In our construction of such an algorithm, we make an extensive use of a property of binary relations, which is implied by the existence of a Maltsev polymorphism, the so-called rectangularity property.

Wave-Domain Semantic ISAC: Holographic Surfaces as Analog Semantic Encoders for Integrated TN-NTN

Shadi Danesh, Pooria Salami, Hesaam Zaravashan +4 more

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Semantic communication, near-field operation, and integrated sensing and communication (ISAC) are often considered separately in terrestrial and non-terrestrial networks (TN--NTN). We show how a large electromagnetic aperture can connect them. \textcolor{black}{Nonlocal metasurfaces and holographic apertures act on the spatial spectrum of an incident field and can execute linear projections, which form an early stage of semantic feature extraction, directly in the wave domain before digitisation, thereby reducing the corresponding digital processing burden.} Near-field focusing also provides position-dependent sensing features, allowing the aperture to serve as an analog semantic-ISAC front end on resource-constrained aerial and satellite platforms. We describe the underlying physics, the co-design of constrained analog projections with lightweight digital decoders, and a case study in…

Gödel's Incompleteness Theorems in Grounded Arithmetic

Bryan Ford

math.LO · · cited 0× · arXiv ↗ · more like this ·

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic in which every term is a program and truth is grounded evaluation. RGA discharges a hypothesis only when it proves the hypothesis decided. This paper shows, in a machine-checked Isabelle/HOL development, how Gödel's incompleteness theorems hold for RGA and for systems built on it. RGA's implication is material and RGA has the disjunction property, so the implications the textbook proof of the second theorem uses fail while its entailments and rules hold: Gödel's proof survives as entailments. RGA does not prove its consistency sentence Con, and RGA derives its own second theorem as the entailment $\mathit{Con}\vdash\neg\mathit{Pr}(\ulcorner\mathit{Con}\urcorner)$ and as one sentence quantified over proofs. The second theorem is then proved once, for every Gödel extension of RGA: an entailment relation on RGA's language…

Context Types: Bunched Modalities for Unifying Safety and Reachability

Zhe Zhou, Benjamin Delaware, Suresh Jagannathan

cs.PL · · cited 0× · arXiv ↗ · more like this ·

Most type systems are designed to verify safety properties: the judgement $e : τ$ holds if $e$ may evaluate to any value contained in the denotation of $τ$, but nothing more. More recent type systems have considered the complementary class of reachability properties: in these systems, the typing judgment holds if $e$ must be able to evaluate to every value denoted by $τ$, and possibly more. This paper introduces a refinement type system for higher-order functional programs where types can capture both safety and reachability properties. Simultaneously supporting both is challenging because each imposes different constraints on how variable bindings in a typing context are interpreted. We address this challenge by treating typing contexts as a kind of resource that mediates which capabilities are available when typing a program. We formalize this notion by developing a resource algebra…

Trust, but verify, audit and attribute: a human-in-the-loop framework for checking AI-produced research results

György Eigner, Patrik P. Süli, Roland Hollós

cs.AI · · cited 0× · arXiv ↗ · more like this ·

Artificial intelligence (AI) systems now produce research results in bulk: in October 2026 a single laboratory released more than 700 AI-generated mathematics manuscripts, only part of them with machine-checked proofs. Such volumes will be checked mostly by AI agents that call specialised software. A passing check certifies only the artefact that was checked. For proofs translated into the proof assistant Lean, it has been shown that this artefact may state something other than the author's text, and that deciding whether a translation is faithful is undecidable in general. The human researcher therefore stays in the loop, and human and AI contributions must be recorded. We propose a domain-independent, human-in-the-loop framework for checking AI-produced results. Validated, agent-usable tools with different grounds of trust check the results; a fidelity audit asks whether each check…

Compile-Gated Lean Proof Refactoring with Enterprise Agent Practices: A Model per Step under a US\$3 Cap, Followed by Programmatic Rewrite Rules

Bobber Cheng

cs.SE · · cited 0× · arXiv ↗ · more like this ·

Our closed-track entry (Arena username Vexorium-Agent) scored 86.31 points on the final board (L = 77.07, H = 81.86, Z = 100) over the 60 final problems, against 33.33 for the reference proofs, 8th at the deadline (top: 92.57), for US\$166.33 at list prices with every call counted (per problem: mean US\$2.772, at most US\$2.874; US\$3 cap). Three practices carry the entry. First, each paid stage runs the model that measured best per dollar for it among the 9 we tested in our own harness: GPT-6.1 Sol the early sessions, GPT-6.1 Terra the later ones and the tail at 70% of Sol's cost per turn, and Gemini 4 Argon the review and repair; Sol also runs the style rewrite. Second, what our development and research runs learned ships as compiler-checked programmatic rewrite rules rather than prompt text (+0.93 points from rules fixed before the release; +0.26 and +0.30, in sample, from passes…

A Hoare Logic for Continuous-Time Stochastic Processes

Kei Imada, Justin Hsu

cs.LO · · cited 0× · arXiv ↗ · more like this ·

Programming language researchers have developed a wide array of tools to reason about probabilistic programs, but it remains unclear how to apply these proof techniques to continuous-time stochastic processes. To bridge this gap, we propose a verification method for properties of continuous-time stochastic processes by reasoning about them as standard programs. To demonstrate our approach, we define a continuous semantics for a probabilistic imperative language $\mathrm{pWhile}^{\mathrm{dt}}$ by taking the Kuratowski limit of the standard semantics, which collects limit points of the standard program semantics as the time-step approaches zero. Then, we present a Hoare-style logic that uses loop invariants and decreasing functions to verify properties of continuous programs. To establish soundness, we identify a broad class of assertions that are preserved from the standard semantics to…