Component Modalities of Quantum Logic

2026-07-16T09:43:01Z

This paper determines the structural and proof-theoretic consequences of the forcing condition in relational quantum modal logic, under which every modal transition available at a world is also available at every world compatible with it. We prove that modal successor sets are constant on compatibility components, so boxed truth sets belong to the Boolean algebra of unions of these components. The relation holding exactly between worlds in the same component assigns to each stable proposition its greatest lower and least upper approximations by unions of components, and in hard superselection models these are exactly the approximations by central propositions. We adopt local validity for sequents with multiple conclusions to give a semantics for modal excluded middle on frames with several components. A connectedization obtained by adding one point then shows that component frames, equivalence frames satisfying the forcing condition, and connected compatibility frames with universal modal accessibility have the same logic for sequents with one conclusion. Finally, maximal consistent pairs yield a canonical model, and the calculus obtained by adding T, 4, and B is proved sound and complete for the three frame classes. These results characterize the logical scope of the forcing condition and establish a complete proof theory for component modalities.

Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System

2026-07-16T07:09:03Z

We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers

2026-07-16T05:20:09Z

Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a constructive dependent type theory, we present a framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations. We first define open, closed, compact and overt subsets for generic spaces in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis and constructive mathematics. From these proofs we can extract programs for testing inclusion, overlapping of sets, et cetera. To enhance the efficiency of the extracted programs, we then focus on Polish spaces, where we give more efficient encodings based on metric properties of the space. As various computational properties depend on the continuity of the encoding functions, we introduce a nondeterministic version of a continuity principle which is natural in our formalization and valid under the standard type-2 realizability interpretation. Using this principle we further derive the computational equivalence between the generic and the metric encodings. Our theory is fully implemented in the Coq proof assistant. From proofs in this Coq formalization, we can extract certified programs for error-free operations on subsets. As an application, we provide a function that constructs fractals in Euclidean space, such as the Sierpinski triangle, from iterated function systems using the limit operation. The resulting programs can be used to draw such fractals up to any desired resolution.

Executing Discrete/Continuous Declarative Process Specifications via Complex Event Processing

2026-07-15T17:49:51Z

Traditional Business Process Management (BPM) focuses on discrete events and fails to incorporate critical continuous sensor data in cyber-physical environments. Hybrid declarative specifications, utilizing Signal Temporal Logic (STL), address this limitation by allowing constraints over both discrete events and real-valued signals. However, existing work has been limited to monitoring and post-hoc conformance checking. This paper introduces a novel execution architecture based on Complex Event Processing (CEP) that enables the real-time execution and enforcement of hybrid declarative models. Our three-layer approach integrates STL-inspired predicates into the execution flow, allowing the system to actively trigger activities and enforce process boundaries based on continuous sensor behavior. This approach bridges the gap between hybrid specification and operational control.

Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity

2026-07-15T16:08:36Z

We study model checking for an epistemic metric temporal logic with past, interpreted over finite Büchi automata under synchronous perfect recall. The logic is motivated by observation-based verification problems such as diagnosis and opacity, where an observer sees only a projection of an execution and reasons about events that may have occurred earlier. These requirements use no alternation between different agents' knowledge. We therefore consider the agent-alternation-free fragment, in which nested knowledge operators must refer to the same agent. We show that model checking for this fragment is EXPSPACE-complete. The lower bound already holds with one agent, one occurrence of the knowledge operator, and no non-trivial metric bounds. For the upper bound, we combine temporal test automata with perfect-recall observers. Because past formulas may have different truth values on indistinguishable histories ending in the same system state, the observer must track temporal automaton states in addition to system states.

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking

2026-07-15T14:35:26Z

The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process: a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.

Inferentialist Game Semantics (Extended Abstract)

2026-07-15T14:01:53Z

Game semantics is an elegant approach to the formal semantics of reasoning and computation that grounds model-theoretic concepts of truth and validity in game-theoretic concepts that emphasize the dynamic and interactive aspects of logical reasoning. In Hyland-Ong games, plays are traces of interactions between a player and an environment and such games provide a naturally appealing semantics for computation that is derived from proof-search in logical systems. Such a semantics can be seen as providing an intensional theory of meaning for systems of logic in terms of (the computation of) proofs. In logic, an intensional theory of meaning for systems of logic is offered by proof-theoretic semantics; in particular, by base-extension semantics (B-eS), in which the model-theoretic interpretation of atomic propositions in a satisfaction relation is replaced by a validity relation which uses provability in `bases' of atomic rules. We establish a fully abstract correlation between B-eS and Hyland-Ong game semantics, employing techniques similar to those used by Sandqvist to give a sound and complete B-eS for intuitionistic propositional logic. We illustrate our semantics through the example of 4x4 Sudoku.

Quantum Bayesian Networks: Compositionality and Typing via Linear Logic

2026-07-15T11:00:46Z

Quantum Bayesian networks provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl's Bayesian networks -- prominent graphical models for classical probabilistic reasoning and inference. The goal of this paper is to bring compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems, and which we prove sound and complete with respect to quantum Bayesian networks.

Definitional Inversion, Without Normalisation

2026-07-15T10:06:45Z

We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-Löf's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $η$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where Gödel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.

A Simple Obligation to Metric Interval Temporal Logic

2026-07-15T08:46:48Z

Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, based on an idea of tracking time-constrained obligations along a word. To check whether a Linear Temporal Logic (LTL) formula is true at a position of a word, it is natural to generate certain obligations that need to be satisfied at a later point. For instance, $a ~\mathcal{U}~ b$ (with strict Until semantics) is true at position $i$ if either $b$ or the set $\{a, a ~\mathcal{U}~ b\}$ is true at $i+1$. We enhance this idea in the context of MITL by introducing a notion of time inside these obligations. However, a naïve procedure could lead to more and more obligations getting generated along the word, with no bound on the number. We propose a simple mechanism to eliminate or merge redundant obligations. For MITL, this mechanism ensures that only a bounded number of obligations are maintained along the entire timed word. We develop this observation into a symbolic procedure for MITL satisfiability using regions.

Ripple: An Open, AI-Formalized Lean 4 Framework for Computing with CRNs

2026-07-15T07:32:07Z

We present Ripple, an open, AI-formalized Lean 4 framework for the mathematics of computing real numbers with chemical reaction networks (CRNs). Ripple formalizes the full ladder of models -- the GPAC / CRN continuum and the CRN-computable reals, the large-population-protocol (LPP) compilation pipeline, and a continuous-time Markov chain (CTMC) layer bridged to the deterministic mean-field limit by three machine-checked versions of Kurtz's theorem, and two Turing-completeness results -- the Bournez-Graça-Pouly GPAC Turing-completeness construction and the Soloveichik-Cook-Winfree-Bruck stochastic-CRN universality theorem. The development is reliable (its core constructions are verified to depend on exactly the three Mathlib foundational axioms, with no sorry); it exposed genuine, fixable gaps in published proofs (the approximate-majority convergence argument and the LPP main theorem); and it proves new results -- a fully machine-checked construction of Apéry's constant ζ(3) as a CRN-computable number via its holonomic generating function, the same recipe turning the modular 1/π series of Ramanujan into a sharp open problem. The formalization was carried out predominantly by AI agents using only publicly available models, so the workflow is reproducible.

Intuitionistic Dynamic Logic

2026-07-15T07:29:29Z

This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such systems provide formal tools for reasoning about change, such as encountered in mathematical systems evolving over time or in the knowledge state of an agent after an information update. We investigate five intuitionistic dynamic logics: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic and bi-intuitionistic linear temporal logic. On the proof theoretic side we develop sound and complete Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. On the semantic side we study these logics over various classes of dynamic models, which are birelational Kripke models satisfying confluence and frame conditions. We establish expressivity results, the finite model property, decidability, as well as complexity bounds. The main contributions are threefold. First, we develop analytic cyclic sequent calculi for intuitionistic master modality and common knowledge logic, where completeness is obtained by a robust proof search argument. Second, we obtain the finite model property and decidability for bi-intuitionistic modal logic via an intricate combinatorial analysis of dynamic models. Third, we develop a sound and complete axiomatization for intuitionistic linear temporal logic featuring the temporal operators next, eventually and henceforth, thereby providing a positive answer to the long-standing open question concerning the existence of a finite axiomatization.

Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

2026-07-15T05:40:08Z

Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

2026-07-15T04:05:03Z

The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $Σ$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and the soundness of Pearl's d-separation theorem on arbitrary finite directed acyclic graphs (DAGs) -- in interventional form for multi-element $X$, $Y$, $Z$, and in Bayesian form for the elementary patterns. The probability monad is also verified as a Markov category; the abstract interface discharges at $\mathbb{Q}$.

Thermodynamic Limits of Proof

2026-07-14T22:01:07Z

Every irreversible recorded distinction has a positive thermodynamic work floor. Landauer's principle supplies the ideal bound $\varepsilon\ge k_B T\ln 2$ per irreversible bit, experimentally verified to $\pm 10\%$. Proof available to an agent is checkable information for that agent: some substrate must produce, retain, and expose evidence that excludes answer-changing alternatives. A finite detector array operating at temperature $T$ for finite time has finite signal-acquisition capacity. Combining finite causal access, positive retained-record cost, and exact lower bounds on required records gives the Physical Counting Impossibility Theorem: no fixed-budget substrate can provide universal exact proof once the retained-record lower bound exceeds the declared budget. The theorem requires exactly $B<\infty$ and $\varepsilon>0$. An answer reports a value; proof supplies checkable grounds for accepting it. A reversible device may compute an answer and erase its scratch history, but proof requires retained, inspectable records. A global answer register, oracle response, entanglement witness, finite survey catalog, or trusted device output supplies proof only through an interface that exposes the relevant grounds to the verifier. A proposed interface must identify the retained-record lower-bound family $R(n)$ it induces. Sound operational claims about efficient solvability inherit the same finite-budget obstruction when their acceptance would license universal exact proof. Substrate-free derivability has proof status only when a physical verification event makes it available to an agent.