arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-07-20T20:50:37Z
Patrick Barlatier, Richard Dapoigny
arXiv categories: math.LO, math.AT

Tarski's geometry of solids reconstructs point-like objects from concentric families of spherical regions rather than taking points as primitive entities. We formalize this reconstruction in Coq within a nominal mereological framework inspired by Lesniewski. The main question is how a regional, point-free geometry can support a Kuratowski closure operator on the objects obtained from such reconstructed points. We distinguish the regional topology of Tarski-Lesniewski solids from a point-class topology built on ball representatives. Point-like objects are treated as concentric point-classes, namely equivalence classes of ball representatives under equality of concentric families. Regional objects provide the source of basic neighbourhoods, but closure acts on point-class plurals rather than on solids themselves. We define point-open plurals and introduce a neighbourhood-based closure operator on them. The central Coq theorem proves that this operator satisfies the four Kuratowski closure axioms. We further define point-closed plurals as fixed points of this closure and derive a topological boundary remainder. The formalization separates regional openness, representative equivalence, and topological adherence, while avoiding the reification of reconstructed points as mereological individuals.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-21T05:40:33Z
Janggun Lee, Jeehoon Kang
arXiv categories: cs.PL

Out-of-order multiprocessor is a critical piece of modern hardware, and their verification must solve the following challenges. First, inter-core interleaving, in which the order their reads and writes reach shared memory is unrestricted. Second, intra-core out-of-order execution, in which instructions fire out of program order. The combination of the two yields weak outcomes, which no sequential execution explains, and modern ISA allows such behaviors to account for them. However, the microarchitecture even exhibits excess out-of-order executions, temporarily entering states forbidden by the ISA. While discarded later, such states complicate reasoning about the core in full-system verification. Prior works verify a range of processor designs, while none have performed unbounded verification for out-of-order multiprocessor exhibiting such weak outcomes. We present the first formal verification of an out-of-order multiprocessor against an in-order, weak-memory ISA. Our key idea is a well-designed core specification, which captures the essence of excess executions in a single list of instructions. Building upon this, we decompose the proof into two steps. The first is a core refinement, proving a core implementation against this specification, abstracting away every microarchitectural state except those necessary to reason about excess executions and the core interface. The second is a system inclusion, serializing the out-of-order memory executions and inter-core interleaving into the ISA, easily removing excess executions thanks to the core specification. All of our proofs are mechanized in Rocq, heavily utilizing large language model (LLM) agents to write proofs automatically.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-22T03:54:53Z
Moritz Doll, Iman Shames
arXiv categories: math.OC, cs.LO, eess.SY

We introduce an open-source library for machine-checked control theory in the interactive proof assistant Lean to lay foundations for the verification of cyber-physical systems. To this end, as representative theorems, we present formalizations of Lyapunov stability theory and the small-gain theorem. First, the machinery employed for formalizing Lyapunov stability, i.e., neighborhood filters, allows stating a Lyapunov theorem that covers both points and sets and applies to continuous, discrete, and hybrid systems. Second, the small-gain theorem is proved via stating input-output systems as relations without the usual well-posedness assumption. The Lean formalization of each of these theorems is then presented. We conclude by discussing the library architecture and mentioning some of the other system theoretic results that are formalized in the library along with future plans.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-22T14:14:50Z
Lorenzo Saraiva, Edward Hermann Haeusler
arXiv categories: cs.LO

In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-22T14:15:25Z
Sebastián Urciuoli
arXiv categories: cs.LO

In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report some substantial progress. We present formal proofs of confluence for beta-reduction and by using Takahashi's revision of Tait and Martin-Löf's proof, subject reduction for the entire family of the Pure Type Systems and consistency for some impredicative subclass, assuming normalization. As to the proof of confluence, we also develop a theory of alpha-commutative relations which, in our view, entails a clearer presentation and treatment of the problem than in similar developments. Finally, we assess general merits and drawbacks of the approach. The whole development has been machine-checked using Agda.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-22T17:25:15Z
Jennifer Paykin, Steven Baldasty, Joseph P. Near, Christian Skalka
arXiv categories: quant-ph, cs.PL

Programming distributed quantum systems requires multiple actors to coordinate precise sequences of quantum operations, classical communication, and entanglement generation. Writing such protocols directly as distributed processes is tedious and error-prone, and subtle mismatches can cause deadlock or silently incorrect quantum states. We present Qoreo, a choreographic programming language for quantum distributed systems in which an entire protocol is expressed as single, global program (a choreography) rather than as a collection of independent actor processes. Qoreo includes a local quantum language with linear types that enforce the no-cloning principle; a choreographic language that combines local quantum computation with inter-actor classical and quantum communication; and a process language for individual network nodes. We prove type safety for choreographies, guaranteeing that well-typed programs implement well-defined quantum operations, and we define endpoint projection~(EPP), which automatically derives a network of independent processes from any choreography. We prove EPP sound and complete with respect to the choreographic semantics; as a corollary, every well-typed choreography projects to a deadlock-free process network. The metatheory of Qoreo is fully mechanized in Rocq, and we provide an extraction pipeline to NetQASM for simulation and deployment on quantum network hardware.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-24T17:56:21Z
Junye Ji
arXiv categories: cs.LO, cs.DS, cs.SC

We formalize in Lean 4 the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices. The program returns $S,U,U^{-1},V,V^{-1}$ and proves $UAV=S$, $U^{-1}SV^{-1}=A$, four inverse identities, the Smith divisibility conditions, and equality of $S$ with a canonical reference matrix. Stabilization terminates because each recursive pass strictly decreases the binary size of the active pivot; the outer algorithm recurses on the lower-right block. The computation also emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are taken from the recorded primitive runs. Composite phases form their traces by concatenating the charge lists returned by the executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, give fixed polynomial bounds for both trace cost and the encoded length of the five output matrices. The theorem concerns these arithmetic primitives; structural operations and compiled Lean runtime are outside the model.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-26T15:26:00Z
Shuqing Zhao
arXiv categories: cs.CL, cs.PL

We report the design and end-to-end verification of first-class IEEE-754 binary32 (FP32) and bfloat16 (BF16) arithmetic for ARCH, a hardware description language intended to be generated by language models. Every operator - comparisons, conversions, add, sub, mul, and fused multiply-add (FMA) - is described once against a single bit-vector IR and rendered three ways from one source: synthesizable SystemVerilog, an SMT-LIB model, and a Lean 4 proof model. The three artifacts cannot drift apart structurally, and the residual per-node printer correspondence is machine-checked: a Yosys-to-SMT miter proves the emitted SystemVerilog equivalent to the SMT model for all 24 operators. Verification splits at the solver-tractability frontier: multiplier-free operators (comparisons, add/sub over all 2^64 inputs, conversions, and all binary BF16 arithmetic) are proved exhaustively equivalent to the SMT-LIB FloatingPoint theory; the SAT-hard multiplier-bearing operators (FP32 mul and FMA) are proved correctly rounded in Lean, sorry-free, against a value-level round-to-nearest-even specification over exact dyadic values. Physical characterization exposed the FMA as the timing outlier: its exact-wide 470-bit datapath does not pipeline in our flow. We reimplemented it as a bounded 98-bit guard/round/sticky datapath that pipelines to 268 MHz on Nangate45, and proved, in Lean and over all 2^96 inputs, that it is bit-identical to the exact-wide reference, so it inherits the reference's proven correct rounding. The equivalence is tractable precisely because the shared multiplier appears on both sides and cancels: neither a SAT solver nor the proof ever solves a multiplier equivalence. (The BF16 FMA is deliberately an FP32-accumulating fusion, characterized as exactly that.) All machine-checked claims are pinned to a tagged open-source release.

arXiv abstract · PDF

Formalized mathematics and autoformalization · cs.SE relevance selection · published 2026-07-20T22:41:55Z
Tasmim Rashid, Muhammad Zubair Malik
arXiv categories: cs.SE

We present an exploratory study on using Large Language Models (LLMs) to generate Alloy formal specifications from both requirements documentation and production source code, and to derive executable test cases from those specifications. We evaluate on two real open-source Python libraries: Flipper, a feature flag management system, and Cerberus, a data validation library. In both cases, the LLM produced workable Alloy specifications and executable tests without any manual correction. For Flipper, our pipeline uncovered a genuine bug that the existing test suite had missed: the library silently accepts duplicate flag names, directly contradicting its documented uniqueness requirement. A direct LLM baseline--generating tests from the same README but skipping the Alloy step--achieved 68% branch coverage yet failed to catch this bug across all three independent runs. This suggests that introducing a formal intermediate representation can surface constraint-level defects that coverage-oriented generation may miss. For Cerberus, the code-derived specification captured an implicit abstraction over sized types that the documentation-derived spec omitted, producing two additional tests. Across both libraries, code-based specifications showed lower variance in test generation (mean SD = 2.15) than documentation-based ones (mean SD = 5.0), though whether this generalises remains an open question. Index Terms--formal specifications, Alloy, large language models, automated testing, specification drift, software validation.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-23T11:15:38Z
Fred Mesnard, Étienne Payet, Wim Vanhoof
arXiv categories: cs.LO, cs.AI, cs.SC

We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-26T07:07:29Z
Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang
arXiv categories: cs.LO, cs.AI, cs.PL, math.CO

Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Turán-type upper bounds, including Mantel's theorem and the Erdős pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Turán densities of Mantel's theorem and the Erdős pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-20T00:20:20Z
Hemant Gouni, Frank Pfenning, Jonathan Aldrich
arXiv categories: cs.PL, cs.CR

Non-interference properties, spanning confidentiality and integrity, have long enjoyed a position as the high water mark of program security guarantees. Information flow type systems comprise the primary means for obtaining non-interference properties of programs, but their potential as a holy grail for secure programming has remained latent. Prior work bifurcates the type system along confidentiality and integrity, resulting in duplicate reasoning machinery and complex specifications. Furthermore, long-held wisdom dictates that non-interference must be weakened with downgrading mechanisms to accommodate the needs of practical programs, nearly all of which violate confidentiality and integrity in the course of fulfilling their purpose. This often pierces abstraction barriers and compromises modular reasoning. We introduce parametric information flow, which uses recent insights from modal type theory to shed light on these issues. In particular, we draw inspiration from work on the open and closed modalities, highlighting their rich interplay. Though each individual modality finds uses throughout the literature, our key insight is that their joint interaction suffices to reconstruct full-spectrum information flow reasoning, producing a single framework accounting for both confidentiality and integrity. Downgrading and analogues of advanced reasoning tools in the lineage of robust declassification are recovered without extensions to our theory, strengthening prior results. We show non-interference via a binary logical relations argument, realizing robustness as an ordinary 2-hyperproperty mediated by our modalities. Our work reveals state-of-the-art downgrading mechanisms to be wholly compatible with those for abstraction and modularity, arising precisely from the semantics of the latter under full-strength non-interference.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE relevance selection · published 2026-07-20T01:00:20Z
Takanori Ishibashi, Kazuhiro Ogata
arXiv categories: cs.SE

Model checking is a powerful technique for verifying properties of systems or protocols, but it often suffers from the state space explosion problem. For protocols such as the Alternating Bit Protocol (ABP) and the Sliding Window Protocol (SWP), increasing parameters such as channel capacities or window sizes leads to a reachable state space that is infeasible for exhaustive model checking. To address this, we propose a technique that combines model checking with simulation relations. We focus on three protocols: the Simple Communication Protocol (SCP), ABP, and SWP. Formalized as state machines, these protocols are presented in decreasing order of abstraction: SCP, ABP, and then SWP, which results in a corresponding increase in reachable states. While SCP is verifiable through direct model checking without state space explosion, the direct application of model checking to ABP and SWP becomes infeasible as their parameter values increase. We demonstrate that ABP satisfies its invariant property by combining model checking on SCP with a simulation relation from ABP to SCP. Furthermore, we demonstrate that SWP satisfies its invariant property through the composition of simulation relations from SWP to ABP and from ABP to SCP, in conjunction with model checking on SCP. These approaches enable the formal verification of protocols with large reachable state spaces by conducting model checking on a significantly smaller state machine.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-20T04:29:26Z
Ian J. Hayes, Larissa A. Meinicke
arXiv categories: cs.PL, cs.LO

The rely/guarantee approach supports the stepwise development of concurrent programs. Our goal is to develop a theory for reasoning algebraically about concurrent programs in a rely/guarantee style, where rely and guarantee conditions are encoding as commands within our theory. As for mathematics, distributive laws are essential for algebraic manipulation of concurrent programs. In this paper we investigate distributive laws for parallel composition and show how these can be applied to rely/guarantee concurrency. The most general distributive laws are only refinements in a single direction, however, by restricting the form of the command being distributed, one can devise stronger equality laws, which are applicable to guarantee commands as well as to suitable combinations of rely and guarantee commands. Our approach is to develop the distributive laws in a more abstract synchronous atomic algebra, and then apply them to an instance of that algebra supporting rely and guarantee commands. The theory has been formalised in Isabelle/HOL along with proofs of the lemmas presented here.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE relevance selection · published 2026-07-20T07:18:59Z
Xinyu Zhang, Runxuan Fang, Ziqun Bao, Yechuan Xia, Jianwen Li, Geguang Pu
arXiv categories: cs.SE, cs.FL

Program verification tools often rely on specific intermediate representations and analysis backends, limiting the reuse of verification algorithms and model checkers across frameworks. In contrast, hardware model checking has developed a mature backend ecosystem, where standard formats such as BTOR2 support reusable algorithms for counterexample search and inductive safety proving. Applying these capabilities to C requires translating assertion-based programs into transition systems that hardware model checkers can directly process. We present C2Btor, a method for encoding such verification tasks into BTOR2 models. C2Btor uses a program counter to capture control transfers, represents data states and memory objects with bit-vectors and arrays, and maps assumptions and assertion checks into BTOR2 constraints and bad-state properties. We evaluate C2Btor on SV-COMP C ReachSafety benchmarks and a curated assertion-category benchmark suite, comparing it with representative program verification tools. C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking, and is especially effective on bit-vector benchmarks, where it solves 75.5% of the tasks with no wrong verdicts. These results show that the BTOR2 route allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-20T09:09:20Z
Stefanie Muroya, Thomas A. Henzinger
arXiv categories: quant-ph, cs.LO

We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE relevance selection · published 2026-07-20T14:17:00Z
Yue Xue
arXiv categories: cs.SE

Smart-contract vulnerabilities often arise from inconsistencies between business paths that should correspond to one another, such as single and batch entry points, direct and adapter-based flows, quote and execution paths, or inverse operations such as buy and sell. Existing analyzers are effective for many local syntactic and data-flow patterns, but they provide limited support for bugs whose oracle is relational: whether two semantically paired paths preserve compatible guards, state transitions, value flows, and failure behavior. This paper introduces chiral analysis, a relational model that treats paired business paths as implicit specifications for each other. We formalize chiral relations as static analogues of metamorphic relations, derive obligations over guards, actors, state, value, ordering, failure behavior, and external interactions, and report a vulnerability when a violated obligation has security impact. We implement this idea in ChiralDetector, a Solidity prototype that extracts business paths, ranks candidate pairs with static facts, applies LLM-based semantic filtering and detection, and validates and deduplicates findings. In a preliminary evaluation on the Phi protocol, ChiralDetector reduced 3,217 statically ranked path pairs to 1,643 semantic candidates, produced 101 deduplicated finding groups, and retained 44 strict-validator positives that manually collapsed to 13 effective unique issues. These include cross-art Merkle proof reuse, fee unit mismatches, public state-tracking helpers, and refund propagation gaps. The results suggest that chiral analysis can expose business-logic bug classes that are difficult to express as single-function rules while providing a structured way to control LLM cost and validator precision.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-20T15:19:00Z
Stephen F. Siegel
arXiv categories: cs.PL, cs.LO

We consider the problem of verifying a message passing program in which the number of processes is a parameter NP and each process knows its unique ID. Processes communicate using send and receive commands which specify a single destination or source. To verify the program, the user provides functions specifying the number of messages sent from process i to process j, the level of each communication event in the happens-before hierarchy, and a fact that holds for the k-th message sent from i to j. These are used to transform the program to a parameterized sequential program which can be verified using any techniques appropriate for such programs. We realize this approach in an extension to Frama-C/Wp to verify C/MPI programs.

arXiv abstract · PDF

Program verification, analysis, and software security · cs.SE relevance selection · published 2026-07-21T06:20:35Z
Yin Wu, Yixuan Liu, Yi Li, Chenyang Peng, Hao Wu, Ming Fan, Ting Liu, Haijun Wang
arXiv categories: cs.SE

Standardized token contracts (e.g., ERC-20) form the foundation of digital assets. However, attackers increasingly abuse this standardization to disguise malicious trap tokens. Unlike obvious violations, these contracts employ a strategy of "deceptive adherence": they strictly adhere to standard protocols to evade detection while embedding covert logic to defraud users. To address this, we first systematize the trap landscape by proposing a novel taxonomy derived from the intrinsic functional lifecycle of tokens (Generation, Circulation, Persistence, and Observation). We then propose TrapHunter, a framework designed to identify these traps and expose covert pathways within these deceptive contracts via intent deviation analysis. Specifically, TrapHunter introduces a unified semantic representation combining Abstract Behavior Trees (ABTs) and Augmented Path Graphs (APGs) to normalize intra-procedural syntax and reveal hidden execution paths driven by inter-procedural state dependencies. Crucially, it bridges the semantic gap by leveraging LLMs to reason about the behavioral intent of deviations from reference implementations, followed by fork-based dynamic validation to confirm exploitability. Experimental evaluation on 269 real-world contracts with three LLMs (DeepSeek, GPT, and Gemini) demonstrates that TrapHunter effectively detects all six categories of traps, achieving an average precision of 81.8% and recall of 85.4%, significantly outperforming state-of-the-art tools.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-22T14:12:32Z
Luiz C. F. Fernandez, Mario R. F. Benevides
arXiv categories: cs.LO

In this paper, we present a dynamic logic with parallel operators for the formal verification of authenticity and safety properties of cryptographic protocols. The logic incorporates communication actions and is specifically designed to reason about protocol executions in adversarial environments. We extend an existing dynamic logic with parallel operators by introducing concepts derived from the Dolev-Yao intruder model. As the underlying logic is completely axiomatizable, we obtain a complete axiomatization for the extended system. Furthermore, we develop a tableau calculus for the proposed logic and prove its termination, soundness, and completeness.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-22T15:09:10Z
Marco Pérez, Pedro López-García, Jose F. Morales, Manuel V. Hermenegildo, Fred Mesnard
arXiv categories: cs.PL, cs.LO

Abstract interpretation-based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states. Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates. In this paper, we address a fundamental issue in relating these two frameworks: studying the translation of Ciao assertions into LPTP formulae and identifying a partial correspondence between assertion-based and logic-based specifications. We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases, and finally analyze the resulting soundness and completeness trade-offs. We argue that our proposal enables a tight integration of Ciao's assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-22T15:11:30Z
Daniel Jurjo-Rivas, Joaquín Arias, Gopal Gupta, Jose F. Morales, Pedro López-García, Manuel V. Hermenegildo
arXiv categories: cs.LO

Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling the analysis of determinism, types, aliasing, and resource usage, as well as application in verification and program optimization. However, Abstract Interpretation has not yet been studied in the context of Goal Directed Answer Set Programming (ASP). In this work, we take a first step in this direction. We present a top-down algorithm based on the PLAI fixpoint, implemented in the abstract interpreter of the Ciao Prolog Preprocessor, to perform abstract interpretation of goal-directed ASP. We also introduce the Shared-Constraints abstract domain, designed to capture potential relations among variables induced by constraints. Finally, we study the practicality of the approach in s(CASP) through three applications: detection of false odd loops over negation, efficient forall evaluation enabled by the Shared-Constraints domain, and abstract specialization (including the simplification of required global constraints). Our results show that compile-time static analysis can improve the evaluation of goal-directed ASP programs.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-23T11:16:49Z
Jan Gruteser, Michael Leuschel, Katharina Engels, Fabian Vu
arXiv categories: cs.LO, cs.AI, cs.GT

ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB's new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-23T11:21:06Z
Santiago Escobar, Raúl López-Rueda, Carlos Olarte
arXiv categories: cs.SC, cs.LO, cs.PL

The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with an unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method can synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-24T14:40:28Z
Julia Butte, André Platzer
arXiv categories: cs.LO, cs.GT

This paper introduces the three-player differential game logic dGL3, which enables the verification of hybrid games of discrete and differential equation dynamics with three players who may or may not form coalitions. Each player has an individual goal they try to fulfill, so the game becomes non-zero-sum when the goals of the players overlap. This enables dGL3 to verify complex situations involving multiple players, taking into account their coalitional power. dGL3 excels at verifying games where players share safety objectives but otherwise pursue different goals, so that they may or may not collaborate. In this case, zero-sum assumptions lead to overly conservative results by neglecting the potential of coordination amongst the players. In this paper, the syntax and semantics of dGL3 are presented and crucial properties of dGL3 are proved. A sound and relatively complete proof calculus for dGL3 is introduced and the use of dGL3 is illustrated in a canonical example.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-25T04:16:14Z
Martin Rinard
arXiv categories: cs.PL

We present prophecy variables for forward formulations of program analysis problems that require information about the future execution of the program. We specify prophecy and history variables via a domain specific language that augments the step rules of the base operational semantics with subset inclusion constraints over the prophecy and history variables. This tight coupling between the prophecy and history variable specification and the operational semantics promotes the construction of correctness and optimality proofs for program transformations, with the proofs structured as forward simulations between the original and transformed versions of the program. In comparison with traditional dataflow approaches, this approach eliminates mechanisms such as explicit control flow graphs, abstraction functions, concretization functions, Galois connections, and separate backward and forward analyses. We present a verified implementation of prophecy and history variables and use the implementation to prove correctness and optimality properties of two classic transformations, partial dead code elimination and lazy code motion, that use both prophecy and history variables. To the best of our knowledge, these proofs are the first machine checked correctness and optimality proofs for these transformations.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-25T12:19:22Z
Frédéric Dabrowski
arXiv categories: cs.LO, cs.SE

Requirements for synchronous programs relate observations across ticks, while general-purpose deductive backends use first-order conditions on local steps. Kairos is a prototype toolchain generating such obligations from synchronous programs and source-level temporal safety contracts in assume-guarantee form. Using the standard automata-theoretic reduction, it translates their linear temporal logic (LTL) formulas into bad-state automata, forms their product with the program, and derives tick-indexed Why3 obligations. We formalize the underlying principles and prove reactive contract correctness: under the stated program and automaton hypotheses, every input trace satisfying the environment assumptions induces a unique execution satisfying the temporal guarantees. The definitions, obligation construction, and proof are mechanized in Rocq. A medical infusion controller illustrates the workflow.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-20T00:44:18Z
Oscar Perez Mora
arXiv categories: cs.PL, cs.LO

Handler calculus conflates resumable and non-resumable effect operations through a single do construct, distinguished only by result type annotation. This conflation does not compromise type safety -- progress and preservation hold -- but it permits resumption bindings for non-resumable operations, creating vacuous bindings that the because-calculus eliminates at compile-time. The because-calculus structurally separates registration (non-resumable, void-returning) from attestation (resumable, non-void-returning) using dual effect rows and level-indexed typing, rejecting such clauses at compile-time via the Resumption Subconstraint. We prove the Conflation Theorem: collapsing the adjoint triple of existential, substitution, and universal functors into a single effect operation is non-faithful -- the erasure from the because-calculus to handler calculus maps rejected clauses to accepted ones. Four movements correspond to four natural transformations; categorical semantics maps each judgment to a category-theoretic construct. We establish progress, subject reduction, and tower progress for the full calculus.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-20T19:07:47Z
David Richter, Timon Böhler
arXiv categories: cs.PL

We revisit the role of higher-order unification in dependently typed languages and identify a fundamental limitation of existing pattern-based fragments: their inability to synthesize functions defined by case analysis. Even simple and ubiquitous constraints arising from type inference, particularly from use of induction principles, fall outside the expressive power of Miller patterns and their modern extensions. We observe that such constraints naturally correspond to definitions by dependent pattern matching. Motivated by this correspondence, we propose integrating dependent pattern matching into the unification process. We present a prototype implementation of a small dependently typed language that collects delayed unification constraints and resolves them via a pattern matching compiler. Our approach successfully infers solutions that are rejected by current systems such as Rocq and Lean, suggesting a new direction for unification that unifies type inference and pattern matching compilation.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T02:51:18Z
Qunhui Zhang
arXiv categories: cs.PL

Type inference for dynamically typed languages must reconcile four qualitatively different sources of evidence: assigned values, explicit declarations, contextual requirements, and structural operations. Existing approaches often combine them into one constraint set, causing spurious conflicts or requiring annotations. We present Generic Constraints Projection (GCP), a zero-annotation inference framework that stores these sources in four monotone slots on a stable definition-time template and evaluates each call in a fresh projection session, preventing cross-call contamination while specializing return types. GCP uses Outline Equational Matching, an open structural preorder, and a future-this projection rule that preserves concrete receiver types across fluent chains and subtype extensions. On the success-state fragment of a bounded type domain, we prove monotonicity, local and global fixed-point convergence, conditional projection soundness, termination, multi-module convergence, and order independence. For an immutable core language, we also prove big-step evaluation existence, type preservation, runtime receiver retention, and projection-evaluation coherence. We instantiate GCP in Outline for typed ontology worlds and in a Python annotation-recovery pipeline. On 513 manually adapted, fact-paired Outline ports of TypeEvalPy cases, GCP obtains 513/513 exact matches, compared with 485/513 for the published Codestral Q&A baseline on the same fact IDs (two-sided exact McNemar p = 7.45e-9). This is a carrier-port evaluation in TypeEvalPy's closed-world Python vocabulary, not a run on unmodified Python sources.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T12:38:05Z
Arturo De Faveri
arXiv categories: cs.LO

We investigate the notion of model of the linear $λ$-calculus from an algebraic perspective. Our starting point is the operad of linear $λ$-terms, whose algebras provide a natural candidate. We prove that this notion of model is equivalent to two other structures: a linear analogue of Curry's $λ$-algebras, and semiclosed operads, a class of operads equipped with an internal abstraction operation. The equivalence between these three approaches unifies three complementary answers to the question of what should be regarded as a model of the linear $λ$-calculus. As a second contribution, we give a finite equational presentation for the linear variant of $λ$-algebras using the linear combinators $\mathbf{B}$, $\mathbf{C}$, and $\mathbf{I}$. Finally, exploiting the equivalence with semiclosed operads, we establish a linear analogue of Scott's representation theorem by showing that every model arises as a reflexive object in a natural monoidal closed category of presheaves.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T14:04:41Z
Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, Thomas Vinet
arXiv categories: cs.LO

Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this paper, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time, known as $\mathtt{FBQP}$.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T14:11:42Z
Alessandro Aldini, Pierluigi Graziani, Claudio Antares Mezzina, Gandolfo Vergottini
arXiv categories: cs.LO

We propose a logical formalisation of computational errors in reactive, nondeterministic systems. To this aim, we introduce a new three-valued symmetric nondeterministic disjunction, designed to provide a faithful logical representation of the nondeterministic choice arising in concurrent computations. The connective is defined within the framework of nondeterministic matrices (Nmatrices) and derives from a minimal combination of Kleene's tolerant semantics and Bochvar's symmetric error persistence, thereby eliminating the residual asymmetry induced by sequential evaluation strategies such as McCarthy's logic. The resulting semantics admits genuinely nondeterministic outcomes in mixed cases involving errors, while preserving commutativity and operational symmetry.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T14:11:58Z
Ana Jorge Almeida, Sandra Alves, Mário Florido
arXiv categories: cs.LO, cs.PL

Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-22T14:12:48Z
Philippe de Groote, Vincent Tourneur
arXiv categories: cs.LO

We introduce a typing system that is particularly well suited for typing the linear lambda-calculus in de Bruijn notation. This typing discipline, which is reminiscent of Hodas' and Miller's model of resource consumption, guarantees that any well-typed term is linear without the need for an occurrence check. We then establish the subject reduction property.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T11:16:12Z
Ehud Shapiro
arXiv categories: cs.PL, cs.DC, cs.LO, cs.MA

A grassroots platform is a multiagent distributed system in which multiple independent instances can form and operate independently of each other and of any global resource, yet may coalesce into ever larger instances, possibly resulting in a single global instance. Grassroots platforms aim to offer an egalitarian/democratic alternative to centralised/autocratic and decentralised/plutocratic global platforms. Here, we present Grassroots Logic Programs (GLP), a multiagent concurrent logic programming language designed for the implementation of grassroots platforms: we recall the standard operational semantics of logic programs; introduce the concurrent operational semantics of GLP as its restriction; recall multiagent atomic transactions; use them to introduce a multiagent operational semantics of GLP; and prove multiagent GLP to be grassroots. The grassroots social graph—the foundational grassroots platform on which all others are based—serves as a GLP programming example.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T11:19:58Z
Pedro Cabalar, Jorge Fandinno, Nicolas Rühling, Torsten Schaub, Sebastian Schellhorn, Philipp Wanko
arXiv categories: cs.AI, cs.LO

While the integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. We address this gap by introducing a many-sorted variant of the Bound-founded Logic of Here-and-There (HTb), providing a versatile framework capable of characterizing equilibrium models across a wide spectrum of alternative semantics for extensions of ASP with linear constraints. We apply this framework to the setting of difference constraints, focusing on the semantic characterization of clingo[DL]. Central to our approach is the formalization of foundedness for numeric variables. By investigating how different hybrid systems - such as clingo[DL], clingcon, and flingo - justify constraint atoms, we uncover the semantic roots of their varying behaviors. This investigation results in a single, consistent framework that not only formalizes the foundations of current systems like clingo[DL] but also facilitates the rigorous study of program simplifications and the future integration of diverse semantic principles.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T11:20:15Z
Arun Raveendran Nair Sheela, Christophe Rey, Florence De Grancey
arXiv categories: cs.LO, cs.AI, cs.SC

Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming. However, they do not support classical negation in the rule component, limiting their ability to represent explicit negative knowledge. This limitation is particularly significant in safety-critical applications, where reasoning often requires explicit negative information rather than interpreting the absence of information as evidence of absence. To address this issue, we introduce an extension of Hybrid MKNF that supports classical negation in the rule component. We formally define the syntax and semantics of the extended language and present a general procedure for computing its well-founded model.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T11:48:45Z
Felix Weitkämper
arXiv categories: cs.AI, cs.LO, cs.PL

Motivated by challenging modelling issues in the life sciences, we investigate the relationship between logic programming semantics and the eventual states of causal processes compatible with those logic programs. More precisely, we show that while stable models of positive logic programs correspond to the eventual states of processes commencing from a neutral state and continuing undisturbed indefinitely, supported models describe the eventual states reachable from arbitrary starting points. This also contributes to the discussion of the appropriate semantics for logic programming as a causal rule language, adding a temporal perspective to recent interpretations of the stable and supported model semantics from an explanatory viewpoint of causality.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T16:29:22Z
Kai Pischke, Nobuko Yoshida
arXiv categories: cs.PL

Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typed communicating processes. Two main MPST methodologies, top-down and bottom-up, have been proposed and are integrated into a wide range of programming languages and tools. The top-down strategy starts by specifying the overall choreography of the protocol (called a global type), from which a set of local types that satisfy safety and liveness are generated by endpoint projection (EPP). Once each participant is type-checked against a generated local type, liveness of the set of typed processes is automatically ensured by construction. The bottom-up strategy directly checks whether local types inferred from processes satisfy liveness to enforce liveness of processes. Since the top-down strategy depends on global types and the EPP algorithms, it has often been considered that the top-down system offers strictly less typability than the bottom-up system. Our paper negates this belief. We prove that, using the precise subtyping for the subsumption rule, the top-down strategy offers exactly the same typability as the bottom-up system. More precisely, a multiparty session $M$ is typable and verified to be live by the bottom-up typing system if and only if $M$ is typable by the top-down typing system. The key to the proof is a principal global type inference algorithm which builds a principal global type from an arbitrary set of live local types. We have implemented the global type inference algorithm together with projection, process type checking and local type inference algorithms, and built a toolchain for both the top-down and bottom-up strategies. We evaluated our toolchain with representative examples from the literature, confirming that the top-down approach is more efficient than the bottom-up approach.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-23T20:27:08Z
William Gaudelier, Albert Cohen, Dumitru Potop Butucaru
arXiv categories: cs.PL, cs.LG

Previous work has shown that the simple dataflow primitives of the Lustre language allow the natural, semantically unambiguous, and compact representation of machine learning (ML) applications, including models featuring complex conditional execution and recurrent state. The Lustre clock calculus is responsible for the static determination of important properties such as liveness (absence of deadlocks) and static memory bounds. Yet existing clock calculi are tailored for embedded control applications. We show they do not cater for the representation of control patterns commonly found in training algorithms, resulting in cumbersome expressions and inefficient compilation. We propose a conservative extension of Lustre's clock calculus addressing this limitation, thereby facilitating the embedding of ML models in reactive applications.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-26T09:07:27Z
Frédéric Dabrowski
arXiv categories: cs.PL

Synchronous reactive programming gives reactive systems a deterministic temporal structure by organizing execution into logical instants and signal-based communication. Boussinot's synchronous reactive model extends this setting with cooperative threads, broadcast signals, and dynamic processes; ReactiveML brings that model into a strict, typed, higher-order functional language. This paper studies whether the same core mechanisms can be reconstructed inside ordinary OCaml 5, rather than exposed by a dedicated language extension. We present Tempo, a library runtime based on algebraic effects and deep handlers: effect operations delimit reactive suspension points, and the handler reifies captured continuations as tasks scheduled by logical-instant semantics. A comparative study with ReactiveML quantifies the overhead of this library-level reconstruction and identifies the runtime mechanisms that dominate its cost.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-26T14:07:38Z
Andrew M. Pitts
arXiv categories: cs.LO

We give a new notion of displayed setoid (family of setoids) in intensional type theory. It is used to give a semantics for extensional type theory with universes (ETU) within safe Agda, which serves as a machine-checkable formalization of intentional type theory augmented with a universe closed under inductive-recursive definitions (IRU). The syntax of ETU is defined in IRU in a traditional extrinsic form, using a well-scoped locally nameless representation of its terms. Giving its semantics in terms of displayed setoids is complicated by the very limited means of expression afforded by IRU. As a corollary we obtain a proof within IRU of the consistency of ETU.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-26T18:31:46Z
Matteo Acclavio, Giulia Manara, Fabrizio Montesi, Xueying Qin
arXiv categories: cs.PL

The Endpoint Projection (EPP) theorem is a cornerstone of choreographic programming. It states that every choreography can be projected to a network of processes that correctly implements it. Proving EPP is notoriously difficult, and existing proofs are complex and non-modular because of the mismatch between the global view of choreographies and the local view of processes. In this article, we show how to reconcile this mismatch by designing a new semantics for choreographies that is built on the local view of processes, as well as a new preorder relation between choreographies and networks that extends bisimulation to deal with the propagation of knowledge of choice among distributed processes. As a result, we can give a modular proof of EPP, which is conceptually simpler than existing ones and also provides better insights on the theory of choreographic programming.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-21T06:46:08Z
Jungin Rhee, Minseong Jang, Jaewoo Kim, Jeehoon Kang
arXiv categories: cs.PL, cs.AR

High-level synthesis (HLS) raises the abstraction of hardware design from concurrent register-transfer level (RTL) programs to sequential programs. Among the forms of parallelism HLS exploits, pipelining demands fine-grained control over pipeline structure and hazard resolution to achieve competitive power, performance, and area (PPA). However, existing tools either lack such control or sacrifice sequential semantics to provide it. We present an HLS tool that embeds fine-grained pipeline control in a sequential programming model, enabling rapid design-space exploration. The tool builds on visibility control, a novel programming abstraction that unifies hazard resolution strategies including stalling, bypassing, speculation, deferred commit, and register renaming. We evaluate on in-order RISC-V cores, histograms, and an AES accelerator. On RISC-V cores, we implement stall, bypass, speculation, and register renaming; on histograms, we implement scheduling strategies that previously required RTL or concurrent programming models. Compiled pipelines outperform HLS tools with sequential semantics and achieve PPA comparable to hand-written RTL.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-21T10:36:17Z
Zhonghua Yi
arXiv categories: cs.PL

Detached semantic facts about opaque native providers do not by themselves justify compiler rewrites: rewrite authority must be confined to the accepted fact, selected provider and build, caller, callback environment, observation, and runtime target. We present a build-authorized path-effect interface that enforces this boundary through fail-closed authorization and link receipts. The design separates receipt closure, callback-environment closure, and projection identity, and passes accepted facts to LLVM through a narrow internal API. We use one-hop topology-load reuse as a minimal observable witness of authority, not as the optimization target. A conservative LLVM consumer reuses a pointer observation only from a noalias root or one constant nonzero projection. Rocq models prove conditional refinement and authority non-amplification under explicit effect, alias, compiler/ABI, and target-resolution premises. We instantiate checked production with Toka: a source-summary gate emits exact LLVM IR, a separate IR checker accepts only a bounded topology-preserving subset, and only accepted IR is compiled into the receipt-bound provider object. A bounded static Darwin/arm64 profile also checks the final direct branch target. Across issuer-declared readv, recvmsg, and Cairo boundaries, authorized IR retains each opaque call, reduces the relevant loads from two to one, and preserves observed results; mismatched providers, builds, callbacks, projections, and unsupported IR remain neutral. A libjpeg case is rejected because its callback environment is open, while a bound callback singleton demonstrates the supported closure rule. The contribution is a checked deployment-compiler boundary with an explicit trust and applicability frontier, not a uniquely expressive effect encoding or a new load-elimination algorithm.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-22T14:13:21Z
Enrique Gallifa-Tronch, João Barbosa, Santiago Escobar
arXiv categories: cs.LO

Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it possible to detect type errors in both programs and queries dynamically.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-22T15:12:37Z
Cristian Grozea, Marius Popescu
arXiv categories: cs.LO

This article presents ASPIC, a new proof-of-concept library that converts extended syntax ASP-Core-2 programs to Picat predicates that can be solved right away with the integrated Picat SAT solver, or embedded in larger Picat programs ("ASP in Picat"), and that can in turn make use of various Picat predicates and functions ("Picat in ASP"). The first tests prove good compatibility with clingo, on programs lacking positive loops and when the special Picat features are not used. With the embedded Picat, it touches the application field of clingcon as well, by being able to efficiently model with both ASP atoms and with finite domain variables, but goes beyond that by being able to model also non-linear constraints.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-22T20:40:45Z
Charles Wade, Devon Beck, Robert MacCurdy
arXiv categories: cs.GR, cs.PL

Computational fabrication workflows increasingly require designers to specify spatially varying behavior, appearance, material composition, and process state. Yet most workflows force these intentions into printer-specific representations, such as material fractions, voxel labels, mesh partitions, or slicer settings. This coupling makes heterogeneous designs difficult to reuse because each backend requires a different realization of the same property. We present a compiler architecture for heterogeneous fabrication that treats design as a staged, typed lowering problem. A source design consists of implicit geometry and named, typed spatial attribute fields over a shared object domain. These attributes may encode measured data, visual appearance, target mechanical behavior, material recipes, process parameters, or other user-specified attributes. Translation models derive compiler-required realization attributes from source or intent attributes, and backend compilers emit machine-facing outputs such as voxel material stacks, process G-code, or configured slicer project files. This separates source modeling, attribute translation, and backend compilation, allowing a design to remain expressed in fabrication-agnostic terms while each toolchain determines how intent becomes executable instructions. We validate the method through fabricated objects and measurements across sampled volumetric data, CT-derived visual and mechanical models, Shore-hardness fields, and full-color fields, implemented via material jetting and material extrusion. These results show that one source design can be lowered into distinct material, process, and slicer representations without rewriting it in printer-specific terms. We provide the representation, translation framework, compiler interface, and workflows as an open-source Python package to accelerate research in heterogeneous computational fabrication.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-22T22:42:34Z
Yunhai Wang, Kecheng Lu, Junhao Chen, Alper Sarikaya, Chenglong Wang
arXiv categories: cs.HC, cs.PL

We present Flint, an intermediate language that enables authors to create high-quality visualizations from concise, semantics-driven specifications without explicitly configuring low-level parameters such as scales, axes, and formatting. Unlike prior systems that infer default configurations from surface-level data representations, often producing brittle choices, Flint introduces a hierarchical data semantic model that allows users to specify the meanings of data fields structurally and helps the compiler derive appropriate visualization configurations. From a concise specification, the system generates and optimizes library-agnostic visualization configurations and translates them into complete, executable specifications for multiple target grammars, including Vega-Lite, Apache ECharts, and Chart.js. We demonstrate that Flint simplifies the authoring process without compromising on visual quality, and it is an effective intermediate language for both humans and AI agents to create visualizations.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-23T11:17:08Z
Ricardo Brancas, Pedro Orvalho, Carolina Carreira, Vasco Manquinho, Ruben Martins
arXiv categories: cs.LO, cs.SE

Automated feedback tools for logic programming education depend on realistic bug datasets that reflect the mistakes students actually make. However, existing mutation testing frameworks for Prolog treat all mutations as equally likely, producing synthetic faults that diverge from classroom reality. We present an empirical study of 7,201 Prolog submissions from 265 undergraduate students, from which we derive a fine-grained taxonomy of student bugs through manual classification of 200 bug-fixing submissions. Guided by this taxonomy, we develop LogMorph, a data-driven mutation tool whose 17 operators are weighted according to the observed error distribution. LogMorph enumerates valid mutation sites on the abstract syntax tree, samples operators proportionally, injects faults, delegating to an SMT-based synthesizer when new code fragments are needed, and validates each mutant against a reference test suite. An evaluation of 16,000 generated mutants shows that the synthetic error distribution closely matches the student distribution, with most bug categories agreeing to within two percentage points. We identify cut-related mutations and synthesizer-generated code as the main sources of residual divergence, and outline how combining the SMT back-end with a language model fine-tuned on student code can further improve realism.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-23T11:17:41Z
Nicos Angelopoulos, Jan Wielemaker
arXiv categories: cs.LO, cs.AI, cs.DB, cs.SC

Chess is a two player strategic game that is embedded in classical AI culture as it was once the frontier for intelligent behaviour. There was the silent assumption that the advent of computer engines that play better than the best humans will extinguish interest in the game. However, the opposite has come to pass, with a growing following for the game. A lot of the computational resources are now centered around training of players, where the engine output is just one aspect. Access to past games is also an essential part, both in knowing what games a specific player has played previously, and also which continuations at a certain position have led to victory more often for each of the two colour players. We present Chess_db a suite of logic programming tools that can effectively manipulate games both in memory and via creating back end databases. In particular, we provide versatile code that creates databases from PGN (portable game notation) game files and explore the suitability of open source key-value databases for storing position tables that provide near-instant access to information pertaining to substantially large number of games.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-26T09:17:26Z
Fabio Aurelio D'Asaro
arXiv categories: cs.LO, cs.AI, cs.LG

FastLAS is a scalable system for Inductive Logic Programming (ILP): you give it some background knowledge, a language bias, and a set of examples, and it searches for a set of logic program rules (a hypothesis) that explains the examples. These notes are a hands-on introduction to writing FastLAS programs. They are organised as a programmer's guide: syntax first, then a ladder of worked, numbered examples of increasing difficulty. Every self-contained example here has been run against FastLAS 2.2.0 and shows the tool's actual output. We keep theory to the minimum needed to write correct programs; throughout, set-off notes flag where FastLAS differs from its sibling system ILASP, and where the two learning algorithms (--opl and --nopl) behave differently. The document is intended as an unofficial tutorial to FastLAS 2.2.0, not as an official language specification.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-26T14:09:58Z
Keren Zhu
arXiv categories: cs.LO

Logic synthesis has evolved from compact two-level minimization to large multilevel flows with many interacting optimization operators. Recent work has invested substantial effort in sequencing these operators: actions are commonly treated as opaque choices in a rapidly expanding search space, while learned circuit representations and heuristic or local-greedy orchestration provide increasingly informed ways to explore it. A central obstacle is the operator vocabulary itself. Production operators are numerous, span different representations and mathematical foundations, and expose behaviors determined by implementation-level guards, bounds, and update order. We address this gap through agentic source analysis, using LLM agents to formulate operator-level relations from pinned ABC and mockturtle implementations and adversarial audits to test their stated scope. The resulting certified relations yield theory-derived operator compression: 40 deployed recipe actions collapse to a 31-action exact Pareto cover, and source-level conditions compile into deterministic admission gates. We integrate these gates directly into ABC Orchestrate to form TACO. Two exact gates reduce Orchestrate runtime by 11% with bit-identical outputs on 66 circuits. In a held-fixed integrated comparison, TACO uses fewer nodes on 14 of 16 circuits, with geometric-mean reductions of 1.0% in nodes and 3.2% in levels, while running 2.6x faster. TACO-max achieves an NDP geometric-mean ratio of 0.903 on HeLO's three exact-input rows.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE relevance selection · published 2026-07-20T07:52:36Z
Yitao Wu, Si Shen, Rui Yang, Hong Peng, Bin Hu
arXiv categories: cs.AI, cs.SE

Verify-repair loops are a standard means for large language model (LLM) agents to correct faulty plans in code generation, mathematical reasoning, and tool use. When both the verifier and the repairer are noisy, repair can damage already-correct plans, and reported acceptance keeps rising while true validity falls, so existing methods lack a principled basis for deciding when repair should stop. We propose VRR-Stop, a robust stopping framework for noisy verify-repair-repeat (VRR) loops. A four-parameter noise model separates verifier false acceptance and false rejection from the repair and damage behavior of the repairer. Belief filtering turns repeated verification votes into an estimate of committed validity, and the loop commits or repairs according to the sign of the true marginal gain, which requires only sign identifiability rather than accurate recovery of all parameters. When verifier discrimination approaches zero, calibration itself fails and estimation error can flip the stopping sign, so we pair VRR-Stop with VRR-Guard, an estimation-free fallback that replaces the incumbent candidate only under a sufficient verification margin. On a GSM8K stress setting, VRR-Stop improves final true validity by 60.6 percentage points over fixed five-round repair at an average cost of 0.72 repair rounds. Across settings, stopping reliability is governed jointly by verifier discrimination and the decision margin rather than by the absolute size of estimation error.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-20T10:11:53Z
Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen
arXiv categories: cs.PL, cs.AI, cs.LG, cs.MA

ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic nondeterminism and externally visible actions while preserving a direct programming style. We present the core design of ETAS. Its static semantics assigns ordinary types through spec conformance and tracks each computation with two behavioral indices: an escaping effect row and a persistent abstraction of the typed action trace it may request. Specs form a terminating compile-time constraint calculus: type specs provide evidence for polymorphism and resource facts, callable specs constrain function and stage shapes, and trace specs express allow, deny, and temporal constraints. Typing checks requested traces against compiled monitors and emits residual obligations when dynamic resources preclude a complete static proof. The dynamic semantics distinguish requested, handled, denied, and committed events; handlers interpret typed actions without making their requests invisible to authorization or audit. We formalize a core calculus and state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We also implement ETAS in Rust with a command-line interface, typed HIR checks, effect and policy diagnostics, handler checks, and trace-aware execution hooks. ETAS provides a programming-language foundation for reasoning about authorization, nondeterminism, recovery, and audit evidence before and during agent execution.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-20T10:15:32Z
Shuoming Zhang, Ruiyuan Xu, Haofeng Li, Qiuchu Yu, Yangyu Zhang, Chunwei Xia, Xiaobing Feng, Chenxi Wang, Huimin Cui, Jiacheng Zhao
arXiv categories: cs.PL, cs.AI, cs.LG

Large language models now write a growing share of the world's code, increasingly inside agents and serving systems that compile, execute, or dispatch generated code without line-by-line review. This works well for mainstream languages but remains brittle for low-resource programming surfaces such as domain-specific languages, custom library APIs, and command-line tools. Even under grammar-constrained decoding, a model can still produce references invalid in the current environment: a buffer never declared, a column absent from the schema, a function the library does not provide, or an unsupported CLI option. This paper introduces decode-time grammars: grammar fragments instantiated during generation from a runtime environment Gamma. A region-specific policy selects a fragment for each hole, and a tightening operator replaces open reference positions with Gamma-typed slots whose candidates are exactly the names, fields, APIs, or options available at that point. Newly generated declarations enter Gamma before later regions are decoded, so the constraining grammar can depend on the prefix already generated. This ensures not only grammatical correctness but also semantic correctness, by preventing references to undefined symbols. We formalize grammar fragments as environment-indexed grammars ordered by refinement, prove No-Ghost soundness for Gamma-slotted fragments, show that refinement preserves this support-set guarantee, and characterize the boundary of mask-enforceable properties. We implement the approach in gproj with offline grammar induction and online policy resolution. Across TileLang, SQL, and P4, with models from 0.6B to 236B parameters, gproj eliminates ghost references by construction at moderate overhead over standard constrained decoding.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE relevance selection · published 2026-07-20T16:53:05Z
Jinhan Kim, Samuele Pasini, Paolo Tonella
arXiv categories: cs.SE

Retrieval-Augmented Generation (RAG)-based systems\footnote{For brevity, RAG-based systems are referred to as RAG systems throughout this paper.} are increasingly deployed in high-stakes settings where correct behaviour depends not only on the language model but also on the retrieval component that selects external documents at inference time. While existing RAG evaluation metrics assess retrieval and generation quality on a per-query basis, typically relying on query-level test oracles such as reference answers or relevance annotations, they provide limited insight into whether a test suite adequately exercises the retrieval behaviour of the system as a whole. In this paper, we introduce Chunk Coverage (CC), an oracle-independent test adequacy criterion for testing the retrieval component of RAG systems. CC measures the fraction of corpus chunks that are retrieved at least once across a test suite, providing a structural view of which parts of the retrieval space have been exercised. We further show how CC can be used to guide test selection and generation by prioritising queries that expand coverage of previously unexercised retrieval regions. We evaluate CC on clinical and financial RAG system scenarios. CC-guided testing reaches 50% of attainable coverage 1.7x faster than random selection and 4.2x faster than redundancy-biased strategies. Moreover, CC improves fault detection effectiveness (APFD) by 10% to 25% over random, indicating earlier discovery of distinct retrieval faults. These results show that CC captures retrieval diversity relevant to effective testing without requiring test oracles.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE relevance selection · published 2026-07-21T05:07:22Z
Ruogu Yang, Yifeng He, Yundi Xu, Yuqing Wei, Hao Chen
arXiv categories: cs.SE

Manually writing unit tests to uncover functional bugs in software libraries is not only time-consuming but also requires a deep understanding of the intended semantics of the APIs. Heuristic-based test generation methods suffer from low usability because they cannot reason about program semantics or interpret source code and documentation as humans do. Traditional fuzzing techniques like OSS-Fuzz often rely on crashes to detect bugs, but functional bugs do not always cause crashes. To overcome these limitations, we present LISA, a novel LLM-based invariant testing framework for software functional bugs. LISA iteratively generates API sequences and program invariants guided by API n-gram feedback, achieving higher bug-detection rates and competitive code coverage compared with both fuzzing and prior LLM-based test generation approaches, and reporting each finding as a high-confidence bug candidate for developer confirmation.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-21T07:57:17Z
Qunhui Zhang
arXiv categories: cs.PL

Large language models increasingly read and act on enterprise data, but SQL gives a late error signal: hallucinated fields or relations can execute and return plausible wrong answers, while incorrect writes cannot be safely assessed after execution. We present VirtualSet, a live, receiver-typed ontology-world interface and generation target for LLMs. Instead of SQL, the model emits set expressions over entity-edge worlds. Generic Constraint Projection (GCP) checks expressions before execution, while future this preserves concrete receiver types through collection chains, turning invalid fields, edges, receivers, and actions into token-anchored type errors. Type-clean reads use a SQL fast path or bounded stream interpretation, with a parity oracle checking both paths over the exercised operator space. The same substrate supports guarded decisions: actions run first in a simulated world, and world-change events require external approval before actualization. On BIRD, we lift relational schemas into typed worlds and compare VirtualSet with direct SQL while holding the model, evidence, values, zero-shot setting, timeout, glossary, repair/voting, and grader constant where possible. On a frozen 1,072-question split, VirtualSet achieves 67.5% accuracy versus 63.5% for glossary-matched direct SQL with repair and voting (+4.0 points; McNemar exact p = 0.00117) using deepseek-reasoner. Full-corpus analysis finds no engine mis-computation of a type-clean expression; remaining errors arise from model semantics or gold defects. In a 30-body guard corpus, the write chain intercepts 20/20 hallucinated action bodies with zero false positives. VirtualSet thus remains competitive on SQL's home benchmark while providing pre-execution semantics for guarded decisions.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE relevance selection · published 2026-07-21T19:01:59Z
Vidyut Sriram, Saatvik Pradhan, Suman Saha
arXiv categories: cs.SE, cs.AI

Large language models can generate C code from natural-language descriptions, but resulting programs often contain security vulnerabilities and compilation errors, posing risks for embedded and resource-constrained systems. This work investigates how feedback and retrieval improve reliability of LLM-generated C code. We present an analysis-and-repair workflow that combines compilation diagnostics, CodeQL static analysis, and KLEE symbolic execution with retrieval of prior repair patterns for iterative refinement. Evaluated on 5,000 C programming tasks exercising embedded relevant vulnerabilities, baseline models show substantial reliability gaps, with compilation failure rates up to 46% and security defect rates up to 49%. Our approach improves both metrics. For CodeLlama 7B, security defect rates decrease from 49% to 19% and total CodeQL errors drop from 15,088 to 2,463 (83.7%). For DeepSeek Coder 1.3B, compilation failures are reduced from 42% to 22% and security defects from 35% to 15%. These results show that integrating lightweight analysis tools can improve the safety of LLM-generated code for embedded development.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-22T04:11:03Z
Yeonseok Lee
arXiv categories: cs.LO

The Korean criminal justice system utilizes summary proceedings (guyaksik) to expedite high-volume minor infractions, such as simple driving under the influence (DUI), unlicensed driving, and minor traffic casualties. Although this mechanism improves judicial throughput, processing these cases creates a substantial administrative burden for prosecutors, driving the need for automated systems that can precisely translate unstructured legal text into deterministic statutory outcomes. While recent Large Language Models (LLMs) excel at semantic extraction, their probabilistic nature inherently limits their reliability in Legal Judgment Prediction tasks. Specifically, when confronted with the arithmetic constraints of legal statutes, LLMs can produce hallucinations. Given that legal accountability permits virtually no tolerance for stochastic errors, purely neural architectures remain limited in their direct judicial applications. To address these limitations, we propose a Neuro-Symbolic framework that bridges unstructured legal facts with formal verification. Our architecture restricts the LLM exclusively to semantic extraction, while offloading statutory fine calculations to a Satisfiability Modulo Theories solver. This division of labor reduces hallucination risks during computation. Furthermore, we incorporate a Human-in-the-Loop verification scheme to preserve professional legal oversight. We formalize the 2026 Sentencing Guidelines for Traffic Offenses within this pipeline, demonstrating a deterministic approach to supporting summary indictments.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · cs.SE relevance selection · published 2026-07-22T06:20:36Z
Shichen Huang, Zhenghe Jiang, Yi Jiang, Ling-I Wu, Jingyang Li, Guoqiang Li
arXiv categories: cs.SE

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines, as well as a production-grade handwritten mutation-testing suite. Ablation studies confirm that each pipeline component is critical to the framework's overall effectiveness.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-23T11:15:19Z
Akihiro Takemura, Katsumi Inoue
arXiv categories: cs.AI, cs.LO

Neurosymbolic (NeSy) systems integrate neural networks with logical reasoning to achieve both generalization and interpretability, but recent work has shown they are susceptible to shortcut reasoning behaviors. We propose a novel method using matrix-based differentiable logic programming to mitigate reasoning shortcuts in two phenomena: constraint satisfaction shortcuts, where constraints are satisfied without achieving the intended task, and cognition shortcuts, where biased data leads to semantically incorrect concept mappings despite logically sound inference. Building on recent matrix-based logic programming semantics, we introduce design elements to mitigate shortcuts, including a unified encoding of rules and constraints in a single matrix. We also identify connections to fuzzy logic t-norms and empirically compare their gradient flow properties. Through carefully designed experiments on MNIST variants, we show that one-to-one grounding of neural outputs to logical atoms significantly reduces both shortcut types compared to previous methods that rely on soft probability distributions. We then confirm that architectural choices in coupling symbolic knowledge with neural learning play a critical role in shortcut mitigation.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-23T11:17:58Z
Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof
arXiv categories: cs.LO, cs.AI

Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem Prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-23T13:31:05Z
Yan Huang, Xubing Hao, Xiaojin Li, Rashmie Abeysinghe, Xiaoqian Jiang, Licong Cui, Guo-Qiang Zhang
arXiv categories: cs.LO, cs.AI, cs.ET

The reliance on unstructured free text for documenting clinical trial protocols creates a significant barrier to automated reasoning, cohort discovery, and trial simulation. The lack of formal structure obscures critical temporal phenotypes, such as dynamic eligibility criteria and event timing constraints. Although Temporal Ensemble Logic (TEL) offers an expressive framework for modeling these elements, manual encoding remains a prohibitive bottleneck. We introduce the CT-TEL workflow: a scalable pipeline leveraging Large Language Models (LLMs) to translate narrative clinical protocols into TEL formulas. We applied CT-TEL to generate logical models for 23 real-world trials from ClinicalTrials.gov. We evaluated translation fidelity via a back-translation approach, using LLMs to convert TEL formulas back into natural language and measuring semantic similarity against source texts. The resulting semantic retention suggests that LLMs may offer a pathway for mapping informal protocols to computable logic, providing preliminary evidence toward scalable clinical trial emulation within the emerging "Symbolic Biomedicine" paradigm championed by the corresponding author.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-24T18:00:00Z
Moein E. Samadi, Andreas Schuppert
arXiv categories: cs.LG, cs.AI, cs.LO, stat.ML

Hybrid mechanistic/data-driven models, which combine first-principles with learned components, are increasingly used in process engineering and scientific machine learning. Common hybrid modeling designs are specified primarily through their architectures and training losses, which offers a limited basis for a shared semantic interface to compare or verify them across domains, with comparatively little attention paid to epistemic uncertainty in the mechanistic part. We bridge hybrid modeling and neuro-symbolic (NeSy) AI by reconstructing these designs as instances of NeSy interface. The resulting translation, Hybrid-to-NeSy (H2N), places mechanistic knowledge on the language side, learned modules on the belief side, and validity domains together with constraints on the logic side. For each design, H2N then yields an explicit NeSy inference functional and a logic-belief decomposition. From this decomposition we derive two metrics: structural violation rate (SVR), measuring whether the learned belief respects the mechanistic structure; and belief dispersion (BD), measuring how concentrated the learned plausibility is, serving as a hybrid model's epistemic uncertainty in its mechanistic part. We instantiate H2N on a case study of a structured hybrid model for binary classification under label noise and show that models with higher SVR and BD exhibit greater variability in held-out accuracy. Under structural distribution shift, H2N further quantifies a model's uncertainty during extrapolations, whereas test accuracy reveals the same shift only post hoc.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-25T03:24:05Z
Zirong Chen, Meiyi Ma
arXiv categories: cs.AI, cs.LO, cs.SC

Chain-of-thought (CoT) prompting enables large language models (LLMs) to tackle multi-step reasoning tasks, yet the generated intermediate steps are not guaranteed to be logically sound. We present Reason Popper-ly, a neurosymbolic framework that uses inductive logic programming (ILP) to learn relation composition rules from reasoning traces and deploys them as an online verifier for step-level correction. Given an LLM-generated trace, the method checks each inferred step against the learned rule table, diagnoses the violation type, rewrites incorrect steps with symbolically derived repairs, and regenerates the remaining suffix so that the model can produce its final answer conditioned on a verified trace. We evaluate on CLUTRR, a multi-hop kinship reasoning benchmark, using five language models over reasoning chains of 2 to 10 hops. Across all models, Reason Popper-ly consistently improves terminal accuracy over standard CoT, with gains of up to 48 percentage points for small models and 15 points for frontier models on the longest chains. Compared with a fully exogenous symbolic pipeline, our method performs better on harder instances by preserving the model's successful grounding while correcting only verifiable reasoning failures. In addition, step-level ILP verification yields a fine-grained error taxonomy that provides diagnostic insight beyond final-answer accuracy.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-25T07:49:38Z
Dongjie Chen, Ping Zhao, Bohua Zhan, Yulong Wang, Shushu Chen, Liangjun Feng, Hao Zhou, Min Shen, Linmu Wang, Weijia Sheng, Xiangyu Wei, Weijie Ding, Jianhui Huang, Yaoqing Gao
arXiv categories: cs.AI, cs.PL

Recent advances in large language models (LLMs) have enabled automated kernel generation and optimization, but most existing approaches rely on surface signals such as compilation feedback and profiling metrics. These signals reveal that a kernel is slow, but not why the backend compiler fails to realize a profitable optimization, especially on emerging accelerators such as NPUs. We therefore formulate kernel optimization as a progressive cross-layer diagnosis problem that links runtime symptoms to IR structure and compiler behavior before rewriting source. Based on this insight, we present our system, a compiler-grounded and hierarchical optimization framework for Triton kernels. the system escalates from lightweight pattern triage and profiling diagnosis to IR attribution and compiler-grounded analysis only when deeper evidence is needed, then proposes evidence-backed source-level rewrites. We implement the system on Triton for Ascend NPUs and evaluate it on 37 successfully converted entries from a standardized NPUKernelBench-derived Ascend 950 benchmark. Across these entries, the system attains a geometric-mean speedup of 4.35$\times$ and a median speedup of 2.73$\times$ from the initial to optimized Triton kernel; 22/37 exceed 2$\times$ and 13/37 exceed 5$\times$. The complete distribution ranges from near-baseline entries to large wins, motivating transparent reporting of the current system's scope and limitations.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-26T08:02:20Z
Nikolaos Kekatos, Stylianos Basagiannis, Panagiotis Katsaros, Alexios Lekidis, Tom Nianios
arXiv categories: cs.CR, cs.AI, cs.LO, cs.RO

Swarms of LLM-assisted autonomous robots are increasingly proposed for cooperative intelligence, surveillance, and reconnaissance (ISR) in contested environments. A growing class of their assurance failures arises not within any single platform but across the swarm: individually-compliant actions compose into a mission-level violation: a prohibited objective split across platforms to evade per-platform lim- its, or a collective budget quietly exceeded. Per-platform guardrails miss these by construction, and contested communications let the violation hide behind lost or delayed evidence. We present a three-tier (platfor- m/squad/mission) compositional runtime-verification framework that de- composes a mission policy into per-agent and cross-agent aspects, aggre- gates per-platform verdicts over a verification-aware messaging fabric, and fuses them with an evidence-aware, two-axis (security x complete- ness) algebra whose provenance names the platforms that jointly trig- gered a violation. Because the fabric makes evidence loss and silence observable, unsupported negative verdicts are downgraded to an explicit unknown rather than reported as mission-wide all-clears. On a simulated ISR mission, an indirect prompt injection that causes real LLM planners to split a prohibited collection task across four platforms is invisible to every per-platform monitor yet detected compositionally with full prove- nance; under an injected fault campaign a best-effort central monitor emits silent false all-clears while the verification-aware fabric emits none

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-20T21:58:13Z
Mikhail Babin
arXiv categories: cs.DM, cs.CC, cs.LO

A finite closure system on a finite set $U$ is a family of subsets that contains $U$ and is closed under intersections. It can be specified in two elementary ways: an implicational specification lists rules $A \to b$ and consists of all $X \subseteq U$ satisfying every rule, while an intersection specification lists subsets $M_1, \ldots, M_t$ and consists of all intersections of subfamilies of that list. We ask whether one specification of each kind defines the same family. This question has remained open in several guises for about thirty years: Khardon (1995) showed that translating between Horn formulas and their characteristic models is equivalent to deciding completeness of a proposed list of characteristic models, leaving the exact complexity open; at ISAAC 2025, enumerating irreducible closed sets from implications was still described as "widely open," even for acyclic convex geometries; closely related questions concerned pseudo-intents and the Duquenne-Guigues basis in Formal Concept Analysis, and functional dependencies and Armstrong relations in databases. We prove that the equivalence test is coNP-complete. Hardness holds for acyclic implications with premises of size at most three, even when every listed subset is correct and none can be removed without changing the closure system generated by the list; the hard part is deciding whether a required set is missing. Unless $P = NP$, the complete canonical lists cannot be generated in time polynomial in the input plus the total output size, even for acyclic convex geometries. Through standard correspondences, the theorem makes Characteristic Models Identification and FD-Relation Equivalence coNP-complete and rules out output-polynomial algorithms for Horn characteristic models, all pseudo-intents of a given formal context (equivalently, its Duquenne-Guigues basis), and premises of minimum functional-dependency covers.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-22T10:31:13Z
Huong Vu Thanh, Duc Dao Van, Khanh To Van
arXiv categories: cs.LO

The radio $k$-labeling (or $k$-coloring) problem seeks a minimum-span assignment of nonnegative integer labels to the vertices of a connected graph $G$ such that $ |f(u)-f(v)| \ge k+1-d(u,v) $ for all vertex pairs. Although numerous theoretical constructions and some heuristic algorithms have been proposed, existing approaches generally fail to provide certified optimal solutions for broad graph classes. This paper presents an exact SAT-based framework for radio k-labeling that combines a compact order encoding with incremental SAT solving. The proposed framework incrementally tightens the admissible span while reusing learned clauses across SAT calls, avoiding repeated formula reconstruction. Experimental results on 146 benchmark instances from nine graph families demonstrate that the proposed approach establishes 38 new best-known radio numbers while matching or improving the best-known radio numbers on 130 of the 146 benchmark instances. The proposed SAT framework outperforms state-of-the-art commercial optimization solvers, including CPLEX and Gurobi, in terms of overall solution quality, and substantially improves upon previously published heuristic methods. Furthermore, by combining the SAT frameworks with ILP models solved by CPLEX and Gurobi, the study certifies optimal solutions for 109 of the 146 benchmark instances, substantially expanding the set of radio-labeling benchmarks with proven optimality. These results demonstrate the effectiveness of incremental SAT solving as a practical exact optimization framework for difficult graph-labeling problems.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:14:45Z
Johannes Schmidt, Mohamed Maizia, Victor Lagerkvist, Johannes K. Fichte
arXiv categories: cs.CC, cs.AI, cs.DS, cs.LO

The propositional abduction problem is a well-known form of non-monotonic reasoning where we are asked to find an explanation of a given manifestation. Recently, there has been an influx of results asking more refined questions about the solution space rather than only individual solutions. For example, we might be interested in finding two solutions that are sufficiently far from each other (diverse solutions) in the solution space. In this paper we consider a related representation question where we ask if a given set of explanations S can represent any other explanation (that is, whether their symmetric difference is smaller than a given k). We first study this problem from a classical complexity perspective and obtain a complete classification. While only a handful of cases are tractable, the increase in complexity compared to classical abduction is often smaller than expected. We then study the parameterized complexity for several parameters and obtain new tractable and hard cases. Interestingly, a full parameterized complexity classification would require resolving the parameterized complexity of the covering radius problem from coding theory. To the best of our knowledge, no useful relationship between coding theory and non-monotonic reasoning has previously been established, but such connections seemingly become important when asking more complex questions about solution spaces.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:16:32Z
Katharina Engels, Jan Gruteser, Michael Leuschel
arXiv categories: cs.LO, cs.AI, cs.SE

Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, giving students direct control over the selection of proof rules. Our tool can import proof obligations from the Rodin platform and provides multiple exports: a trace file for proof replay in ProB, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to Rodin, allowing the ProB prover to be used as second chain. Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is more compact, maintainable and extensible. While a preliminary iterative deepening prover with simple heuristics is already available and useful for finding short proofs, we aim to obtain fast automatic provers in the future.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:18:34Z
Gioacchino Sterlicchio, Angelo Oddi, Riccardo Rasconi, Francesca Alessandra Lisi
arXiv categories: cs.LO, cs.AI

The growing demand for Urban Air Mobility (UAM) introduces significant challenges in airspace management, particularly within densely populated metropolitan regions. As the number of aerial vehicles-such as drones, air taxis, and helicopters-continues to rise, so does the risk of mid-air collisions and conflicts with existing air traffic and obstacles. Ensuring safe and efficient UAM operations requires robust strategic deconfliction mechanisms. We propose an Answer Set Programming (ASP) based approach for strategic deconfliction, focusing on time synchronization and route optimization for conflict-free flight plans. The solution is benchmarked against Constraint Programming (CP), emphasizing scalability and resource use. Results show that ASP offers faster execution and better scalability for small to medium cases, while CP maintains stable memory but degrades with complexity.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:19:08Z
Ngoc-Mai Pham, Trang-Linh Nguyen, Thi-Hai-Yen Vuong, Ha-Thanh Nguyen, Van-Giang Trinh
arXiv categories: cs.LO

An effective examination and test schedule for patients plays a crucial role in hospital resource management. In this work, we formulate a new reactive patient-flow scheduling problem in multi-department hospitals where walk-in patients arrive over time and each patient requires multiple examinations per visit. Upon each arrival, the scheduler computes a feasible examination pathway-both the sequence of examinations and the room assignment-for the incoming patient only, while previously scheduled assignments remain fixed. This process is subject to medical precedence constraints and room capacity limitations. We model the problem declaratively in Answer Set Programming (ASP) with clingo, and optimize a two-part cost: travel time between consecutive examination locations and queue-induced waiting time, weighted by the duration of the upcoming examination. To assess robustness under stochastic service times, we propose a Discrete-Event Simulation (DES) evaluation layer and a baseline greedy policy for comparison. On large-scale synthetic datasets across various capacity regimes and patient loads, the ASP approach reduces median stay time and increases the proportion of zero-wait patients compared to DES-based baselines. These improvements are most pronounced under heavy load, while the approach still outperforms baselines across all capacity settings, with smaller gains at higher capacities.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:19:24Z
Daimy Van Caudenberg, Alexander Ek, Carlos Cantero, Bart Bogaerts
arXiv categories: cs.LO, cs.AI

Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:20:48Z
Rafaello Sanna, William E. Byrd, Nada Amin
arXiv categories: cs.PL

We present chrKanren, a dialect of the purely relational constraint logic programming language miniKanren which includes support for Constraint Handling Rules (CHR), a language for writing rule-based programs such as constraint solvers. We show how to integrate CHR's constraint propagation mechanism into the language of miniKanren search streams such that both processes remain complete. We also use chrKanren to illustrate novel applications of constraints in miniKanren, such as semantic unification of user-defined data structures and type-and-example-directed synthesis for relational interpreters in the style of MYTH.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-23T11:21:22Z
Xiangyu Guo, Ajay Bansal
arXiv categories: cs.PL

This paper presents Constraints as Verifiers and Emitters (CaVE), a constraint storage approach for handling integrity constraints in stableKanren. stableKanren is a normal logic-program solver based on extended unification and resolution. Integrity constraints control the outcomes of goals in normal logic programs, which is critical for non-monotonic reasoning. There is no resolution-based algorithm for handling integrity constraints that can be used in stableKanren. Therefore, we design Constraints as Verifiers and Emitters (CaVE), a constraint storage that works with resolution to support integrity constraints. We discuss variants of CaVE with respect to the integrity constraints, ranging from propositional to grounded and predicate versions. We implement CaVE using Scheme in stableKanren and show a series of example normal programs written in stableKanren with integrity constraints.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-20T10:31:33Z
Toru Takisaka, Hongjie Qing, Libo Zhang
arXiv categories: cs.PL

Martingale-based methods are central to probabilistic program verification, but strong global non-negativity requirements can exclude simple certificates from tractable template classes. Relaxing this requirement enlarges the search space for automated synthesis, but naive relaxations are unsound in the probabilistic setting. We introduce lazy Streett supermartingales and their lexicographic extension, showing that weak non-negativity can nevertheless be used soundly to certify almost-sure satisfaction of $ω$-regular properties with polynomial templates under a broad class of sampling distributions, including all bounded-support distributions. This extends prior weakly non-negative methods from termination to general $ω$-regular verification. We further give a compositional account of lexicographic certificates in terms of one-dimensional ones. Experiments on 170 polynomial probabilistic-program benchmarks show increases of 20.0-23.5 percentage points in verification success over the strongly non-negative baseline.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-20T13:35:50Z
Gabriel Dengler, Carlos E. Budde, Laura Carnevali
arXiv categories: stat.ME, cs.LO, cs.PF

Importance splitting (ISPLIT) evaluates the probabilities of rare events in non-Markovian models. It requires a heuristic importance function (IFUN) that estimates the distance to the target. While including timer evaluations in the IFUN can substantially improve the effectiveness of ISPLIT, the existing time-sensitive IFUNs evaluate simulation states with respect to single sampled timer values. Thus, reaching highly important states requires simultaneously sampling specific combinations of timer values, yielding several unproductive simulation runs. In this paper, we revisit time-sensitive ISPLIT with the goal of steering simulation runs towards important states. First, we study how timer values can be resampled conditioned on the elapsed time. The importance can be evaluated by considering the set of feasible timer values, decoupling importance estimation from timer samples. Second, we exploit the global age of a simulation to identify and prune the executions that can no longer reach the target within the remaining time budget. Together, these ideas lead to a taxonomy of distance metrics clarifying the role of timer bounds, resampling, and the global age. In particular, for models with unbounded timers, we show that time-sensitive IFUNs collapse to ordinary IFUNs under resampling. Experiments demonstrate that the proposed formulations substantially improve the accuracy of ISPLIT estimators.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-22T15:09:38Z
Maxime Mahout
arXiv categories: cs.LO, q-bio.PE

The automated reconstruction of patient family history is a common challenge in genetic counseling for disease prevention. Such a family history is usually determined for a particular subset of diseases that are Mendelian, i.e. monogenic, and classified into three categories depending on the chromosome the gene is located: autosomal, X-linked or Y-linked. Mendel's inheritance laws allow for simple probabilistic modeling of the genetic transmission of monogenic disorders. Genetic counsellors use knowledge about the patient's family history and Mendelian laws for assessing risks of transmitting or inheriting congenital conditions. We present mendelprob.pl, a probabilistic logic programming algorithm in ProbLog for deriving probabilities of inheritance of genotypes and phenotypes for genes with two alleles through multiple generations. In particular, the user can input genotypes and phenotypes for a patient and its family, and automatically determine the most probable genetic family history. We illustrate the ProbLog model on practical examples of patient pedigrees from the literature and from a genetic counseling handbook. We show that our method correctly infers probability of individual genotypes from knowledge about familial genotypes, yielding the same results as tool pedprobr. However, unlike pedprobr, our approach can exploit knowledge about familial phenotypes. It can also directly distinguish between autosomal, X-linked, and Y-linked disorders, using its intuitive logical modelling. We provide our ProbLog tool for free and open-source on GitHub, making it easily available for genetic counsellors. We conclude on the importance of providing explainable formal methods for a task that clinicians might want to perform using proprietary software.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T00:06:45Z
Jack Liell-Cock, Sam Staton
arXiv categories: cs.PL, math.PR

Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete probabilistic languages. An imprecise coin flip is simply a BDD variable whose weight is left free rather than fixed. We introduce Imp, a Haskell-embedded DSL for imprecise probabilistic programming. A graded monad, indexed by finite sets of named sources of epistemic uncertainty, restores the commutativity that the standard convex powerset monad lacks, and GHC's type system enforces this at compile time. Weighted model counting is parametric in the semiring, so the same compiled BDD supports exact, differentiable, and interval-bounded inference.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T09:10:57Z
Marco Zamponi, Florian Lammel, Ezio Bartocci, Michele Chiari
arXiv categories: cs.LO

Signal Temporal Logic (STL) is a formalism used to describe temporal properties of real-valued signals in cyber-physical systems. In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck. Despite tableau-based satisfiability procedures being a natural solution to solve this problem, we have recently found out that the only existing tree-shaped tableau for bounded discrete-time STL does not provide a sound satisfiability/unsatisfiability verdict for all possible STL formulas. In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau which we prove to be sound and complete for bounded discrete-time STL. On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, checks the logical implication and equivalence between specifications, and extracts unsatisfiable cores, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced First-Order Logic and Satisfiability Modulo Theories encodings for STL, which allow it to act as a portfolio solver. We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving correctness guaranteed by our sound tableau procedure.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T11:21:39Z
Kilian Rueckschloss, Felix Weitkaemper
arXiv categories: cs.AI, cs.LO, cs.PL

Pearl famously argues that causal knowledge enables the prediction of intervention effects. By contrast, purely descriptive knowledge supports only conclusions drawn from observations. His theory of causality, however, is developed exclusively within Bayesian networks and causal models. Consequently, it is largely restricted to acyclic causal relationships, and transferring its ideas to other formalisms risks misinterpretation or inconsistency. This paper brings Pearl's approach to causality into probabilistic logic programming (PLP). To this end, such programs are aligned with philosophical foundations established in prior work that do not rely on temporal notions; that is, all relevant events are assumed to occur simultaneously. A formal causal semantics for these programs, together with a notion of intervention and an implementation, is proposed. It is shown that this semantics coincides with the P-log semantics for stratified ProbLog programs, while the two may differ in the non-stratified case and for other PLP formalisms.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T11:22:41Z
Adam Kostka, Jarosław A. Chudziak
arXiv categories: cs.LO, cs.AI, cs.MA

Existing approaches to multi-agent belief combination have established mature foundations for combining uncertain beliefs under common assumptions: consensus methods use iterative averaging, logic-based methods resolve conflicting knowledge bases, and epistemic logic analyzes agents' information states. Typically, these approaches assume that the structure determining what each agent can represent remains fixed. However, in many scenarios, agents gain or lose observational capacity during execution, and what was once admissible may become structurally impossible. This paper presents a formal framework for handling such runtime changes in epistemic partitions over continuous belief profiles. A hybrid approach exploits the advantages of answer set programming in elaboration tolerance, declarative integrity constraints, and explanations, with the numerical flexibility of Python. The framework applies to domains where agents operate at heterogeneous and possibly changing levels of resolution, and provides formal guarantees of admissibility preservation under refinement, unique mass-preserving repair under coarsening, and explanation completeness. Evaluation across 100 randomly generated topology changes confirms complete violation detection and explanation coverage.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T13:59:07Z
Jiahao Fan, Xiaojin Li, Yan Huang, Xubing Hao, Licong Cui, Guo-Qiang Zhang
arXiv categories: cs.LO

The American Academy of Sleep Medicine (AASM) Manual is the clinical standard for polysomnography (PSG) scoring, but its narrative rules can admit multiple reasonable interpretations, contributing to inter-scorer variability and implementation differences across studies and software systems. We present a formal framework for translating sleep-scoring rules into Rational Ensemble Logic (QEL), a dense-time (i.e., a continuous, rational-valued timeline rather than discrete steps) formalism that combines first-order quantification with metric temporal operators. Using an extraction-and-compilation procedure, we identified 18 unique atomic propositions and derived 12 final specifications corresponding to clinically scoreable AASM events. Back-translation of QEL specifications into clinician-facing language retained high semantic fidelity to the original scoring narratives (embedding cosine similarity: 79.3, 95% CI: 79.0--79.7) despite low lexical overlap (ROUGE-L: 18.3, 95 CI: 17.6--18.9). Formalization also clarifies latent ambiguities, including implicit physiological latencies and overlapping exclusions. This framework yields executable, rigorous rule specifications for computational phenotyping, more consistent implementation across datasets, and standardized open-source PSG analysis. This work is a part of the "Symbolic Biomedicine" program championed by the corresponding author.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-23T14:42:17Z
Yan Huang, Xiaojin Li, Licong Cui, Guo-Qiang Zhang
arXiv categories: cs.DB, cs.LO

Large sleep-study repositories contain rich time-stamped physiological annotations, but cohort discovery is still commonly implemented as ad hoc scripts or scalar-index filters. We present a logic-based temporal cohort discovery engine that brings formal semantics, model checking, specialized indexing, and empirical evaluation into a unified biomedical informatics framework. We adopt Rational Ensemble Logic (QEL) as a dense-time formal foundation for sleep-data querying and represent each annotated polysomnogram as a Biomedical Event Structure Temporal Model (BEST), a finite mapping from event labels to non-overlapping rational interval ensembles. Cohort discovery is formulated as model checking of QEL formulas over BEST databases. We organize common sleep-research requirements into three reusable temporal query patterns: single-event retrieval, dual-event temporal pattern matching, and event data extraction. The prototype cohort discovery engine was implemented in Python with in-memory and MongoDB-backed execution modes and evaluated on synthetic interval datasets containing up to 90 million intervals and on real-world National Sleep Research Resource annotations from the Cleveland Children's Sleep and Health Study (CCSHS) containing 515 subjects, 202,587 intervals, 23 event labels. 2DFC constructs indexes in linear space and linear build time, reducing build time at 90 million intervals from 11,549 s with RTFC and 23,902 seconds with 2DRT to 3,655 seconds. On CCSHS, cohort-selection queries executed at sub-second latency at native scale and under 45 seconds at 1,000 times scale. This work is a part of the Symbolic Biomedicine program championed by the corresponding author.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-20T13:25:55Z
Valentin Shehtman, Dmitry Shkatov
arXiv categories: math.LO, cs.LO

We consider products and semiproducts of propositional modal logics L with S5 and present new examples of product and semiproduct logics axiomatized in the minimal way and enjoying the product (or semiproduct) FMP. An essential part of the proof is local tabularity of these (semi)products for L of finite depth; it is obtained by using bisimulation games. These results readily imply decidability for 1-variable fragments of predicate modal logics QL and QL+Barcan formula. We also present new counterexamples, i.e. (semi)products not axiomatizable in the simplest way.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-21T08:38:24Z
Tomasz Kowalski, Katarzyna Słomczyńska
arXiv categories: math.LO

We give a generic construction of the n-generated free Hilbert algebras and Brouwerian semilattices by a uniform method applicable to any variety of Hilbert algebras or Brouwerian semilattices, as long as a manageable description of subdirectly irreducible algebras in that variety is available. A slight modification yields analogous constructions for varieties of Hilbert algebras and Brouwerian semilattices with zero. As examples we construct free algebras in varieties of bounded height and of bounded width; we also find a closed formula for the free spectrum of linear Hilbert algebras. Finally, we obtain a few results on structural completeness of varieties of Hilbert algebras with zero, in particular, we give a sufficient condition for a quasi-equation to be equivalent to an equation.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-21T10:48:02Z
Guillermo Badia, Tomasz Kowalski, Grigory Olkhovikov
arXiv categories: math.LO

The question of the expressive power of a given logical language with Kripke relational semantics has at least two dimensions: (1) what the language can say about frames, and (2) what it can say about models. The Goldblatt-Thomason theorem provides a model-theoretic characterisation of modal axiomatisability for elementary classes of frames in terms of closure under taking generated subframes, disjoint unions, bounded morphic images, and reflection of ultrafilter extensions. Goldblatt also provides a similar characterisation for axiomatisability in intuitionistic logic of classes of models rather than frames. In this article we provide analogous results for bi-intuitionistic logic, a natural expressive extension of intuitionistic logic obtained by adding a binary connective dual to the intuitionistic implication, introduced in the 1970s independently by Dieter Klemke and Cecylia Rauszer. Together with previous results, such as a van Benthem bisimulation characterisation theorem and a Lindstrom theorem, this provides a complete picture of the expressive power of propositional bi-intuitionistic logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-21T13:22:59Z
Sam Buss, Pavel Pudlák
arXiv categories: math.LO

The Student-Teacher game is an extension of Herbrand's theorem. In the game, Student and Teacher take turns giving values for existentially and universally quantified variables, and Student is allowed to backtrack to propose other values for existentially quantified variables. The game has become increasingly important for proving lower bounds on provability in theories of bounded arithmetic. In those applications, the game is played in an arithmetical theory; however, this paper studies the Student-Teacher game in the setting of pure first-order logic, so it is more closely related to Herbrand's theorem and the midsequent theorem. When played in pure first-order logic, a formula~$\varphi$ is logically valid if and only if there is a Student-Teacher game with a winning strategy for Student for establishing~$\varphi$. We present a refined version of the Student-Teacher game in arbitrary first-order universal theories and include a proof of the validity of Student-Teacher games from the sequent calculus midsequent theorem in an appendix. The game is presented as a finite tree with vertices and edges labeled by terms, and with a total order on the nodes. The totally ordered tree represents the players' interaction. Our main results show that minimal trees in the Student-Teacher game can be arbitrarily complex. Specifically, for every totally ordered tree~$T$, we construct a valid prenex formula~$\varphi$ such that every Student-Teacher game for~$\varphi$ contains $T$ as a substructure. It follows not only that there is no computable bound on the size of Herbrand disjunctions, which is a well-known fact, but also that there is no bound on their complexity in the sense that it is not possible to restrict the types of totally ordered trees knowing only the length of the formula.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-21T14:58:31Z
Ryan Tay, Harsh Beohar, Charles Grellois
arXiv categories: cs.LO

We introduce a coalgebraic extension of the higher-order modal fixed-point logic (HFL) which subsumes both HFL and its probabilistic extension. We show that the emptiness problem for non-deterministic finite automata as well as the value-1 problem for probabilistic automata reduce to model-checking problems for this coalgebraic formulation of HFL.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T03:45:03Z
Chuangjie Xu
arXiv categories: cs.LO

This paper separates two components of functional interpretations: affine information propagation and contraction. We introduce information nuclei as an algebraic interface to capture the affine component. An information nucleus specifies what information is associated with finite-type objects, how exact objects are compatible with such information, and how information is propagated through functions. From any information nucleus we obtain a formula translation and a soundness theorem for affine finite-type arithmetic. Extending soundness to finite-type arithmetic with contraction requires one additional ingredient: a formula-indexed contraction structure reducing the challenges generated by duplicated assumptions to a single challenge. Finite collections of candidates with union yield a Herbrand-style interpretation, while exact information with challenge selection yields the usual Dialectica interpretation over an arithmetic system restricted to decidable primitive formulas. The resulting framework provides a uniform method for specifying the information carried by extracted realizers, allowing existing functional interpretations to be systematically enriched with auxiliary data, such as continuity information.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T08:39:19Z
Rafael Ongaratto, Hans van Ditmarsch
arXiv categories: cs.LO, cs.MA

In this work we propose a dynamic turn in paraconsistency. We introduce AMLFI1, the action model extension of the paraconsistent logic LFI1. A special case is PALFI1, a paraconsistent logic of public announcements. It corresponds to another, recently published, paraconsistent public announcement logic: the differences in their axiomatizations are mutually admissible. We also introduce UMLFI1, that extends AMLFI1 with factual change. Soundness and completeness are proven for all logics, and all extend the epistemic paraconsistent logics KLFI1, KB4LFI1 and S5LFI1, known from the literature. With such dynamic epistemic paraconsistent logics we can formalize obtaining and resolving provisional contradictions.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T14:14:34Z
Dominik Pichler, Mirko Tagliaferri
arXiv categories: cs.LO

Robust classification is commonly understood as the stability of a classifier under small perturbations (often adversarial) of input data. In this paper, we propose a logical framework for robust classification grounded in topological semantics for modal logic. Evaluation points are feature vectors representing machine-readable objects, and formulas express explicit classifications. Robustness is interpreted geometrically as local truth persistence: a classification is robust at a point if it holds throughout some non-empty open neighbourhood of that point. Building on this perspective, we introduce a logical language with a robustness modality interpreted over S4 topological spaces, together with a robustness-sensitive conditional connective. This conditional connective captures global inclusion relations between robust regions and other properties of the classifier: it holds at a point when the neighbourhood witnessing the robustness of one formula is contained in the truth set of another. In this way, robust classifications can be systematically linked to classification conditions. We provide a sound and complete axiomatisation of the resulting logic. Finally, we introduce Minimal Robust Models, a constructive method for generating models from specified robustness constraints, which yields formal tools for analysing, explaining, and structuring robust classification behaviour.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T14:15:08Z
Jun Suzuki, Charles Grellois, Katsuhiko Sano
arXiv categories: cs.LO

This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints ($μ$IMALL) by means of its phase semantics. A classical first-order multiplicative-additive linear logic system with the least and greatest fixpoints was introduced by Baelde and Miller (2007). Its intuitionistic fragment was discussed in Baelde (2012), but the cut-elimination theorem for this fragment has not yet been proved. We introduce a propositional fragment of this system, $μ$IMALL, and establish the cut-elimination theorem. To prove the theorem, we define phase semantics for $μ$IMALL and show the following two statements: (1) Soundness: if a formula is provable in $μ$IMALL, then it is true in all phase models, and (2) Cut-free Completeness: if a formula is true in all phase models, then it is provable in $μ$IMALL without Cut. Okada (1999, 2002) employed a phase semantic method to prove the cut-elimination theorems for classical and intuitionistic linear logic systems. De et al. (2022) applied this method to a propositional fragment of classical propositional multiplicative-additive linear logic with the least and greatest fixpoints. We refine and apply their arguments to prove the cut-elimination theorem for $μ$IMALL.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T14:40:00Z
Zhicheng Chen
arXiv categories: math.LO

Fundamental logic (Holliday 2023) is a non-classical logic based only on the introduction and elimination rules for conjunction, disjunction, and negation in a Fitch-style natural deduction system, while a preconditional (Holliday 2025) is a binary operation on a bounded lattice satisfying five natural axioms and subsuming Heyting implication, the Sasaki hook on ortholattices, and Lewis-Stalnaker-style conditionals satisfying flattening. We combine the two by giving a consequence-relation presentation $\mathsf{K}$ whose algebras are exactly Holliday's bounded lattices with a preconditional, and then studying two natural extensions, $\mathsf{T}$ and $\mathsf{F}$, the latter being fundamental propositional logic with a preconditional. For $\mathsf{T}$ and $\mathsf{F}$, we prove strong completeness with respect to a purely relational semantics, using a canonical model whose points are pairs of theories, and establish the finite model property and hence decidability. Finally, following Holliday and Massas (2026), we adapt their GMT- and Goldblatt-style embeddings to fundamental logic with a preconditional. The resulting translations are full and faithful into ortho-$\mathsf{S4}$ and intuitionistic $\mathsf{KTB}$, respectively. The new conditional clauses send the preconditional to a boxed Sasaki hook on the former side and to a strict intuitionistic conditional on the latter whose classical $\mathsf{KTB}$ reading is equivalent to the Goldblatt translation of the Sasaki hook. The frame constructions follow the reduct-and-companion pattern of Holliday and Massas; the essential additional ingredient is the semantic transfer calculation for the preconditional.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-22T15:51:23Z
Raffaele Di Donna, Giulio Guerrieri, Lorenzo Tortora de Falco
arXiv categories: cs.LO

We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic (MELL) to recover a sequent calculus proof from a proof-structure. We present a geometric restriction on proof-structures allowing us to turn this necessary property into a sufficient one, computationally efficient: we can thus introduce the notable fragment VMELL of MELL for which the property is indeed a correctness criterion. The fragment VMELL brings together the classical and intuitionistic polarizations. We translate the bang calculus terms into proof-nets of VMELL, factorize the usual translations in linear logic of the call-by-name and call-by-value lambda-calculi, prove that cut elimination simulates bang reduction, and provide an explicit characterization of the bang calculus terms as proof-nets.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-23T13:44:39Z
Giuliano Rosella, Yale Weiss
arXiv categories: math.LO

A logic is Post complete if it is consistent but has no consistent proper extensions. In this article, we systematically investigate the Post complete extensions of certain basic conditional logics. We identify all of the finitely many regular and normal Post complete conditional logics, and prove analogues of Makinson's embedding theorems. We also show that certain basic conditional logics have uncountably many Post complete extensions for which closure under some, but not necessarily all, rules peculiar to the conditional are relaxed. We reflect on what our results tell us about the structure of certain lattices of conditional logics and also draw some morals for multimodal logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-24T09:19:58Z
Matthew de Brecht
arXiv categories: math.LO, math.CT

We give self contained proofs of the completeness of countable $σ$-coherent theories, for both propositional and predicate logic. By $σ$-coherent logic we mean the fragment of geometric logic that only allows countable signatures and countably infinite disjunctions. In the propositional case, each theory determines a quasi-Polish space of models, and formulas (up to provable equivalence) are interpreted as continuous functions from the space of models to the Sierpinski space. In the predicate case, each theory determines a quasi-Polish category of models, and formulas (up to provable equivalence) are interpreted as continuous functors from the category of models to the quasi-Polish category of overt discrete quasi-Polish spaces. We further extend this analogy by investigating a notion of ``sobriety'' for certain topological categories.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-25T18:29:27Z
Hafez K. D., Seyed-Mohammad Bagheri
arXiv categories: math.LO

Topological semantics for affine modal propositional logic is introduced. The interior operator on subsets is replaced with the lower semi-continuous envelope operator on functions. Completeness and affine compactness theorems are proved for this logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-26T18:50:09Z
Lutz Straßburger
arXiv categories: cs.LO

We propose a new proof theoretical method for proving Lyndon interpolation. Our proof does not use the sequent calculus but is based on a generalization of the splitting lemma in deep inference. We then formulate the interpolation theorem as a decomposition of a derivation into an up-fragment and a down-fragment. This can be seen as (i) a strengthening of the standard formulation of the interpolation theorem, and (ii) a generalization of the cut elimination theorem. We demonstrate the flexibility of our approach by applying it to linear logic, classical logic, and modal logics. For this, we also introduce novel cut-free proof systems for several modal logics in deep inference.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-21T10:24:12Z
Ruaan Kellerman
arXiv categories: math.LO, cs.LO

A tree is a partially ordered set that is downwards linear and downwards connected. A tree is called bounded when each of its paths (i.e. maximal linearly ordered subsets) contains a greatest element. In a bounded tree, each path can be defined by a first-order formula using the leaf of the path as parameter. Bounded trees can be used to model computational systems such as Zeno machines whereby the leaf of a path represents the state to which an infinitely long sequence of computations converges, or a state that is assigned to a computational sequence that loops. We identify a sufficient condition under which certain trees that are not bounded, can be elementarily embedded in trees that are bounded. Several tree operations are also given, and Feferman-Vaught style preservation properties for these operations are proved.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-21T15:34:48Z
Mervyn Tong
arXiv categories: math.LO, math.CO

We prove that $(k+1)$-uniform hypergraphs definable in an NIP strongly $k$-distal structure satisfy a homogeneous regularity lemma -- they can be partitioned into a bounded number of simplicial complexes, most of which are homogeneous (meaning that the restriction of the hypergraph to the simplicial complex is either complete or empty). Furthermore, the parts of the partition can be chosen uniformly definably, and the size of the partition is polynomial in the reciprocal of the error parameter. This extends the homogeneous regularity lemma proven by Chernikov and Starchenko for hypergraphs definable in a distal structure. We prove this by introducing $k$-strong honest definitions and showing that an NIP structure is strongly $k$-distal if and only if every formula $\varphi(x_1, ..., x_k; y)$ has a $k$-strong honest definition. This extends the theory of strong honest definitions in distal structures to the higher-arity setting.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-21T20:41:44Z
Leon Chini
arXiv categories: math.LO

This paper further studies the model companion of an endomorphism acting on a vector space, possibly with extra structure. Let $T$ be a model-complete theory that $\varnothing$-defines an infinite $K$-vector space $\mathbb{V}$. In previous work, we introduced a family $\{T^C_θ: C \in \mathcal{C}\}$ of extensions of the theory $T_θ:= T \cup \{\text{``$θ$ is an endomorphism of $\mathbb{V}$''}\}$ that parameterizes all consistent extensions of the form $$ T_θ\cup \left\{\sum\nolimits_{k}\bigcap\nolimits_{l}\operatorname{Ker}(ρ_{j, k, l}[θ]) = \sum\nolimits_{k}\bigcap\nolimits_{l} \operatorname{Ker}(η_{j, k, l}[θ]) : j \in \mathcal{J}\right\}, $$ where all sums and intersections are finite, all the $ρ[θ]$'s and $η[θ]$'s are polynomials over $K$ with $θ$ plugged in, and $\mathcal{J}$ is some possibly infinite index set. We also presented a sufficient condition that implies that every $T^C_θ$ has a model companion $Tθ^C$. In this paper, we show that, under this sufficient condition, the model companion $Tθ^C$ has $\operatorname{NATP}$, a neostability property recently introduced by Ahn and Kim, whenever $T$ does.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-22T14:13:05Z
Raul Fervari, Santiago Figueira, Gabriel Goren-Roig, Leonardo Torres
arXiv categories: cs.LO

Path Predicate Modal Logic (PPML) is a generalization of Basic Modal Logic, where atoms are relational predicates instead of propositional symbols. The study of PPML is motivated as a way to abstractly investigate data-aware formalisms, such as XPath or DataGL. In this paper, we investigate some basic model theoretical aspects of PPML to better characterize its expressive power. More concretely, we investigate different ways of defining Hennessy-Milner classes, and a van Benthem characterization theorem. In doing so, we discuss the main challenges of dealing with the novel features of PPML, and what are the similarities with the standard approaches.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-23T19:23:48Z
G Conant, C Terry
arXiv categories: math.CO, cs.LG, math.LO

We prove function-theoretic analogues of a quantitative result of Hodges on extracting the order property from a sufficiently large 2-tree coded in a binary relation. Similar analogues for functions were previously obtained by Daskalakis and Golowich and by Anderson and Benedikt. These results are from statistical learning theory, where 2-trees are captured by sequential fat-shattering dimension, and the order property is controlled by various notions of "thresholds". Our first main result (Theorem 1.11) focuses on extracting a less restrictive kind of threshold from a tree, and yields significantly better bounds compared to what can be obtained from earlier results focusing on more restrictive versions. Part of the motivation for Theorem 1.11 lies in a companion paper, where this theorem is used to obtain efficient bounds in quantitative regularity lemmas for "stable functions". Here will use Theorem 1.11 to reprove a result of Anderson and Benedikt in a stronger form and with improved bounds. We also use Theorem 1.11 to prove an at most double-exponential bound on dual sequential fat-shattering, which resolves an open problem. In our second main result (Theorem 1.14), we give a new proof of a result of Daskalakis and Golowich on extracting "tight thresholds" from large sequential fat-shattering dimension, with improved bounds. This resolves another open problem related to correcting the proof of a result claimed by Jung, Kim, and Tewari.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-23T19:23:53Z
G. Conant, C. Terry
arXiv categories: math.LO, math.CO

We prove quantitative stable regularity lemmas for binary real-valued functions, extending the work of Malliaris and Shelah for stable graphs. The statements of our results are modeled after non-quantitative theorems for stable functions due to Chavarria, Conant, and Pillay. One of the key tools in our quantitative proof is an "analytic symmetry lemma", which gives a function-theoretic analogue of the fact that a pair of good sets in a graph has density close to 0 or 1. We also develop a function-theoretic treatment of Malliaris and Shelah's random sampling method for refining partitions consisting of good sets into equipartitions.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-25T15:59:03Z
Evelina Daniyarova, Alexei Myasnikov
arXiv categories: math.LO, math.CT

We introduce projective logical geometry and prove that two algebraic structures are strongly bi-interpretable if and only if their categories of projective logical sets are equivalent relative to the class of interpretation functors, which is also equivalent to their categories of projective definable sets being equivalent relative to the class of translation functors. These constructions generalize two ideas of Boris Plotkin: the concept of geometric equivalence in universal algebraic geometry and the transition from universal algebraic geometry to logical geometry. Furthermore, our categorical approach offers a fresh perspective on the theory of interpretations, enabling us to establish a series of fundamental results using categorical methods.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-25T18:09:22Z
Mostafa Mirabi, Anand Pillay
arXiv categories: math.LO

We study a special case of a relatively categorical theory $(T,P)$, namely when $T$ is an internal cover of $T^{P}$. We give a structure theory for relatively categorical internal covers. After passing to $T^{eq}$ and naming a parameter from the $P$-part, they are precisely the "pure torsor covers" of $T^{P}$, obtained simply by adjoining a new sort $S$ for a principal homogeneous space or torsor of an $\emptyset$-definable group $G$ in $T^{P}$, and a symbol for the action. We prove that $T$ is relatively $ω$-stable (or $ω$-stable over $P$) as defined in [4] iff the dual binding group $H$ has the $DCC$ on definable subgroups.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-26T19:19:52Z
Zhentao Zhang
arXiv categories: math.LO

We prove that every group $G$ definable in the pure $p$-adic field $\mathbb{Q}_p$ is weakly regular. We show that every one-parameter subgroup is definable. We also show that its one-parameter core $G_u$, together with a suitable regular open subgroup $G_Ω$, is definable. Finally, we show that if $H$ is a dfg component of $G$, then $G_u=\langle(H^g)_u:g\in G\rangle$. In fact, $G_u$ is a finite product of the one-parameter cores of finitely many conjugates of $H$. In particular, when $G$ is definably amenable, $G_u=H_u$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-20T03:38:13Z
Logan McDonald
arXiv categories: math.LO

Cardinal characteristics of the continuum are the cardinalities of interesting families of reals. A well-studied example is that of maximal almost disjoint (MAD) families of sets of natural numbers. Significant work has been done investigating computability-theoretic analogues of cardinal characteristics. By considering encodings of MAD families as a single `universal' set, Lempp, Miller, Nies, and Soskova (2023) studied the class of encoded MAD families. Such a class is referred to as a mass problem; one can study the relative complexity between mass problems. In Section 2, we build on the study of mass problems as analogues of cardinal characteristics. We define mass problems of maximal eventually different (MED) families of computable functions in the same way and compare them against the mass problems defined by Lempp et al. In Section 3, we survey work by Greenberg, Kuyper, and Turetsky (2019) that provides an abstract framework for cardinal characteristics and their effective counterparts. We show that this framework is suitable for obtaining results in the setting of mass problems. In Section 4, we showcase a construction by Schrittesser (2018) of an effectively closed MED family in set theory. We show that the construction is sufficiently effective that the computable members of the constructed family are MED relative to computable functions.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-20T08:16:24Z
Lu Liu, Ludovic Patey
arXiv categories: math.LO, math.CO

We prove that for every non-arithmetic set~$C$ and every arithmetic finite coloring of~$\mathbb{N}$, there is an infinite set $H \subseteq \mathbb{N}$ whose non-empty finite sums of distinct elements is monochromatic, and $C$ is not $H$-computable. We also study restrictions of Hindman's theorem to simple colorings.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-21T05:36:11Z
Vinicius de Oliveira Rodrigues
arXiv categories: math.LO, math.CO

The rearrangement number $\mathfrak{rr}$ is the least cardinality of a collection of permutations of $ω$ such that every conditionally convergent real series is disrupted by some permutation in the collection. Blass, Brendle, Brian, Hamkins, Hardy, and Larson proved that $\max\{\operatorname{cov}(\mathcal N),\mathfrak b\}\leq\mathfrak{rr}\leq\operatorname{non}(\mathcal M)$ and asked whether $\mathfrak{rr}<\mathrm{non}(\mathcal M)$ is consistent. We prove that $\mathfrak{rr}<\operatorname{non}(\mathcal M)$ is consistent with ZFC. We also prove, in a different forcing extension, that $\max\{\operatorname{cov}(\mathcal N),\mathfrak b\}<\mathfrak{rr}$. We further derive consequences for the subseries number $\mathfrak{s}_{\mathrm{sub}}$ and the splitting number $\mathfrak s$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-24T04:42:01Z
Emma Dinowitz
arXiv categories: math.DS, cs.IT, math.LO, math.MG

In analogy to the point-to-set principle for Hausdorff and packing dimension of Lutz, Lutz, and Mayordomo, we develop a Kolmogorov complexity point-to-set principle framework for upper and lower topological pressure and BS dimension in dynamical systems (and by extension for upper and lower entropy). As a demonstration of this framework we expand upon the Bowen pressure equation results of Climenhaga, as well as prove a pointwise version of the Bowen pressure equation.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-24T11:12:47Z
Brinda Venkataramani
arXiv categories: math.LO

We study finiteness classes arising from Ramsey-theoretic principles in set theory without the Axiom of Choice. First, we answer a question of Brot, Cao, and Fernández-Bretón concerning Gowers' $\mathbf{FIN}_k$ theorem. The $\mathbf{FIN}_k$ operation gives rise to a finiteness notion for each $k\geq 1$, but we show that this notion is independent of the value of $k$: the resulting hierarchy collapses, and every level is equivalent to $H$-finiteness, i.e., to Dedekind-finiteness of $[X]^{<ω}$. We then turn to the Rainbow Ramsey theorem and the Canonical Ramsey theorem. The corresponding failure classes $\operatorname{\mathbf{RRT-Fin}_n^m}$ and $\operatorname{\mathbf{CRT-Fin}}$ are genuine finiteness classes contained in $\operatorname{\mathbf{D-Fin}}$. We prove several inclusions placing them relative to standard Ramsey-theoretic finiteness classes of Brot--Cao--Fernández-Bretón, prove their independence from the collapsed Hindman--Gowers class, and analyze the parameter dependence of the rainbow classes through Fraenkel--Mostowski examples. The finer questions of strictness, and the full two-parameter structure of the rainbow classes, are left open where the present arguments do not settle them.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-26T13:02:39Z
Yair Hayut, Assaf Rinot, Zhixing You
arXiv categories: math.LO

Foreman and Magidor showed that the continuum hypothesis implies the existence of a countably-closed $\aleph_2$-cc forcing notion $\mathbb P$ for adding $\square_{\aleph_1}$. Here, we show that $\mathbb P$ may consistently be realized as an $\aleph_2$-Souslin tree. More generally, we prove that $\square_λ$ may be added by a $λ^+$-Souslin tree, providing the first analog of the Foreman--Magidor forcing at the level of successors of singular cardinals. Our construction is uniform and extends to inaccessible cardinals as well.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-26T17:08:26Z
John Krueger, Eduardo Martinez Mendoza
arXiv categories: math.LO

We explore the prospect of basis-like results for the class of Aronszajn lines which are consistent with the Continuum Hypothesis (CH). In particular, we prove that each of the following statements is consistent with CH: Any two Countryman lines contain isomorphic or anti-isomorphic uncountable suborders; for any coherent Aronszajan tree $T \subseteq {}^{< ω_1} ω$, the filter $\mathcal{U}(T)$ is an ultrafilter. The first result confirms a conjecture of Shelah in the context of CH which was previously shown to follow from the Proper Forcing Axiom. On the other hand, the weak diamond principle $2^ω< 2^{ω_1}$ implies that there does not exist a two element basis for the Countryman lines.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-26T23:28:47Z
Junhong Chen, Daheng Ju
arXiv categories: math.LO, math.CO

We take the first step toward the study of set-theoretic principles below the axiom of choice $\mathsf{AC}$ and the axiom of foundation $\mathsf{AF}$ by studying Frucht's theorem, an ordinary mathematical theorem which is provable with either $\mathsf{AC}$ or $\mathsf{AF}$ but not provable without both, and its variants. Specifically, we propose a number of such principles, study the relations between these principles and the standard axioms, and prove provability and unprovability results using (infinite) graph-theoretic constructions and permutation models, which draw a preliminary map of this new area of set theory.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-20T18:08:57Z
David Gepner, Hadrian Heine
arXiv categories: math.AT, math.CT

We study fibrations of higher categories from the perspective of oriented category theory, a framework which accounts for lax phenomena in higher category theory via systematic enrichment in the Gray tensor product. We give several equivalent characterizations of fibrations of $(\infty,\infty)$-categories and oriented categories, and show that categories of fibrations naturally organize to form oriented categories. We study the interaction between fibrations and oriented pullbacks and construct higher-categorical versions of free fibrations and universal fibrations. The latter give rise to Grothendieck constructions for fibrations of $(\infty,\infty)$-categories and oriented categories.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-21T11:20:14Z
Mahmud Azam, Steven Rayan
arXiv categories: math.DG, math.AG, math.AP, math.CT, math.RT

Let $X$ be a compact Kähler manifold. In prior work, we constructed diffeological moduli stacks of Higgs and flat bundles on $X$, related by extension completion of smooth harmonic families. Here, we develop the relative analytic theory. On Sobolev completions over arbitrary plots, we prove that every smooth stable Higgs family satisfying the numerical conditions admits a global smooth harmonic metric. Fixing a Hermitian--Einstein determinant metric removes scalar freedom, and then elliptic regularity and normalized gluing yield plotwise smoothness. The theorem holds at every finite parameter regularity $C^d$ and on reduced singular parameter spaces with ambient extensions. For a Higgs deformation $η$, the normalized metric variation satisfies $L_hs=-\mathcal S_h(η)$ and $s=-G_h\mathcal S_h(η)$ up to an independent rank-one determinant term for $\mathrm{GL}_r$. This computes the plotwise differential and recovers the classical comparison. Locally split, constant-type polystable families admit smooth harmonic metrics. Real-analytic examples show general polystable families may have neither continuous harmonic metrics nor relative harmonic filtrations and may lie outside every $C^d$ extension-generated locus. In one example a singular harmonic reduction produces a continuous adjoint Higgs field and a flat family with semisimple slices. This defines a weak $C^0$ operator-level harmonic mediator, strictly larger than the metric-regular one, whose endpoint images after finite extension completion and stackification satisfy $\mathscr M_{\mathrm{Dol},0}^{\mathrm{wk}\mathcal H}(X)\simeq\mathscr M_{\mathrm{dR},0}^{\mathrm{wk}\mathcal H}(X)$. We characterize the extension-generated stack by relative harmonic filtrations, develop their obstruction theory, analyze the loss of extension data under heat flow, and construct the smooth Hodge $λ$-family on the stable locus.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-25T14:25:57Z
Isaac Carcacía-Campos
arXiv categories: math.CT, cs.DB, math.AT

A database instance on a small category may be represented as a set-valued functor or, equivalently, as a discrete opfibration. Its sections correspond to globally coherent choices of records. When no global section exists, we measure the failure of global coherence by the minimum number of subcategories on which coherent choices can be made. Regarding natural transformations as directed homotopies, we introduce right and left directed fibrations and relate them to Grothendieck opfibrations and fibrations. We define directed versions of Lusternik-Schnirelmann category and sectional category and establish their invariance and comparison properties. Every functor admits a Grothendieck opfibration model on which directed sectional category is computed by strict local sections, together with a canonical discrete approximation obtained from connected components of comma categories. For functorial databases, we study directed sectional category under decomposition, iteration, and data migration, and characterize initial objects of finite connected acyclic schemas through the existence of global sections of objectwise non-empty databases.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-20T01:06:04Z
Bangxin Wang
arXiv categories: math.CT, math.DS

We develop a categorical framework for closed dynamical systems in which the abstract pattern of admissible evolutions is separated from its concrete realisation. A closed dynamical system is formulated as a functor $X\colon S\to C$ from a small category $S$, viewed as an abstract evolution shape, to a coefficient category $C$. By varying $S$ and $C$, this single definition encompasses many important examples including autonomous, non-autonomous, switched, hybrid, and stochastic systems. Within this framework, we introduce invariant subsystems, equilibria, and orbits in functorial terms. We then formulate convergence by combining a cosieve-based intrinsic notion of eventuality on the evolution shape with neighbourhood filters of invariant subsystems. Finally, we establish a categorical Lyapunov principle based on categorical sublevel neighbourhoods. This yields abstract stability and convergence criteria that recover the classical Lyapunov method in standard examples.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-20T01:54:28Z
Abhishek Banerjee, Surjeet Kour, Dipti Paik
arXiv categories: math.RA, math.CT

We study coalgebra measurings between multiplicative sequences of algebras and the maps induced by them on Hochschild homology. The Hochschild theory of multiplicative sequences is introduced as a functor taking values in graded algebras in the symmetric monoidal category of chain complexes, constructed with the help of the shuffle product. We develop the universal measuring coalgebra, or Sweedler Hom for multiplicative sequences, as well as study several other Sweedler operations in this context. In particular, we obtain an enrichment of multiplicative sequences over cocommutative coalgebras. Using an appropriate theory of bimodules over multiplicative sequences, we study maps induced by comodule measurings on the Hochschild theory with coefficients, as well as the corresponding enriched categories. Finally, we consider measurings and generalized Sweedler operations between multiplicative sequences induced by comultiplicative sequences of coalgebras, and also the maps in Hochschild theory obtained from them.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-20T16:24:36Z
Maxime Culot, Bo Shan Deval
arXiv categories: math.CT, math.GR

The Kaluzhnin--Krasner embedding establishes that, for a group extension, the middle group can be embedded into the wreath product of its kernel and cokernel. Recently, this construction has been generalised in a categorical framework, recovering both the classical group-theoretic result and its analogue for Lie In this article, we apply this categorical framework to two specific cases: precrossed modules and crossed modules (over groups). For precrossed modules, we introduce a Kaluzhnin--Krasner embedding -- previously unformulated -- by rigorously following the steps of the categorical procedure. In contrast, for crossed modules, we encounter substantial obstacles: while we present partial positive results, we also explain why constructing a full-fledged Kaluzhnin--Krasner embedding in this context is far more difficult.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-21T20:35:50Z
Pavel Etingof, Dmitri Nikshych, Victor Ostrik
arXiv categories: math.CT, math.QA, math.RT

We discuss the classification of twisted Deligne products of two semisimple tensor categories $\mathcal C,\mathcal D$, i.e., categorifications of the tensor product of their Grothendieck rings in which the factors are categorified by $\mathcal C$ and $\mathcal D$. In particular, we show that if both factors have no non-trivial gradings, or if one factor has neither non-trivial gradings nor tensor structures on the identity functor, then the only twisted Deligne product is the ordinary one. Using the work arXiv:2405.10207 by Müller, Peña Pollastri and Plavnik, this gives, in principle, a group-theoretical classification of twisted Deligne products and, more generally, exact factorizations of arbitrary fusion categories. In the Appendix we introduce the notion of categorical $n$-cocycles for $n=2,3,4$ and show that they are all pullbacks of group $n$-cocycles from the universal grading group of the underlying based ring. In the case of $4$-cocycles, this answers a question of Johnson-Freyd, Ostrik and Yu from arXiv:2601.09060.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-21T21:29:00Z
David Forsman
arXiv categories: math.CT, math.LO, math.QA

Ulmer introduced a semantic notion of bialgebras that unifies a broad class of algebraic and coalgebraic structures. We develop a syntactic counterpart by introducing signature pairs $(Σ,σ)$ and bialgebraic theories $T$, providing a uniform language for constructing internal bialgebras in a $2$-categorical setting. For every bialgebraic theory $T$ and $Σ$-model $M$ within a $2$-category with PIE limits, we construct the object $M^T$ of internal $T$-bialgebras. Our approach to bialgebras admits a general Induced Functor of Algebras Theorem extending the classical lifting of lax monoidal functors to the categories of internal monoids. Since the construction of $M^T$ is expressed entirely in terms of PIE limits, accessibility, local presentability, orthogonal factorization systems, regularity, and exactness lift along the construction $M \mapsto M^T$ under suitable assumptions.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-22T03:16:08Z
Yiwei Zheng
arXiv categories: math.QA, math.CT

We give complete conjugacy classes of modular group SL(2,Z). Particularly, the conjugacy classes of hyperbolic elements are decided by the proper equivalence classes of indefinite forms, and we give an example. Finally, we describe the coset representatives of centralizer of S, ST, T and hyperbolic elements of SL(2,Z).

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-22T07:31:49Z
Muneto Miyaji, Hiroaki Nagaya, Kento Ogawa, Takayuki Okuda
arXiv categories: math.CT, math.MG

In this paper, we provide a categorical framework for understanding coarse subspaces of coarse spaces. First, we introduce the notion of a controlled total relation between coarse spaces and show that the category whose morphisms are closeness classes of controlled total relations is isomorphic to the conventional category of coarse spaces defined using closeness classes of controlled maps. Next, we show that the assignment associating to each coarse space the finite-join partially ordered set of its coarse subspaces is functorial, and prove that this partially ordered set is naturally isomorphic to the poset of subobjects in the category of coarse spaces. Furthermore, we formulate asymptotic disjointness between coarse subspaces and show that mono-morphisms preserve this relation. These results provide a categorical interpretation of the framework of coarse subspaces introduced by Leitner--Vigolo [Lecture Notes in Math.~(2023)] and characterize coarse subspaces as objects intrinsic to the category of coarse spaces. They also provide a foundation for a coarse-geometric interpretation of the properness criterion established by Kobayashi [Math.~Ann.~(1989); J.~Lie Theory (1996)] and Benoist [Ann.~of Math.~(1996)] (cf.~Nagaya--Ogawa--Okuda [Proc.~Japan Acad.~Ser.~A (2025)]).

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-23T01:24:26Z
Ronan O'Gorman
arXiv categories: math.AG, math.LO

We formulate a group chunk theorem in the context of sheaves on sites which generalizes many similar results in model theory and algebraic geometry. Secondly, we develop an algebro-geometric analogue of Hrushovski's method of producing a group chunk from germs of definable functions on stationary types. The use of the model-theoretic tools of canonical bases and elimination of imaginaries is replaced with the use of Hilbert schemes to study ``canonical'' families of rational morphisms, allowing us to extend the previously known results over more general base schemes. The proofs of these results involve some technical work which may be of independent interest. First, we study partial morphisms in arbitrary categories, and show that a presheaf of partial magmas on a small category admits a universal morphism to a group. On the model theory side, we show that type-definable sets of $M^{eq}$ can be interpreted as sheaf quotients of type-definable sets. On the algebraic geometry side, we develop a theory of rational morphisms and families of rational morphisms of schemes over an arbitrary base.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-23T09:48:00Z
Marco Abbadini, Francesca Guffanti
arXiv categories: math.LO, math.CT

We give a self-contained proof of Gödel's completeness theorem entirely within the formalism of first-order Boolean doctrines (an algebraic approach to classical many-sorted first-order logic). Moreover, we show that Gödel's completeness theorem entails that the fiberwise Stone dual of a first-order Boolean doctrine is its type space functor; roughly speaking, this means that the Stone dual of the Boolean algebra of formulas in context $X$ is the Stone space of $X$-pointed models modulo elementary equivalence.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-23T22:14:52Z
Siddhant Jajodia, So Nakamura, Manuel Reyes
arXiv categories: math.CT, math.GR, math.RA

This is a thorough study of quotients of hyperstructures that generalize hypergroups, namely mosaics and semimosaics. The quotients in these categories generalize those studied previously in the literature on hypergroups. We describe the effective congruences in these categories by characterizing them in terms of their underlying equivalence relation. This characterization is applied to provide new methods of constructing quotient objects modulo the action of endomorphisms, as well as to study explicit quotient mosaics of some small groups. We also show that the category of mosaics has a natural proto-exact structure.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-24T15:20:21Z
Dali Zangurashvili
arXiv categories: math.GN, math.CT

Our earlier results on effective codescent morphisms of Hausdorff topological spaces are strengthened and complemented. In particular, it is proved that any embedding $p:B\rightarrowtail E$ with compact $B$ and normal $E$ is an effective codescent morphism in the category of Hausdorff topological spaces.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-25T08:31:03Z
Dali Zangurashvili
arXiv categories: math.CT, math.GN, math.RA

Employing the techniques of transporting a factorization system from one category to another via an adjunction, developed in our earlier papers, a factorization system is related to a radical on a homological category.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-25T10:51:26Z
Federico Campanini, Laura Cossu
arXiv categories: math.CT, math.RA

We study the category $\mathsf{AtoMon}$ of atomic monoids and atom-preserving homomorphisms. We prove that $\mathsf{AtoMon}$ is locally finitely presentable by exhibiting a strong generator consisting of compact objects. We show that $\mathsf{AtoMon}$ admits (regular epi, mono)-factorizations but that it is not a regular category: we construct a regular epimorphism which is not pullback-stable. We also establish adjunctions for the group of units and explicitly construct the ``cofree atomic monoid'' over an arbitrary monoid. Finally, we exhibit a way to lift torsion theories of $\mathsf{Grp}$ to pretorsion theories of $\mathsf{AtoMon}$ and extend this construction to a more general setting.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-26T03:02:36Z
Colin Bloomfield, Peter Jipsen, Valeria de Paiva
arXiv categories: math.LO, cs.LO, math.CT

Categorification---the process of constructing a categorical model of a piece of mathematics---often identifies a common abstraction that connects formerly unrelated but known structures. In the case of de Paiva's categorification of Gödel's Dialectica interpretation, we find that its specialization to partial orders produces (functorial) embeddings of Heyting algebras into residuated lattices that appear to have been overlooked. For the non-categorical audience, we present this specialization and take care to reproduce the original proofs in the algebraic setting. Along the way we obtain results particular to this algebraic setting: an embedding lacking an evident adjoint in de Paiva's general construction acquires a definable one here; a single Dialectica tensor validates contraction in the intuitionistic construction D yet refutes it in the classical variant G; and, over ZF, the poset reflection PD(Set) collapses onto the four-element algebra PD(2) exactly when the Axiom of Choice holds.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-26T07:38:18Z
Ryo Kanda
arXiv categories: math.CT, math.RA, math.RT

We construct a Grothendieck category that has a noetherian generator, satisfies AB4*, and is not equivalent to a module category. This gives a negative answer to Djament's problem. The category is obtained as a Gabriel quotient of a module category over the endomorphism ring appearing in the work of Herbera, Příhoda, and Wiegand. The proof relies on the trace criterion established by Martini, Parra, Saorín, and Virili.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-26T09:33:15Z
SeungJu Lee
arXiv categories: math.CT

Distinct proofs, programs, formulas, or rewrite paths may have the same observable behavior while differing in occurrence structure, sharing, interfaces, or transformation history. We develop a guarded realization semantics that retains these distinctions when an error is extracted. The resulting error magnitude is bounded above by a certificate attached to the chosen realization and below by the greatest lower bound determined solely by the observed behavior. For linear double-pushout rewriting in a typed presheaf setting, we identify the greatest subobject transported intact through a rewrite step and through a finite rewrite path. Guarded local estimates compose to give pathwise upper certificates. At the set level, the complementary lower bound is the infimum of magnitudes in a behavior fiber. For non-discrete categories, it is given by a pointwise right Kan extension when that extension exists, and it reduces to the strict-fiber infimum under a Grothendieck fibration hypothesis. For continuous surjective linear observations onto finite-dimensional normed spaces, the lower reflection is the induced quotient norm. Applied to finitely many distinct characters on a compact metrizable abelian group, this yields an interpolation norm with an exact dual formula. Continuous and discrete Abel transfer theorems then convert observed coefficients into lower bounds for tail amplitudes, with consequences for Mellin transforms, generating functions, and normalized point-count errors of curves over finite fields. Under the stated guards and soundness hypotheses, every realization satisfies $Q(O(\mathrm{Err}(r))) \leq A(\mathrm{Err}(r)) \leq U(r)$.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-25T10:36:34Z
Tianshi Yu, Gilles Barthe, Minbo Gao, Mingsheng Ying, Li Zhou
arXiv categories: cs.LO, cs.PL, math.FA, quant-ph

Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient omputational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics. Yet, the semantic foundations of CVQC remain underdeveloped. To address this gap, we develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness. A main contribution of this work is to isolate a well-behaved quantitative predicate domain that achieves sufficient expressiveness to accommodate unbounded values as they arise in the infinite-dimensional, continuous setting. Specifically, we choose closed positive quadratic forms as semantic predicates, representing finite expectations, domains of finiteness, and infinite penalties in one ordered object. We validate our choice by establishing that our semantic predicates satisfy desirable closure properties including the definition of weakest preconditions. We validate our design with two case studies, including an example based on the celebrated GKP error-correcting code, for which we establish a second moment bound.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-20T09:01:50Z
Wolfgang Faber, Laura Giordano, Ricardo Rocha, Vítor Santos Costa
arXiv categories: cs.LO, cs.PL

Since the first conference in Marseille in 1982, the International Conference on Logic Programming (ICLP) has been the premier international event for presenting research in logic programming. These proceedings include the Technical Communications of the 42nd ICLP, held 20-23 July 2026 as part of FLoC 2026 in Lisbon, Portugal. The papers and extended abstracts in this volume address the following areas and topics: theoretical foundations, language design and programming methodologies, program analysis and optimization, applications and implementation methodologies. This volume features contributions to two submission tracks of ICLP 2026: the Main track and the Recently Published Research track.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-21T20:26:14Z
Ben De Bondt, Andreas Thom
arXiv categories: math.OA, math.GR, math.LO

We study homomorphisms, with a focus on isomorphisms, between the tracial metric reduced products of finite dimensional unitary groups and of matrix algebras. A variant of Ulam stability for unitary groups and a classification of the almost surjective continuous homomorphisms between finite dimensional unitary groups are proved and then used to show that all isomorphisms of product form of these tracial reduced products are induced by almost permutations of the coordinates and coordinatewise application of automorphisms. We prove coordinate recognition for these reduced products and obtain under set theoretic assumptions rigidity and classification results for their full automorphism groups. For tracial reduced matrix algebras we obtain such rigidity result in the more general context of center-preserving $*$-homomorphisms.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-22T21:02:37Z
Denise M. Case
arXiv categories: cs.LO, cs.AI

A record system declares when two records refer to the same entity, occurrence, scope, or rule. Its disclosed implementation mechanisms induce a corresponding operational identity relation. The declared and implemented relations may diverge systematically without producing a provenance gap or detectable contradiction. A system can apply, consistently and with every record individually correct, a rule of sameness that no artifact declares. This paper formalizes that implemented relation. A declared identity regime partitions a finite record domain into co-reference classes; a disclosed mechanism, through its typed identity-relevant outcomes, induces an operational identity partition of the same domain. The audit compares these partitions in the refinement lattice. A mechanism is faithful when the declared partition refines the operational partition, so no declared class is split. A divergence witness is a pair the declaration merges and the mechanism separates; such witnesses are decidable by pair enumeration. When an imported sibling basis also splits a declared class, local comparison with its partition yields sibling-aligned, sub-sibling, super-sibling, or sibling-incomparable divergence. This result reports only the relationship; it does not identify the basis carried by the mechanism. Global equality of the operational and sibling partitions is defined separately as regime substitution and does not follow from sibling alignment. A version field incremented on every textual edit inhabits the sub-sibling case by splitting declared classes more finely than either imported basis. The audit is three-valued and relative to the disclosed artifacts, evaluated surfaces, and identified uses; each boundary has a finite refuting witness. A passing verdict is non-monotone because extending the transformation history can merge declared classes and create a witness among records already examined.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-23T03:52:29Z
Bowen Xu
arXiv categories: cs.LO, cs.AI

Goal reasoning in Non-Axiomatic Logic (NAL) explains how an adaptive system derives means for realizing desired events under insufficient knowledge and resources. However, the representation of avoidance is less clear. A common convention is to express ``avoid $G$'' as the goal sentence ``$\neg G!$'', but this notation conflates two different readings: pursuing the negated event $\neg G$, and avoiding the positive event $G$. This paper shows that the conflation can produce a paradoxical case in which an avoidance intention is converted into a positive goal to act merely because acting is usually followed by the absence of hurt. Starting from NAL's basic definition of goals, the framework is extended with a corresponding definition of anti-goals, so that avoidance can be represented without treating it as the pursuit of a negated event. Finally, a mental operation, $\op{prevent}$, is introduced to connect anti-goal reasoning with ordinary goal reasoning in cases of active prevention. Four minimal case studies check that the resulting rules distinguish pursuit, passive avoidance, active prevention, and withholding action to preserve a desired event.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-23T11:22:25Z
Heather Merhout, Daniela Inclezan
arXiv categories: cs.LO, cs.AI

In the field of Artificial Intelligence, an agent is a system which is able to autonomously make decisions in order to reach a desired goal. As these systems grow more prevalent in our day-to-day lives, there has been an increased need to add explainability features which can provide an account for an agent's behavior. We therefore propose a framework that outlines how to produce comprehensible explanations for policy-aware agents, or agents which have rule-enforcing policies incorporated in their decision-making framework. This framework is designed using insights from the social sciences on how to produce good explanations. It is implemented in the Answer Set Programming language while using Python to assist with information extraction and natural-language translation. Because these agents incur penalties when violating policies, we are able to leverage these penalties to detect undesirable events in scenarios that are counterfactual to the agents' original actions. This lends itself to creating contrastive explanations (e.g., "the agent performed this action because, had it not, undesirable event X would have occurred."), which formulate the core component for our explainability framework. The framework is evaluated using a survey wherein human participants provide feedback on our program-generated explanations.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-24T14:47:59Z
Runzhou Li, Hongfei Fu, Qingkai Shi, Peisen Yao
arXiv categories: cs.FL, cs.DS, cs.PL

Semantic regular expressions (SemREs) attach external Boolean predicates to matched spans, making both the number and the sequentiality of oracle calls central resources. For a fixed expression and word, we represent membership by a polynomial-size monotone span circuit and identify optimal semantic evaluation with Boolean decision-tree evaluation. We determine the extremal power of adaptivity asymptotically sharply. For every $E\ge2$, there is a unary, star-free, semantic-depth-one instance of syntax size $Θ(E)$ with $E$ essential oracle keys and only unit-length semantic spans whose one-round cost is $E$, whereas its exact two-round and unrestricted deterministic costs are \[ \log_2 E+\tfrac12\log_2\log_2 E+O(1). \] Consequently, the largest nonadaptive-to-adaptive ratio is $(1+o(1))E/\log_2E$, including the optimal leading constant. A second restricted family exhibits a complete round hierarchy: its optimal $R$-round cost is $Θ(R E^{1/R})$. Thus the maximal gap already appears in two rounds, while other instances interpolate smoothly across all round budgets. Both constructions admit one-predicate realizations over the fixed alphabet $\{0,1,\#\}$ with logarithmic-length semantic spans and $O(E\log^2 E)$ total representation size. Under pointwise error $δ<1/2$ and worst-case expected cost, randomized nonadaptive complexity is exactly $(1-2δ)E$ for every instance with $E$ essential keys. Finally, for a fixed word $w$ and $h$ predicate names, the exact randomized minimax value is $(1-2δ)h sd(w)$, where $sd(w)$ counts distinct substring values; a span bound $s$ replaces $sd(w)$ by $sd_s(w)$. These results separate semantic information acquisition, parallel latency, and local symbolic matching cost.

arXiv abstract · PDF