AI 速览：作者报告构造出经典色数任意大而量子色数恒为3的图，首次改进了自 Brassard–Cleve–Tapp 以来的量子色数间隙。
We confirm a conjecture of the first author [SODA'26] on a strong form of pseudo-telepathy for Khot's $d$-to-$1$ games: for every $d\geq 4$, every $ε>0$, and every $k\in\mathbb N$, there is a $d$-to-$1$ label-cover game of classical value less than $ε$ that admits a perfect quantum strategy using finite-dimensional shared entanglement with measurement contexts of radius at least $k$. As a consequence, there exist graphs whose quantum chromatic number $χ_q$ is $3$ and whose classical chromatic number $χ$ is arbitrarily large. This is the first improvement on the quantum chromatic gap since the work of Brassard, Cleve, and Tapp [Phys. Rev. Lett.'99], which produced graphs for which $χ$ grows exponentially in $χ_q$. To prove the conjecture, we proceed as follows. We start with a ``stretched'' version of the Mermin--Peres magic square, obtained by spacing out its equations and linking them with additional long equation wires. This operation increases the radius of the initial measurement contexts of a perfect quantum strategy for the game, while preserving classical unsatisfiability. We then apply parallel repetition to make the classical value small, and we turn the system into a pseudo-telepathic multi-layered Kneser hypergraph via a PCP construction of Dinur, Guruswami, Khot, and Regev [STOC'03]. Finally, we feed the resulting hypergraph into the reduction of Fei, Minzer, and Wang from hypergraph colouring to $4$-to-$1$ games, we establish quantum completeness of this reduction, and we show that it preserves context radius.
FARMS: A Verifiable Foundation for Automated Computational Science
Di Wu, Ling Liang, Haizhao Yang
AI 速览：作者提出 FARMS，将计算数学知识转化为可供 AI 解释与复用、并带有显式保证的“计算知识”基础。
Automated computational science could accelerate discovery by selecting, adapting and developing numerical methods. This prospect requires mathematical knowledge that AI systems can interpret and reuse with explicit guarantees. Here we present FARMS, a faithful and efficient foundation that transforms computational mathematics into AI-ready computing knowledge. FARMS connects formal statements to source context, algorithmic meaning and quantitative guarantees through source preparation, reusable representations and semantic review. Across 171 targets in randomized numerical linear algebra and numerical partial differential equations, 157 were accepted by the pipeline, with mean estimated costs of US \$0.85-2.29 per target across sources. Lean-checked implications from explicit source premises connect selected statements to computational skills, illustrated by a heat-flow solve and wave-response compression. FARMS therefore supports an affordable, reusable knowledge foundation for trustworthy automated computational science.
AI 速览：提出一个基于 SMT 的可扩展 Lean 证明自动化框架 crush，用去函数化桥接高阶构造与一阶求解器，并支持可扩展的翻译与证明重建。
Lean's rich expressiveness supports higher-order functions, inductive datatypes, and user-defined abstractions, making it challenging to translate proof obligations into first-order Satisfiability Modulo Theory (SMT) queries and reconstruct kernel checked proofs. We present crush, an extensible SMT-backed proof automation framework for Lean. To bridge the gap between Lean's higher-order constructs and the solver's first-order logic, crush uses defunctionalization to encode function values and their applications. We formalize this translation for a supported higher-order fragment and prove its soundness. Moreover, crush provides metaprogramming interfaces for extending both Lean-to-SMT translation and the reconstruction of Lean proofs from solver certificates without modifying the translation pipeline. We implement crush as both a tactic and a backend for other third-party automation systems. We show that across four such use cases that target verification and general proof automation, crush discharges more obligations than the competing backends and reconstructs more kernel-checked proofs than the baselines.
Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
AI 速览：提出代数世界模型（AWM），将未知环境中的探索转化为可执行假设、范畴论引导的结构化模型，并在 Lean 4 中形式化证明可达性与不可能性。
AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.
On Deciding the Constraint Loop Problem in Dimension Two
Daria Goliasova, Toghrul Karimov
AI 速览：作者通过分析无限运行见证的结构，将二维线性约束循环终止性判定从多项式空间改进到多项式时间，并给出基于 Z3 的实现。
Recently, Guilmant, Lefaucheux, Ouaknine, and Worrell [2] proved decidability of the termination problem for linear constraint loops over two real-valued variables, thus settling a wellknown open problem. Their algorithm is based on a theoretical result that such a loop does not terminate if and only if it has a witness of an infinite run of a specific shape. By analysing the structure of the witness carefully, we show that termination such loops can be decided in polynomial time, improving on the polynomial space bound argued by Guilmant et al. We also present an efficient implementation of the polynomial-time algorithm based on the satisfiability modulo theories (SMT) solver Z3.
A Hierarchy of Composition Procedures for Logic-Based Workflow Patterns
Radosław Klimek
AI 速览：论文提出从 ΠC₀ 到 ΠC₄ 的模式组合过程层次，将工作流模式的组合复杂度与时间逻辑片段 TL_j 的表达力分离，形成 ΠC_i[TL_j] 框架。
Logic-based workflow patterns capture recurring behavioural structures together with reusable temporal specifications. Their composition raises distinct problems as workflow structures become richer, including instantiation, nesting, conditional execution, repeated occurrences, and traceability of generated formulae. This paper proposes a hierarchy of Pattern Composition ($ΠC$) procedures, from $ΠC_0$ to $ΠC_4$, that organizes these requirements as progressively richer compositional capabilities. The hierarchy separates compositional complexity from the expressive power of the temporal-logic fragment, represented by $TL_j$, yielding a framework $ΠC_i[TL_j]$ for developing logical workflow specifications. We develop activation-aware Pattern Composition ($ΠC_2$), which distinguishes the structural presence of a nested pattern from its execution in a particular workflow context. We formalise its recursive procedure, analyse its properties, and define an evaluation protocol for conditional activation, conservativity under mandatory composition, and specification growth. The hierarchy also characterizes selective occurrence qualification for iterative patterns ($ΠC_3$) and provenance for tracing generated formulae to their sources ($ΠC_4$). Finally, we outline $ΠC_{\mathrm{Assist}}$, an orthogonal mode in which AI proposes and refines pattern expressions subject to the hierarchy's compositional checks.
Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets
Marco Bernardo, Andrea Esposito, Claudio A. Mezzina
AI 速览：作者提出用后向就绪多重集相等增强前向后向互模拟，从而在稳定配置结构和可逆进程演算中给出遗传历史保持互模拟（HHPB）的两种互补刻画。
We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, over stable configuration structures, and an operational one, in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity (FRB) augmented with backward ready multiset equality, which is able to distinguish between autoconcurrency and autocausation. With respect to previous work, we thus shift the emphasis from uniquely identifying events, as done in other characterizations, to counting occurrences of identically labeled events associated with incoming transitions. This yields a more lightweight behavioral equivalence than HHPB: our bisimulations are still binary relations instead of ternary ones and do not need to incrementally build any labeling- and causality-preserving bijection for occurred events. We show that our characterizations are valid in the absence of non-local autoconflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures HHPB, and backward ready multiset logic, developed for our extension of FRB.
AI 速览：作者提出 Vampire-Hammer，将 Lean 目标交给 Vampire 自动定理证明器求解，并重建可由 Lean 内核检查的证明。
We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel. Vampire-Hammer uses the Lean-auto framework to process goals and premises before dispatching them to Vampire for proof search. Doing so, we rely on standard TPTP problem formats and annotated TSTP proofs that support proof reconstruction. With a 10-second budget on 196,083 eligible Mathlib theorems, Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget.
In this work, we present the first semantic interpretation of useful call-by-value evaluation through a non-idempotent intersection type system called U. One first contribution of this paper is a characterisation of termination of useful call-by-value evaluation via U-typability. That is, a term is typable in system U if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system U provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of useful evaluation is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy. Our third contribution is a termination-equivalence result between standard call-by-value, which may perform erasing reductions, and useful call-by-value, which is non-erasing. To establish this result, we introduce a non-erasing restriction of standard call-by-value, a refinement that serves as an intermediate calculus bridging standard and useful call-by-value. We show that all three calculi have the same termination behaviour, and hence induce the same observational equivalence.
Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec, Qing Wang
A behavioural theory consists of machine-independent postulates characterizing a particular class of algorithms or systems, an abstract machine model that provably satisfies these postulates, and a rigorous proof that any algorithm or system stipulated by the postulates is captured by the abstract machine model. The class of interest in this article is that of synchronous parallel algorithms. For this class a behavioural theory has already been developed by Blass and Gurevich, which, though mathematically correct, fails to be convincing, as it is not intuitively clear that the postulates really capture the essence of (synchronous) parallel algorithms. We present a much simpler (and presumably more convincing) set of four postulates for (synchronous) parallel algorithms, which are close to those of Gurevich's sequential ASM thesis. The key difference is an extension of the bounded exploration postulate using multiset comprehension terms instead of ground terms formulated over the signature of the states. In addition, all implicit assumptions are made explicit, which amounts to representing states of a parallel algorithm by meta-finite first-order structures. The article first provides evidence that the axiomatization characterizes the whole class of deterministic, synchronous, parallel algorithms, then formally proves that parallel algorithms are captured by Abstract State Machines (ASMs). The proof uses the requirement of the bounded exploration postulate that update sets be uniformly definable, by equality-free first-order formulae, in the finite critical structures determined by the witness terms; these formulae are translated into the guards of a parallel ASM rule. This version corrects the characterization proof of the first version, whose key lemma was false; the bounded exploration postulate has been amended accordingly.
We complete Maksimova's classification of Craig and deductive interpolation in normal extensions of S4. In particular, we prove Craig interpolation for the six extensions of S4 for which the status of the property was still open. The proof strategy builds upon the ideas of Smoryński, but employs a novel approach using Fine's frame formulas for splitting clusters in transitive models.
Peter Dolog, Kim G. Larsen, Marius Mikučionis, Frederik F. K. Rasmussen
For more than three decades, UPPAAL has supported the modelling and analysis of real-time and cyber-physical systems. Yet building a suitable model, formalising the intended properties, choosing analysis techniques and interpreting counterexamples remain iterative tasks that demand substantial expertise. Large language models (LLMs) can offer plausible explanations and even solutions, but they are not necessarily correct. We present UPPAAI, an extension of UPPAAL in which users construct, explain, debug and specify models in dialogue with an LLM. The guiding principle is that the user requests, the LLM proposes, explains and orchestrates, and UPPAAL verifies. UPPAAI exposes the UPPAAL editor, queries and verifier through a Tools API. We report on seven case studies, from explaining to a newcomer to learning a controller, covering timed automata, stochastic hybrid automata and strategy learning. LLMs proved to be extremely helpful in not just generating solutions but also pro-actively suggesting relevant UPPAAL features it was not asked about.
We construct, for each deterministic Turing machine that halts on all inputs, one polynomial vector field with rational coefficients that performs the same logical computation at unit Euler step, at every smaller or variable step in $(0,1]$ with divergent sum, and along the flow. This unifies discrete-time and continuous-time computation by polynomial dynamics, which earlier characterizations treated separately. For a machine making $T$ transitions in space $H$, a logical scale $h=2^{-s}$ with $s=O(H)$ suffices, with physical time $O(s(T+s))$, drift disturbances up to $h^{2K}$ for a fixed exponent $K$, and $2Ks+3$ fractional bits at unit step. On a fixed compact domain, polynomial time and robust eventual decision characterize P and PSPACE, respectively, with polynomial scale thresholds and no supplied stabilization horizon in the space case. Without sign, floor or conditional primitives, margin amplification at bounded speed, overlapping polynomial gates and interval-product estimates give the common realization, from which we derive shared logical traces, fixed-field PSPACE-complete prediction and a robust safety family with polynomial certificates common to all Euler steps and the flow.
We provide a new foundational approach to the generalization of terms up to equational theories. We interpret generalization problems in a universal-algebraic setting making a key use of projective and exact algebras in the variety associated to the considered equational theory. We prove that the generality poset of a problem and its type (i.e., the cardinality of a complete set of least general solutions) can be studied in this algebraic setting. Moreover, we identify a class of varieties where the study of the generality poset can be fully reduced to the study of the congruence lattice of the 1-generated free algebra. We apply our results to varieties of algebras and to (algebraizable) logics. In particular we obtain several examples of unitary type: abelian groups; commutative monoids and commutative semigroups; all varieties whose 1-generated free algebra is trivial, e.g., lattices, semilattices, varieties without constants whose operations are idempotent; Boolean algebras, Kleene algebras, and Gödel algebras, which are the equivalent algebraic semantics of, respectively, classical, 3-valued Kleene, and Gödel-Dummett logic. Finally, we prove that the variety of MV-algebras, the equivalent algebraic semantics of Lukasiewicz logic, has nullary type.
We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in \emph{affine logic} the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and {\it vice versa}. By contrast, in the setting of \emph{Łukasiewicz logic}, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Łukasiewicz logic but are all equivalent.
Many problems in control can be expressed as quantified constraints, such as robust forward and backward reachability, synthesis of controllers, solutions to motion planning problems. In this paper, we develop a method for computing inner and outer approximations of global solutions to very general quantified constraints, generalizing widely the state of the art on similar problems, usually restricted to at most one alternation of quantifiers or to local solutions. By global solutions, we mean characterizing accurately the entire set of solutions, within some prescribed bounds. For this, our approach uses a set inversion technique relying on oracles for set inclusion using local solutions to related quantified reachability problems. We exemplify the approach throughout the paper on different examples related to control problems.
For a strictly increasing $G:\mathbb{N}\to\mathbb{N}$ with $G(0)\geq 1$, we study minimal-basis function algebras generated by recursion along generalized inverses of its iterates. Bounded recursion requires an earlier pointwise majorant; unbounded recursion has no such requirement. If the orbit $G^{[t]}(0)$ has no polynomial upper bound, we obtain exact fixed-function membership spectra, reverse-divisibility inclusion, and indexed intersections that need not be single-stride algebras. Every finite divisibility-downset is realized in both regimes, and mixed strides admit fixed functions expressing any finite monotone Boolean condition on their additive stride monoid. For every generator, the realized bounded spectra form a bounded meet-semilattice: a construction sharing a bounding input coordinate realizes finite intersections without an unrestricted selector. Polynomial orbit growth is equivalent to definability of each of ordinary predecessor, unary doubling, and addition in any fixed unbounded stride algebra. In this case the algebra is ordinary primitive recursion relative to its inverse map, giving full collapse for primitive-recursive $G$. Ordinary predecessor belongs to a bounded stride algebra exactly when the orbit is polynomially bounded and $G$ has bounded successive differences; equivalently, ordinary bounded recursion embeds. A locality obstruction explains the additional bounded requirement, and two primitive-recursive generators with quadratic orbits have opposite bounded collapse behavior.
We study finite-terminating, address-only step recursion on the nonnegative reals, from zero, unit successor and projections. For reduced positive rational strides $s=a/q$ and $t=b/v$, we prove $\mathcal{C}s\subseteq\mathcal{C}t$ if and only if $q$ divides $v$, for both the bounded and unbounded algebras $\mathcal{C}\in{\mathcal{B},\mathcal{U}}$. The bounded compiler preserves earlier global majorants on every auxiliary input. Mixed rational stride sets are classified by least common denominators and supernatural denominators. Primitive-recursive translated-coordinate grid codes characterize the unbounded algebras and yield $\mathcal{U}{1/q}\cap\mathcal{U}{1/v}=\mathcal{U}{1/\gcd(q,v)}$. For bounded intersections, we prove an exact reduction: all corresponding identities hold if and only if the single identity $\mathcal{B}{1/2}\cap\mathcal{B}_{1/3}=\mathcal{B}_1$ holds, equivalently if the Boolean parts of the integer successor and addition algebras under scalar bounded recursion coincide. A Boolean reconstruction reduces general functions to predicates; a clipped fine-grid simulation with a frozen global resource bound identifies the union of predicate precision classes with the addition level. These reductions do not decide the resulting predicate equality, so literal bounded intersections remain unresolved. We also prove that unbounded-program equality is $Π^0_1$-complete and extensional bounded-algebra membership is $Σ^0_2$-complete. The model has no free real arithmetic or Zeno limits; semantic majorant validity is distinguished from syntax transformation.
Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is challenging, due to the strong interference exhibited in these algorithms. The Ben-Ari concurrent garbage collector is an algorithm where the complex interactions between the components prevent the construction of compositional rely and guarantee conditions. This paper investigates an approach for verifying the Ben-Ari algorithm, which enables reasoning to be performed in a more compositional manner in cases where compositional reasoning would not otherwise be possible. This is accomplished by reasoning that a given property holds for all instances of a particular variable and then instantiating the variable to the local variable required. As well as providing a reasoning approach which is more compositional, the result is the identification of the core property required of a component, thus enabling a deeper understanding about the reasons why the algorithm works correctly. This helps to reveal the reasons why the rely/guarantee approach does not work directly for some problems.
We develop a formal semantics for a general class of coordinated systems of parameterized transformations, taking the Transformer as a paradigmatic starting point but abstracting from its particular mathematical instantiation. Representational vectors receive both extensional reference and ordered intensional interpretations, while parameter structures acquire relative, second-level interpretations that determine how argument properties are preserved, replaced, or combined. This yields the notion of a transforming concept: a parameterized transformation whose numerical action is coordinated with a corresponding property-level map. We then distinguish the common algebraic-semantic core of these systems from their architecture-specific functional organization, allowing different mathematical instantiations and mechanical realizations of the same abstract system type. The framework is applied to attention heads and residual connections, providing semantic explanations that depend only on the shared algebraic-semantic core and their local functional organization and therefore generalize beyond the standard Transformer. These analyses also reveal the modularity of the framework: complex architectures can be decomposed into simpler semantically coordinated subsystems whose organization may recur across different abstract system types.
Wen Fang, Xianxian Li, Jun Liu, Jie Luo, Yongxin Tong, Ke Xu
We study self-reference and solution independence in Boolean $K$-SAT as a finite analogue of Gödel incompleteness. Independence is defined through factorial moments of the solution count. Constant-width random formulas fail this criterion due to correlations among overlapping assignments. At a covering threshold, logarithmic-width random CNFs have a Poisson solution count, with positive probabilities of unsatisfiability and unique satisfiability. Replacing a redundant clause by one falsified by the unique solution yields an unsatisfiable companion preserving the unsigned incidence graph. For every permitted local view of a good uniquely satisfiable formula, an unsatisfiable companion preserves that view. Irreducibility defeats deterministic and bounded-error evaluators using $N^c$ clause queries, for fixed $0<c<1$. It establishes a local information obstruction, not an unrestricted time lower bound. For fixed $δ>0$, transcripts of $N^{1-δ}$ queries leave $N-o(N)$ bits of witness entropy. On typical support graphs, expansion yields linear Resolution width, linear PC/PCR and SOS degree, and exponential proof size. Bounds hold for semantic Cutting Planes under a partition condition and for Positivstellensatz with bounded product width, uniformly over unsatisfiable support-preserving signings. Structural evidence and the limits of acceleration strategies motivate the self-referential $K$-SAT exhaustive-search hypothesis (SRK-ESH): no uniform deterministic algorithm deciding the promise family achieves a fixed proportional saving in the exponent. This dual-evidence criterion combines intrinsic hardness mechanisms with algorithmic evidence. We interpret this hypothesis as a quantitative projection of the Gödel-style local--global gap. The information obstruction constrains quantum local observation and statistical learning from bounded local information.
Sebastian Körner, Oliver Emil Bøving, Christoph Matheja
Weighted programming is a framework by Batz et al. for describing mathematical models or optimization problems as imperative programs parametrized over semirings and then analyzing them with program verification techniques like weakest precondition calculi. Applications include reasoning about expected outcomes of probabilistic programs and competitive analysis of online algorithms. We extend weighted programming with (1) countable nondeterminism and (2) user-defined additive rewards, where programs are parametrized over modules instead of semirings. The resulting framework enables reasoning about expected resource consumption of probabilistic programs and about optimal scores of combinatorial games. A technical challenge is that wp-calculi for weighted programs with (1) and (2) over arbitrary modules can be unsound, because it is well-known that continuity properties commonly used in program semantics break in the presence of countable nondeterminism. We study conditions under which a wp-style transformer for reasoning about weighted programs is sound with respect to an operational ground truth defined in terms of weighted decision processes (WDPs) - transition systems that generalize Markov decision processes by drawing transition weights and state rewards from a module. Based on those conditions, we show that a range of concrete instances of the weighted programming framework enjoy sound weakest precondition reasoning. We demonstrate the usefulness of our wp-semantics through case studies for different modules. We mechanized our extended weighted programming framework and our main soundness results in the interactive theorem prover Lean. Instantiating these results for probabilistic programming yields, to the best of our knowledge, the first mechanized proof of a fixed point characterization of minimal expected rewards in Markov decision processes with countable nondeterminism.
Higher-order recursion schemes (HORS) are finite, simply typed recursive programs that generate potentially infinite trees. Their monadic second-order model-checking problem is decidable. We prove that tree equivalence of deterministic HORS is undecidable and, more precisely, $Π^0_1$-complete under total computable many-one reductions. The lower bound holds for safe, productive schemes of order at most four over the fixed ranked alphabet $Σ_2=\{e:0,d:2\}$, consisting of one nullary and one binary symbol. Adapting the counter-guard witness of Boiret, Piorkowski, and Schmude, we generate all candidate executions of a two-counter machine by producing both continuations at every counter test. An integer weight is nonzero exactly on legal prefixes. Functions at fixed simple types represent the polynomial of growing degree. A shift recurrence updates them without storing a separate step counter, allowing the witness to be implemented by safe applicative HORS rules. At candidate halts, the intermediate schemes generate unary observation subtrees whose lengths encode the two natural-number components of the signed weight. Invalid candidates give matching observations; a legal halt produces a finite discrepancy. Fixed constructor contexts encode these intermediate trees over $Σ_2$. For the upper bound, a finite monotone semantics decides head convergence and supports an algorithm computing exact tree prefixes at any prescribed finite depth, including positions labelled $\bot$.
Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, Nathalie Sznajder
Temporal graphs are graphs where the presence or properties of their vertices and edges change over time. When time is discrete, a temporal graph can be defined as a sequence of static graphs over a discrete time span, called lifetime, or as a single graph where each edge is associated with a specific set of time instants where the edge is alive. For static graphs, Courcelle's Theorem asserts that any graph problem expressible in monadic second-order logic can be solved in linear time on graphs of bounded tree-width. We propose the first adaptation of Courcelle's Theorem for monadic second-order logic on temporal graphs that does not explicitly rely on a parameter proportional to the lifetime, or defined as the maximum number of time-edges incident with any vertex which in the worst case is higher than the lifetime. We then introduce the notion of derivative over a sliding time window of a chosen size, and define the tree-width and twin-width of the temporal graph's derivative. We exemplify its usefulness with meta-theorems with respect to a temporal variant of first-order logic. The resulting logic expresses a wide range of temporal graph problems including a version of temporal cliques, an important notion when querying time series databases for community structures.
Generative AI can convert uncertainty into authoritative-seeming verdicts, displacing the justificatory work on which democratic epistemic agency depends. As a corrective, I propose a Brouwer-inspired assertibility constraint for responsible AI: in high-stakes domains, systems may assert or deny claims only if they can provide a publicly inspectable and contestable certificate of entitlement; otherwise they must return Undetermined. This constraint yields a three-status interface semantics (Asserted, Denied, Undetermined) whose statuses mark entitlement to categorical speech rather than truth values of the underlying world-claim. The framework distinguishes internal entitlement from public standing while connecting them through the certificate as a boundary object. Philosophically, it develops a form of applied intuitionism: resistance to unwarranted completeness becomes a norm of public machine speech, under which categorical commitment requires exhibited and contestable entitlement. I operationalize the constraint through structured certificates, decision-layer gates for threshold and argmax predicates, and a reason-coded output contract. A design lemma shows that, under a refutation-soundness condition on the contractually specified negative side, certificate-sound binary totality presupposes witnessed decidability on the declared scope. Under the proposed normative output contract, Undetermined is not a tunable reject option but a mandatory status whenever the available certificates do not uniquely license assertion or denial. By making outputs answerable to contestable warrants rather than confidence alone, the paper aims to preserve epistemic agency where automated speech enters public justification.
Monotonic semantic path orders (MSPOs) are powerful reduction orders, but their effective use in theorem proving and termination analysis raises three issues: efficient comparison of terms, ground totality, and a reduction-pair formulation. Inspired by weighted path orders (WPOs), we introduce generalized weighted path orders (GWPOs) which encompass both WPOs and MSPOs. GWPOs and MSPOs coincide as classes of reduction orders, thereby yielding efficient and ground-total subclasses of MSPOs. We further formulate the reduction-pair version of the GWPO for the dependency pair method, from which a reduction-pair version of the MSPO is obtained. In contrast to the reduction-order setting, the correspondence between GWPOs and MSPOs no longer fully carries over, establishing the GWPO as a framework of independent interest. Effectiveness of the resulting reduction pairs is assessed by standard termination benchmarks.
We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation. Our framework exploits the structure of the simulation algorithm: Hamiltonians are given as weighted sums of Pauli strings, embedded into larger unitaries through block encodings, and transformed into time-evolution operators by quantum signal processing (QSP). Using a symbolic Pauli-sum semantics for ancilla-indexed circuit blocks, our verifier proves that the distinguished all-zero ancilla block is proportional to the target Hamiltonian and infers the subnormalization factor automatically. It then verifies the QSP layer by extracting the implemented polynomial transformation and certifying its approximation error. This structure-aware abstraction is essential for scalability. Composing our verified block encoding and QSP wrapper yields an estimated macro-expanded size of about 1.52 million gates. The verifier certifies the block encoding once and checks the QSP layer through its abstract interface, without expanding the oracle calls. Our implementation verifies block encodings of structured Pauli-sum Hamiltonians with up to 256 system qubits and verifies QSP Hamiltonian-simulation instances by extracting their implemented polynomials and checking the resulting approximation bounds. These results show that fully automated verification can handle common Hamiltonian-simulation circuits at substantial scale when it exploits their algorithmic structure.
We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.
In this paper, we present a mental temporal logic BPICTL together with a sound and complete axiomatization, which generalizes CTL by introducing mental modalities. A sound and complete inference system of BPICTL is given. We also prove the finite model property and decidability of BPICTL. Furthermore, we present a model checking algorithm for BPICTL.
Relational pattern languages generalize Angluin's pattern languages by requiring the strings substituted for repeated occurrences of a variable to stand in a given relation, rather than to be identical. We study erasing pattern languages under the equal-length relation, where all occurrences of a variable must be replaced by strings of the same length. Over alphabets with at least three letters, this class is known to be learnable in the limit from positive data. We show that over a binary alphabet it is not, which resolves an open question from earlier work. Our proof reveals that non-learnability already holds for the restricted subclass of languages generated by patterns that have exactly three maximal substrings of variables. We then show that patterns with at most two maximal substrings of variables are learnable in the limit from positive data for every alphabet of size at least two. If the target pattern is known to have at most one maximal substring of variables, this can even be achieved by an iterative learner, which updates its hypothesis using only the current example and its previous hypothesis.