https://arxiv.org/api/Hce7RFt7u7ViZ9dJiEMwu0mCUbI 2026-07-21T19:47:41Z 19781 105 15 http://arxiv.org/abs/2607.10650v1 2026-07-12T08:34:08Z

Fixed-point logics provide an expressive intermediate framework for reasoning about temporal properties of programs. One of the key approaches to solving their validity checking problem is via transformations from least fixed points to greatest fixed points ($μ$-to-$ν$ transformations), which generalizes a reduction from termination verification to safety verification studied in binary reachability analysis. In this paper, we introduce game-semantic interpretations of $μ$-to-$ν$ transformations. We first introduce a new $μ$-to-$ν$ transformation based on parity relations. We show that solving $μ$-to-$ν$-transformed fixed-point equation systems corresponds to finding winning strategies in the game semantics of the original fixed-point equation systems. We apply the same game-semantic framework to interpret two existing $μ$-to-$ν$ transformations, one by Kobayashi et al.\ and the other by Unno et al, and show that they admit analogous game-semantic interpretations. Furthermore, we show that the game introduced by Tsukada et al.\ corresponds to an alternative characterization of the winning condition. On the implementation side, we propose optimization techniques for efficiently solving our new $μ$-to-$ν$ transformation. We implement these techniques in a fixed-point logic solver, compare our approach with existing solvers, and demonstrate the effectiveness of the proposed optimizations through experiments.

2026-07-12T08:34:08Z Satoshi Kura Hiroshi Unno http://arxiv.org/abs/2606.19936v2 2026-07-12T06:59:27Z

Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structures which can be verified and expressed in the precise language of a proof assistant. In this paper, we present Prismriver, a formalization library of music theory in Lean 4. We use Prismriver to generalize beyond existing work that assumes equal temperament tuning. We also discuss modelling counterpoint music theory with Prismriver. By formalizing music theory in Lean 4, we open the door to verifiable algorithmic composition and accompaniment generation. Prismriver also has a custom DSL integrated with MusicXML exports to interoperate with other music software. Prismriver can be used to compose music with Lean, using monadic composition primitives.

2026-06-18T08:33:37Z Leni Aniva Claire Wang 10.1145/3830435.3830954 http://arxiv.org/abs/2607.10594v1 2026-07-12T06:13:54Z

We prove that, on finite graphs of rank-width at most two, VR-recognizability and counting monadic second-order definability coincide. This advances the recognizability-versus-definability problem from bounded linear clique-width to the first nontrivial bounded rank-width level beyond the rank-width-one split-decomposition case. The proof first treats split-prime graphs. The maximal partial-tree theory of Clark and Whittle organizes the non-sequential cut-rank-two separations, while a single strong separation orients all strong equivalence classes and yields a CMSO-definable laminar family of canonical cores. Although the auxiliary partial tree is not itself transduced, it proves that every canonical local piece has a port-contiguous layout of uniformly bounded linear rank-width. The width argument uses partition atoms and the branch-width-three display theorem of Hall, Oxley, Semple, and Whittle and does not assume that graph torsos remain prime. Coherent ordered rank-two frames then permit a finite-state bottom-up evaluation whose local transitions are definable by the bounded-linear-clique-width theorem of Bojańczyk, Grohe, and Pilipczuk. Finally, the CMSO-transducible canonical split decomposition lifts the result from prime graphs to arbitrary graphs of rank-width at most two.

2026-07-12T06:13:54Z Antonios Kalampakas http://arxiv.org/abs/2607.10318v1 2026-07-11T13:47:08Z

This volume of the Electronic Proceedings in Theoretical Computer Science (EPTCS) includes the contributed papers presented at the 21st International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2026), in Lisbon, Portugal, on July 24th, 2026, at the Federated Logic Conference (FLoC 2026) as a satellite event of the 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). The program committee for this edition of LFMTP was chaired by Olivier Hermant and Sophie Tourret. More information about LFMTP can be found on https://lfmtp.org.

2026-07-11T13:47:08Z EPTCS 448, 2026 Sophie Tourret INRIA and MPI for Informatics Olivier Hermant Mines Paris - PSL 10.4204/EPTCS.448 http://arxiv.org/abs/2607.10216v1 2026-07-11T09:00:34Z

The theory of simplicial complexes is a cornerstone of topology, offering a sophisticated tool for computing invariants. We present a formalization of abstract simplicial complexes and stellar subdivisions in the Lean proof assistant. We adopt a purely combinatorial framework in order to provide a cohesive foundation for studying the theory of stellar subdivisions as seen in many contexts of combinatorial topology. In particular, we provide formalizations of morphisms between abstract simplicial complexes; several crucial constructions and operations on complexes, such as links and joins; and perform a comprehensive study of how stellar subdivisions interact with these operations. We state and prove a number of identities commonly used in the study of triangulated manifolds, such as deriving equivalences between links in an abstract simplicial complex $K$ and in a stellar subdivision $σ_s K$, including results with no references in the standard literature. To our knowledge, this is the first formalization of stellar subdivisions in any proof assistant.

2026-07-11T09:00:34Z Garett Cunningham Daniel Zach Stefan Friedl http://arxiv.org/abs/2607.13069v1 2026-07-11T01:32:22Z

Large language models produce chain-of-thought (CoT) reasoning that appears logically sound yet may not genuinely depend on its stated premises. We introduce interventional grounding audits, a black-box, step-level test of premise dependency: we intervene on a single premise by substituting its target predicate with a fresh symbol, re-run the model, and check whether each reasoning step's normalized conclusion (canonical predicate form) changes. We evaluate on ProntoQA, a synthetic multi-hop deductive reasoning benchmark with gold proof trees, where step-level premise dependencies are known. Applied to 50 ProntoQA problems with GPT-4o, our method achieves F1 = 0.806 on detecting proof-tree dependencies (F1 = 0.885 on predicate-determining dependencies; Recall = 100%), significantly outperforming a self-consistency baseline (F1 = 0.343; 95% bootstrap CIs non-overlapping). We further identify that 66% of correctly-solved problems contain at least one aligned step insensitive to a direct proof-tree dependency under consistent substitution -- all involving entity-introduction premises, a documented blind spot of the consistent-substitution evaluator -- a "right answer, wrong reasoning" signal invisible to passive methods. All audit certificates, raw outputs, and reproduction scripts are available in a public GitHub repository, and we discuss scope limits beyond formal, parsable benchmarks.

2026-07-11T01:32:22Z Accepted at the ICLR 2026 Workshop on Logical Reasoning of Large Language Models (https://iclr.cc/virtual/2026/10017466) Hironao Nakamura http://arxiv.org/abs/2601.16152v2 2026-07-10T21:50:23Z

Data systems increasingly operate under persistent legal, political, and analytic disagreement, where no single interpretive authority can be assumed. A neutral substrate provides stable shared reference without requiring agreement about causal or normative interpretation: it fixes reference structurally and leaves interpretation to extension layers. This paper derives the identity structure such a substrate requires using a small transformation algebra. Identity is treated as transformation-invariance: a referent is individuated by the admissible operations that preserve it. Once routine record operations are fixed, individuation becomes a structural calculation. That calculation exposes a mismatch between reference kinds and identity regimes. An accountability substrate must refer to six carrier kinds: obligation-bearers, rules, occurrences, scopes, records, and plain referents. Three kinds have more than one admissible basis. A scope may be fixed by extension or structure; a rule by content or structure; a plain referent by locus or object. Decomposition separates the scope readings, refinement separates the rule readings, and forking separates the plain-referent readings. Counting reference kinds gives six, while transformation analysis forces at least nine identity regimes. The three additional regimes add no new kind to the inventory. They arise from identity behavior under ordinary operations, and any attempt to collapse them reappears as a hidden regime that persistent disagreement cannot hold fixed. The result is a conditional lower bound. A richer transformation basis may leave the bound unchanged or force further splits, but it cannot erase a distinction witnessed here. The additional regimes correspond to distinctions often handled by modeling convention, but such conventions cannot substitute for regime-level identity commitments under persistent disagreement.

2026-01-22T17:51:02Z 55 pages Denise M. Case http://arxiv.org/abs/2607.09605v1 2026-07-10T16:59:26Z

Many production quantum programming languages represent hybrid quantum computations by extending a classical base language with a quantum effect, where qubits are addressed by reference, and quantum operations are understood to mutate some external quantum state. However, the semantics of this view of quantum computation remains underdeveloped, especially when the language allows mid-circuit measurements and non-termination. In this work, we provide a general method for building denotational semantics for such languages, by defining the quantum orchestra monad, which precisely captures this style of quantum effect. The monad has a concrete presentation, being based on the formalism of quantum instruments, a common tool in quantum information theory for capturing the action of a quantum process along with its classical outcomes. It acts on the category DCPO, and so enables the interpretation of divergent hybrid programs. The quantum orchestra monad serves as a natural extension of both the classical state monad and the probabilistic powerdomain monad. We investigate some of the subtleties present when trying to naïvely extend these definitions to the quantum non-commutative case.

2026-07-10T16:59:26Z 25 pages + 23 appendix Alex Rice Dominik Leichtle Kim Worrall Robert I. Booth http://arxiv.org/abs/2607.09558v1 2026-07-10T16:03:19Z

In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.

2026-07-10T16:03:19Z Clotilde Bizière Jérôme Leroux Grégoire Sutre http://arxiv.org/abs/2607.09534v1 2026-07-10T15:38:33Z

Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.

2026-07-10T15:38:33Z Kathleen Barsse Romain Péchoux Simon Perdrix http://arxiv.org/abs/2607.13065v1 2026-07-10T13:20:38Z

This report contains the proceedings of the 21st International Workshop on Termination (WST 2026), which was held in Lisbon on July 25. It was affiliated with the 13th International Joint Conference on Automated Reasoning (IJCAR 2026), which was part of the Federated Logic Conference (FLoC 2026).

2026-07-10T13:20:38Z Florian Frohn Étienne Payet http://arxiv.org/abs/2607.09366v1 2026-07-10T12:44:08Z

Program verification is crucial for software correctness, but producing fully verified programs remains difficult in practice. This paper studies whether implementation structure affects automated verifiability when multiple generated programs are intended to satisfy the same task-level semantics. We present Diversify2Verify, a staged LLM-based pipeline for Why3 that infers representation-specific contracts, generates and tests diverse recursive and imperative array/list implementations, and attempts verification with bounded verifier-guided annotation repair. We also construct a verification-oriented benchmark of 73 tasks over integers, arrays, and lists, yielding 292 implementation variants. Diversify2Verify verifies 96 artifacts initially and 154 after two repair passes, improving artifact-level verification from 32.9% to 52.7%. At the task level, at least one variant verifies for 49 of 73 tasks, a 67.1% success rate. These results show that task-equivalent implementations can differ substantially in verifiability and that implementation diversity helps find verification-friendly artifacts.

2026-07-10T12:44:08Z Shirley Yu Ruben Martins http://arxiv.org/abs/2605.28215v2 2026-07-10T10:34:44Z

In-context learning (ICL) enables multimodal large language models (MLLMs) to classify images from a few labelled examples. Yet, how these models use the provided context remains opaque. While Chain-of-Thought prompting is widely used, recent work argues that it may not reflect true internal computation. In this paper, we systematically evaluate the concept-based explainability of frozen MLLMs under few-shot ICL using five conditions of increasing formal rigour, ranging from baseline classification to Description Logics (DL) axiom generation. Evaluating four state-of-the-art MLLMs via an independent LLM-as-a-judge pipeline, we demonstrate that explaining is genuinely harder than predicting alone. Surprisingly, forcing models to generate formally structured, concept-based explanations degrades predictive accuracy monotonically (from 93.8% to 90.1%), contradicting the assumption that explicit reasoning universally aids performance. However, when models successfully articulate class-discriminative visual features, explanation quality strongly correlates with correct predictions. Our findings suggest that while MLLMs excel at visual classification, they lack the specific instruction-tuning required for formal, machine-verifiable explainability.

2026-05-27T09:32:34Z Accepted to the CompLearn Workshop at ICML 2026 Carmen Quiles-Ramírez Leticia L. Rodríguez Nicolás Martorell Natalia Díaz-Rodríguez http://arxiv.org/abs/2606.18977v2 2026-07-10T09:58:57Z

Proving termination or non-termination of lasso programs is a challenging problem in program verification. To unify state-of-the-art approaches under a common execution framework, we present PaSTTeL, a modular and generic parallel portfolio framework for termination and non-termination analysis of lasso programs. PaSTTeL is designed to: (1) facilitate the integration of new analysis algorithms into the portfolio, (2) execute registered strategies concurrently, and (3) act as a self-contained library component that can be seamlessly embedded into any external project requiring (non-)termination analysis. Initial experiments demonstrate that an instantiation of PaSTTeL performs competitively against state-of-the-art tools.

2026-06-17T12:00:32Z Presented at WST 2026 Anissa Kheireddine Souheib Baarir Hugo De Sa Pereira Pinto http://arxiv.org/abs/2601.14211v4 2026-07-10T08:55:57Z

We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a deterministic matching problem. Our unification procedure can be seen as a special case of full higher-order unification where flex-flex pairs can be solved in a most general way. Moreover, our method generalizes Libal and Miller's recent functions-as-constructors higher-order unification (FCU) by dropping their global restriction on variable arguments, thereby losing the property that every solvable problem has a most general unifier. In fact, minimal complete sets of unifiers of deterministic higher-order patterns may be infinite, so decidability of the unification problem remains an open question.

2026-01-20T18:17:11Z accepted at IJCAR 2026 Johannes Niederhauser Aart Middeldorp 10.1007/978-3-032-32592-1_12