cs.LO — Pith

Top Pith

7

cs.LO 2026-05-14 3 theorems

Real-valued provability in linear logic converges to MALL at infinite hardness

by Matteo Capucci, Robert Atkey +2 more

pQLL calculi prove cut-elimination and completeness for soft lattices, supporting differentiable additive connectives in verification.

abstract click to expand

Real-valued logics have seen a renewed interest in verification for probabilistic and quantitative systems, in particular machine learning models, where they can be used to directly integrate specifications in the training objective. To do so effectively one has to strike a balance between the logical properties of the connectives and their semantics. A major hurdle in this sense is to give ``soft'' (i.e. differentiable) semantics to additive connectives -- in linear and fuzzy logics, additives are necessarily ``hard'' lattice operations. In this paper, we solve this problem by combining an accurate analysis of the properties of sum and product on the reals with a significant revision of sequent calculus. We introduce `quantitative sequent calculi', which simultaneously generalize hypersequent calculi of fuzzy logics and deep inference, and in which validity of a proof and provability of a sequent are real-valued quantities. We present a family of calculi, pQLL, indexed by a hardness degree $p$, prove cut-elimination theorem for them, and show completeness for enriched residuated `soft' lattices. For $p = \infty$, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when $p \to \infty$.

1 0

Top Pith

3

cs.LO 2026-05-15 2 theorems

The paper shows that adding a reversal operation to self-dual cubical type theories is a…

by Evan Cavallo, Christian Sattler

Eliminating reversals from cubical type theories

Adding reversals to self-dual cubical interval theories yields a conservative extension via the twist construction, enabling the first…

abstract click to expand

Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this interval yields different type theories. A reversal is an involutive operator on the interval that swaps its two endpoints. We show that for cubical type theories with self-dual interval theories, such as the minimal theory of two endpoints or the theory of a bounded distributive lattice, the extension of the theory with a reversal that internalizes the duality is a conservative extension. The key tool is a "twist construction": the product of an interval and its dual is again an interval with a reversal given by swapping coordinates. Our conservativity result applies to "opaque" cubical type theories, without strict equations reducing the filling operator at concrete type formers or eliminators from higher inductive types at path constructors. Using the same twist construction, we also construct models of strict cubical type theory with reversals in categories of cubical sets without reversals. We thereby give the first model of a theory with reversals whose homotopy theory corresponds to that of topological spaces.

0

Top Pith

2

cs.LO 2026-05-14 2 theorems

Hoare logic equivalent to second-order logic with first-order predicates

by Daniel Leivant

A foundational characterization of Hoare Logic

Partial correctness assertions for iterative programs hold in one system exactly when they hold in the other.

abstract click to expand

We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic.

0

math.LO 2026-07-03

Theory-topos duality defines conceptual completeness for logic fragments

by Ivan Di Liberti, Umberto Tarantino +1 more

Conceptual completeness for subgeometric logics

Fragments satisfying the duality embed conservatively into geometric logic; coherent, regular and disjunctive logics are shown to qualify.

abstract click to expand

We explore the notion of conceptual completeness for a fragment of geometric logic in the framework developed by the first and third author. Unlike its traditional interpretation as a reconstruction of syntax from semantics, in this paper we characterise conceptual completeness of a fixed fragment in terms of a duality between theories and topoi. We then show that conceptually complete fragments are conservatively embedded in full geometric logic, thus casting conceptual completeness in a new proof-theoretic light. We give a new proof of conceptual completeness for coherent logic, and we also show that regular, disjunctive, and essentially algebraic logic with falsum are conceptually complete. Finally, we show that our notion is equivalent to a traditional reconstruction result under the assumption of completeness with respect to set-based models: in the coherent case, we thus recover Makkai's original reconstruction theorem via ultracategories.

0

cs.DS 2026-07-03

Courcelle theorem refined to ETH-tight variable counts per block

by Daniel Lokshtanov, Fahad Panolan +3 more

Fine-Grained Bounds for Courcelle's Theorem

The running time now tracks the exact number of first- and second-order variables inside each quantifier alternation rather than alternation

abstract click to expand

Courcelle's theorem states that there exists an algorithm that takes as input a graph $G$ of treewidth at most $t$ and a MSO formula $\phi$, and determines whether $G$ satisfies $\phi$ in time $f(\phi,t) \cdot n$. It is folklore that the the function $f$ contains a tower of exponentials whose height depends as a linear function of the number of quantifier alternations of the input formula $\phi$. A classic reduction of Frick and Grohe shows that, assuming the Exponential Time Hypothesis (ETH), the linear growth of the height of the tower is unavoidable. Nevertheless, there is still a huge gap between existing upper and lower bounds -- after all, there is quite a difference between a single exponential and a double exponential running time. In addition, this only gives us a very coarse understanding in the time complexity of Courcelle's theorem. In this paper, we prove a fine-grained version of Courcelle's theorem with nearly ETH-tight dependence on the treewidth parameter $t$ and the quantifier structure of $\phi$ (specifically, the number of first order and second order variables in each quantifier alternation block).

0

cs.CC 2026-07-03

Clause substitution creates local blind spot in K-SAT

by Wen Fang, Xianxian Li +4 more

Self-Referential K-SAT and the Finite Analogue of G\"odel's Incompleteness Theorem

Indistinguishable SAT/UNSAT pairs force wide clauses in Resolution and push proof size toward 2^N.

abstract click to expand

Self-reference and solution independence are core properties underlying intractability. This paper establishes a finite combinatorial analogue of G\"odel's incompleteness theorems within Boolean $K$-SAT. While standard random $K$-SAT has assignment correlations that disrupt solution independence, we resolve this via a logarithmic-width ensemble ($K = O(\log N)$). Here, satisfying assignments converge to a Poisson distribution, letting unsatisfiable and uniquely satisfiable formulas coexist. By executing a single-clause substitution conditioned on the unique solution, we construct structurally irreducible SAT/UNSAT pairs that are indistinguishable via local evaluation. Using algorithmic information theory and Shannon channels, we prove that deductive pipelines restricted to a sublinear window suffer from an informational blind spot, forcing a descriptive lower bound of $K(\mathcal{A}) \geq \Omega(N^{1-\delta})$. This deficit forces any Resolution refutation of the UNSAT instance to utilize wide clauses ($w(\pi) \geq \Omega(N^{1-\delta})$), triggering an exponential proof-tree explosion ($S(\phi) \geq \exp(\Omega(N^{1-2\delta}))$). As $\delta \rightarrow 0^+$, this bound converges to the worst-case $2^N$ threshold, reframing the Strong Exponential Time Hypothesis (SETH) as a direct projection of G\"odel incompleteness onto finite computation. We diagnose the decades-long stagnation in complexity theory. Transitioning from Turing's class separation to a G\"odelian paradigm of instance indistinguishability, we introduce a multi-dimensional comparative framework that contrasts these two historical lineages across distinct perspectives. The self-referential hardness exhibits physical invariance: it precludes quantum shortcuts due to the necessity of global semantic analysis and delineates a scaling bottleneck for machine learning architectures operating on lossy, local compression.

0

cs.LO 2026-07-03

LLMs invent predicates to boost ILP success from 0% to 58%

by Tingting Yu, Pei-Cing Huang +3 more

ADVENT: LLM-Driven Automatic Predicate Invention for ILP

Automatic creation of reusable rules via LLM and Prolog loop enables cross-task learning on relational data.

abstract click to expand

Predicate invention (PI), the creation of new predicates to extend the hypothesis space, remains a critical bottleneck in Inductive Logic Programming (ILP). Existing methods rely on domain expertise and produce semantically opaque predicates, hindering adaptation to unfamiliar domains and cross-task reuse. We present ADVENT, an LLM-driven PI mechanism for ILP. ADVENT pairs LLM abductive generation with Prolog deductive verification, forming an iterative loop in which concrete execution results guide the LLM to refine candidate predicates. The mechanism leverages Large Language Models to identify implicit patterns in structured relational data and invent auxiliary predicates with meaningful names and definitions. Invented predicates and learned rules accumulate in a knowledge pool for cross-task reuse. Experiments on nine poker-hand concepts across seven LLMs show that LLM-driven PI achieves 58% success rate where ILP alone fails entirely, formal verification raises this to 80%, and the knowledge pool yields gains up to +31 percentage points, while producing human-interpretable rules. These results suggest that ADVENT offers a promising direction for automating predicate invention and enabling cross-task knowledge reuse in ILP.

0

cs.SE 2026-07-02

Kani verifies 16000+ Rust harnesses per stdlib change

by Rémi Delmas, Zyad Hassan +10 more

Kani: A Model Checker for Rust

Translates MIR to CBMC to prove functional correctness and absence of panics beyond what the type system guarantees.

abstract click to expand

Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.

0

cs.AI 2026-07-02

Rewrite method certifies 105 of 185 expert problems at 91% precision

by Ben Slivinski, Michael Saldivar

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

By requiring explicit justifications for every state change, it surfaces hidden premises and fabricated citations that holistic judges miss.

abstract click to expand

When should an AI system's answer be trusted? Formal proof assistants offer certainty but cannot reach most of the problem distribution; scalar LLM judges offer coverage but produce opaque scores that cannot be audited after the fact and are subject to the same coherence issues as any LLM. We present Theoria, a verification architecture that closes this gap. A candidate solution is rewritten into a sequence of typed state transitions, each licensed by an explicit justification, whether that be a citation, computation, or problem-given fact, and every transition is independently auditable. The foundational invariant is completeness of change: every difference between consecutive proof states must be accounted for, so hidden premises surface as unlicensed mutations rather than passing silently. On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 at 91.4% strict precision (Wilson 95% CI [84.5%, 95.4%]). Every certification produces a human readable proof trace in which each step can be independently challenged. Holistic LLM judges achieve comparable precision at matched coverage but fail on different problems (Jaccard 0.14-0.36), making the approaches complementary. On 95 adversarial poisoned proofs across 15 domains, structured judges catch 94.7% versus 83.2% for holistic judging (p= 0.0017). The overall 11.5 pp gap concentrates in hidden premises (90.6% vs. 62.5%, a 28 pp difference) and fabricated citations (100% vs. 90%), the error classes where the formal analysis predicts an advantage; performance is identical on arithmetic and theorem-misapplication errors, where no advantage is predicted. On GPQA Diamond (n= 65), certified precision is 97.1% (Wilson CI [85.1%, 99.5%]).

0

cs.LO 2026-07-02

Minimal frames make injectivity definable in modal-temporal logic

by Alfredo Burrieza

Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Restricting to the O² family controls functional multiplicity so the language defines more properties over orders, with the strict reading k

abstract click to expand

We study the expressive power of the simplest modal-temporal language, obtained by adding Prior's temporal operators $G$ and $H$ to the basic modal language with $\Box$. This language is the standard bimodal combination of modal and tense logic; under its functional interpretation it is denoted $L_{T\times W}$. To analyse its definability across five order types, we consider two semantic readings of the temporal operators: the standard reading ($G,H$), which includes the current instant, and the strict reading ($G^{\ast},H^{\ast}$), which always excludes it. We examine nine functional properties -- totality, non-totality, injectivity, surjectivity, monotonicity, strict monotonicity, antitonicity, strict antitonicity, and constancy -- over preorders, strict preorders, partial orders, linear orders, and strict linear orders. Our analysis reveals two different levels of expressive power. In the original multiflow setting, the language is quite weak and the two readings coincide. When we restrict the semantics to minimal functional frames (the $O^{2}$ family), many properties become definable, and the choice of reading becomes crucial: the strict reading can define properties such as injectivity even in reflexive orders. The same definability patterns appear with indexed languages and with the Uniform Domain condition on the semantics of $L_{T\times W}$. That three such different ways of controlling functional multiplicity lead to identical definability patterns indicates that the expressive limitations of the original framework come from the uncontrolled multiplicity of functions, not from any weakness of the operators. Even after controlling functional multiplicity, a set of properties remains undefinable in all non-linear orders, showing that the lack of connectivity is a fundamental obstacle.

0

cs.LO 2026-07-02

LRAT-Catcher imports SAT certificates into Lean4 theorems

by Stefan Szeider

LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection

Reflection runs the verified checker natively, proving S(4)=44 and R(4,4)=18 where explicit proof terms run out of memory.

abstract click to expand

SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an LRAT certificate into Lean 4 as a theorem. LRAT-Catcher runs the formally verified LRAT checker from Lean core as compiled native code via reflection. This scales to instances where Mathlib's explicit proof-term import exhausts memory. LRAT-Catcher also composes cube-and-conquer solving runs entirely inside Lean. Per-cube refutations are combined with a cover-completeness certificate, itself an LRAT proof, into a single unsatisfiability theorem. Verified encodings connect CNF-level results to the original combinatorial problems. We evaluate the tool against Mathlib's proof-term import and the external checker cake_lpr on establishing the Schur number S(4) = 44 and the Ramsey number R(4,4) = 18 as Lean theorems.

0

quant-ph 2026-07-02

All three-qubit nonlocality paradoxes via parity proofs classified

by Nadish de Silva, Santanil Jana +1 more

Three-qubit nonlocality paradoxes: beyond GHZ

Enumeration shows far more structures than earlier work assumed and breaks the regularity conditions used in all prior constructions.

abstract click to expand

Quantum nonlocality paradoxes, such as that of GHZ, provide maximally sharp logical obstructions to classical probabilistic models of quantum correlations. They are key resources in a broad variety of information-theoretic tasks that exhibit unconditional quantum advantage. For example, in nonlocal games, which are communication tasks that serve as core technical tools in recent landmark results in quantum computational complexity theory. Their role in establishing quantum advantage motivated their study by Abramsky et al. who introduced an infinite family of three-qubit paradoxes exhibiting novel conditional structure. This was later extended by de Silva et al. into a full classification program. In this work, we completely classify all three-qubit nonlocality paradoxes established via a biconditional parity proof; this is a very large class of paradoxes that encompasses all earlier-known examples. We do this by introducing a suite of new structural and combinatorial techniques. We find that the landscape of nonlocality paradoxes is far richer than previously understood, violating regularity conditions underlying all prior constructions.

0

cs.LO 2026-07-02

Interval abstraction bounds reachability in general stochastic automata

by Pedro R. D'Argenio, Arnd Hartmanns +1 more

Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Refinable intervals with big time steps give sound bounds for arbitrary continuous distributions without restricting the model class.

abstract click to expand

Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularly useful to faithfully model and analyse dependable systems involving faults, maintenance, and repairs. Effective SA analysis approaches have so far been limited to statistical model checking and thus deterministic SA, while previously proposed model-checking techniques apply to limited subclasses of SA only, or do not scale. In this paper, we present the first dedicated SA model checking approach that is general and effective: It puts few restrictions on the input SA, and we show in our experimental evaluation that it works well for nontrivial examples. It combines a refinable interval abstraction of the continuous distributions with a direct application of the "big time steps" semantics of SA, providing upper/lower bounds on maximum/minimum reachability probabilities. We extend the Modest and Jani modelling formalisms with support for SA, and provide a prototype implementation of our approach in Rust.

0

cs.LO 2026-07-02

Restricted searches tame combinatorial growth in semantic labelling

by Dieter Hofbauer, Johannes Waldmann

Semantic Labelling in Practice

Experiments test exhaustive checks inside narrowed spaces and context-closure on fixed algebras as workable routes for termination proofs

abstract click to expand

Automating semantic labelling for termination proofs is a combinatorially hard problem since the number of algebras grows prohibitively large even for small domains. We report on experiments with our tools Matchbox and MnM, comparing various model finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras.

0

cs.AI 2026-07-01

PolicyGuard turns policies into symbolic rules and LLM questions for compliance checks

by Sameer Malik, Ayush Singh +1 more

PolicyGuard: From Organizational Policies to Neuro-SymbolicCompliance Review Engines

Separating formal logic from local document interpretation makes reviews inspectable, updatable, and testable on tasks like NDA clause evalu

abstract click to expand

Policy-grounded document review requires determining whether a target document complies with organization-specific policies, guidelines, or playbooks. While large language models can assist with policy interpretation and document analysis, end-to-end prompting leaves the applied policy logic implicit, making compliance decisions difficult to inspect, update, and test. We present PolicyGuard, a neuro-symbolic framework for policy-grounded document compliance review. PolicyGuard converts organizational policy guidance into an executable review engine consisting of typed relational logic rules and atom-level extraction questions. During review, LLMs answer these local questions using retrieved document evidence, and a symbolic evaluator applies the formal rules to detect non-compliance. We instantiate and evaluate PolicyGuard on company-specific NDA compliance review, where contract clauses must be checked against organization-specific negotiation policies. By separating policy formalization, local document interpretation, and symbolic compliance evaluation, PolicyGuard makes document review more explicit, maintainable, and systematically testable.

0

cs.LO 2026-07-01

Selection method generalized to wK4 gives frame proof of FMP

by Simon Santschi, Niels C. Vooijs

Logics Containing wK4: Selection \`a la Fine

Transparent construction replaces algebraic proofs and unifies Fine's finite model and finite width theorems for strongly cofinal subframe l

abstract click to expand

We generalize Fine's Iterative Selection Method to the weakly transitive setting. In particular, this provides a transparent frame-theoretic proof of the finite model property for (strongly) cofinal subframe logics extending wK4, which was previously established using algebraic methods. Using the same construction, we generalize Fine's Finite Width Theorem to the weakly transitive setting, connecting these two celebrated theorems of Fine.

0

cs.LO 2026-07-01

Generalized Medvedev logics lack finite axiomatizations

by Han Xiao (Tsinghua University)

Non-finite Axiomatizability of Generalized Medvedev Logics

Topless products of rooted frames with a top yield logics that cannot be captured by any finite set of axioms, settling two open conjectures

abstract click to expand

We introduce a generalized form of Medvedev logics obtained by removing the greatest element from finite products of rooted Kripke frames with a top. We show that, before removing the top, the intermediate logic characterized by such finite products is exactly KC. Classical Medvedev logic is characterized by topless products of 2-chains, and a theorem of Maksimova, Skvortsov and Shehtman establishes that it is not finitely axiomatizable. Motivated by this result, Nick Bezhanishvili conjectured that non-finite axiomatizability extends to topless products of arbitrary finite chains and, more generally, to topless products of finite rooted frames with a top. We prove that every such generalized Medvedev logic is not finitely axiomatizable, thereby settling both conjectures in the affirmative. In 2003, van Benthem, Guram Bezhanishvili, and Gehrke introduced Cheq, the logic of chequered sets, and we show that whenever Cheq is a sublogic of a generalized Medvedev logic, the latter is not finitely axiomatizable over Cheq. Finally, we investigate the order structure of generalized Medvedev logics. We prove that there are at least countably many distinct generalized Medvedev logics and that no least such logic exists. These results extend the classical theory of Medvedev logic and clarify the behaviour of intermediate logics generated by topless product constructions.

0

cs.LO 2026-07-01

Logic adds degrees and comparisons to understanding

by Yu Wei (Department of Philosophy, East China Normal University)

Better Understanding, Understanding Better

Level-indexed modalities and graded structures let models compare how well different agents understand the same proposition.

abstract click to expand

"Any fool can know; the point is to understand." A well-known remark often attributed to Einstein captures a widely shared intuition: understanding is more than merely knowing. Yet epistemic logic has paid relatively little attention to understanding, despite its central role in contemporary epistemology, philosophy of science, and recent debates about AI. A recurring theme in the philosophical literature is that, unlike knowledge, understanding comes in degrees: one may understand something more or less well, and one's understanding may be better than another's. We introduce a comparative epistemic logic of understanding with level-indexed understanding modalities and a comparative connective for saying that one agent understands why a proposition better than another agent does. Semantically, we enrich multi-agent epistemic models with agent-indexed graded explanation structures and a justification-style term algebra. This yields a unified framework for representing minimal, ordinary, more demanding, and ideal understanding, together with comparisons between agents with respect to the same formula at issue. We distinguish a finitary bounded-level calculus from an infinitary full-language companion system. We establish soundness and strong completeness, and show that each fixed finite-level fragment is decidable.

0

cs.LO 2026-07-01

Knowing-value logic with successor gets finite model property

by Hongyi Wang (Department of Philosophy, Peking University)

Knowing-Value Logic with Successor Arithmetic

Axiomatization is strongly complete for non-standard models and weakly complete for standard models; solves consecutive numbers puzzle

abstract click to expand

In their prior work, Wang and Fan proposed conditional knowing-value logic and provided a complete axiomatization. However, in natural language scenarios and logic puzzles, knowing-value reasoning often appears together with arithmetic operations, which motivates us to enrich knowing-value logic with arithmetic function symbols. In this paper, we extend the language of conditional knowing-value logic with equality and the successor function. Due to the failure of compactness over the class of standard models, we additionally introduce non-standard models to facilitate the technical analysis. Our main results establish the finite model property and provide an axiomatization that is strongly complete with respect to the class of non-standard models and weakly complete with respect to the class of standard models. Furthermore, we extend our logic with public announcement operators and use the resulting system to formalize and solve the "Consecutive Numbers" puzzle. This work provides a novel framework for integrating epistemic logic with arithmetic.

0

cs.LO 2026-07-01

GLS gains uniform Lyndon interpolation via non-wellfounded proofs

by Borja Sierra Miranda (University of Bern), Thomas Studer (University of Bern)

Uniform Lyndon Interpolation via Non-wellfounded Proofs

The result settles an open question and supplies an alternative cut-elimination argument.

abstract click to expand

Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to prove uniform Lyndon interpolation. We close this gap by showing uniform Lyndon interpolation for the provability logic GLS. This logic was known to have uniform interpolation, but it was open whether it has uniform Lyndon interpolation (or at least non-uniform Lyndon interpolation). The methodology we provide is easy to adapt to other provability logics if a non-wellfounded sequent calculus is available for them. In addition, we offer an alternative proof of cut elimination for GLS via non-wellfounded proofs.

0

cs.LO 2026-07-01

TEL stays sound when base logic turns relevant or intuitionistic

by Igor Sedlár (Institute of Computer Science, Czech Academy of Sciences)

Non-classical Topological Evidence Logic

An interior-of-complement operator lets coherent justification be expressed in the weak relevant modal logic BS4 with full soundness and com

abstract click to expand

Topological Evidence Logic (TEL) is a recent approach to epistemic logic that uses topological tools to model coherent epistemic justification. Specifically, a hypothesis is coherently justified if and only if it is entailed by a dense open set. In its simplest form, TEL can be formulated as an extension of S4 with a global modality. All currently studied forms of TEL are based on classical propositional logic, which has been heavily criticised for misrepresenting the way in which ordinary agents reason. In this article, we show that the TEL approach is robust under modifications to the propositional base. We show that an extension of the intuitionistic modal framework recently introduced by de Groot and Shillito, incorporating a global modality, enables coherent justification to be expressed in an intuitionistic setting. Furthermore, we adapt the recent work of Standefer et al., which extends relevant logic with a global modality, to show that coherent justification can be expressed in a relevant setting if an interior-of-complement operator is added to the language. Our main technical result is a soundness and completeness theorem for relevant TEL based on the weak relevant modal logic BS4.

0

cs.LO 2026-07-01

Tense logic gains uniform interpolation via bisimulation extension

by Katsuhiko Sano (Hokkaido University)

Uniform Interpolation of Basic Tense Logic

The semantic argument for modal logic adapts to the converse relation without new conditions

abstract click to expand

This paper establishes the uniform interpolation theorem for basic tense logic, which is also known as two-way modal logic or modal logic with converse. First introduced by Arthur Prior, basic tense logic is a syntactic expansion of basic modal logic with a converse modality. Its corresponding accessibility relation is defined as the converse of the standard accessibility relation in a given Kripke model. Although basic tense logic has been widely studied since its introduction, its uniform interpolation property has yet to be fully established. For basic modal logic K, Albert Visser (1996) provided a semantic argument formulated in terms of layered (or bounded) bisimulation, explicitly attributing the uniform interpolation property of K to Silvio Ghilardi. This paper extends Visser's semantic argument to demonstrate that basic tense logic also enjoys the uniform interpolation property.

0

cs.MA 2026-07-01

Analytic cut holds for distributed knowledge logics

by Ryo Murai (Independent Researcher), Sizhuo Liu (Hokkaido University) +1 more

Analytic Cut in Epistemic Logics with Distributed Knowledge

Sequent calculi based on K45, KD45 and S5 admit restricted cut and therefore Craig interpolation, including when the empty group is allowed.

abstract click to expand

Distributed knowledge is a notion of group knowledge studied in multi-agent epistemic logic. Semantically, the distributed knowledge of a group is interpreted via an accessibility relation given by the intersection of the epistemic accessibility relations of the agents in that group. This paper investigates sequent calculi for epistemic logics of distributed knowledge based on K45, KD45, and S5. While cut elimination holds in existing sequent calculi for modal logics K45 and KD45, it fails in all the systems mentioned above. Instead, we establish the analytic cut property for all three systems by adapting Takano' s (2018) strategy, which restricts the cut formulas to the set of subformulas of the conclusion of the cut rule. As a corollary, the Craig interpolation theorem holds for all logics considered. We also show that all proof-theoretic results remain valid when the empty group is allowed for the distributed-knowledge operator, in which case the distributed knowledge for the empty group is interpreted as the global modality.

0

math.LO 2026-07-01

Halo operator equals ω-accumulation points on every space

by Yoàv Montacute

Halo Semantics for Modal Logic

The resulting operator satisfies axiom 4 without separation axioms and yields completeness of K4 for all infinite spaces.

abstract click to expand

In nonstandard analysis the halo of a point in a topological space is the intersection of the nonstandard extensions of all its open neighbourhoods. We define a parametric family of modal operators from the halo by varying which elements of the nonstandard extension are admitted as witnesses, and identify four canonical instances. Two recover well-known modalities: the topological closure and the Cantor derivative. A third reduces to Kripke semantics over the specialisation preorder. The fourth, purely nonstandard instance admits only nonstandard witnesses. The Transfer Principle forces it to coincide with the $\omega$-accumulation point operator, a classical topological notion not previously studied in modal logic. Unlike the Cantor derivative, the $\omega$-accumulation operator maps arbitrary sets to closed sets without any separation axiom, yielding an $\omega$-Cantor-Bendixson decomposition on all topological spaces. Axiom 4 holds universally, again without separation conditions. We prove that K4 is the complete logic over infinite spaces, and GL over infinite $\omega$-scattered spaces.

0

cs.LO 2026-07-01

Modular models yield realisation theorem for intuitionistic justification logic

by Sonia Marin (University of Birmingham), Paaras Padhiar (University of Birmingham) +1 more

Intuitionistic Justification Logic, Semantically

Semantic bridge shows every theorem of the modal logic has an explicit realizing term

abstract click to expand

Justification logics are explicit versions of modal logic. In the classical setting, this means boxes are refined with explicit proof terms and interact with each other through proof operations. This exercise was extended to intuitionistic modal logic with native diamonds. In this setting, diamonds are refined to satisfier terms and come equipped with additional operations. Justification logic enjoys a connection to its corresponding modal logic through a realisation theorem. In the classical setting, this is achieved through either proof-theoretic or semantic methodology. So far, intuitionistic justification logic with satisfiers has only been presented syntactically with a proof-theoretic realisation theorem. We present two classes of semantics for intuitionistic justification logic with soundness and completeness results: basic modular models, which extend possible world semantics for intuitionistic propositional logic; modular models which contain Kripke-style machinery to promote "backwards compatibility" to modal logic. Using modular models, we present a realisation theorem to establish a connection between intuitionistic justification logic and its corresponding intuitionistic modal logic.

0

math.LO 2026-07-01

Translations map relevant logics into normal modal logics

by S{o}ren Brinck Knudstorp

Possibly Relevant Translations

The mappings clarify structural links between the logics and produce corollary results while raising further questions.

abstract click to expand

We develop translations from relevant logics into normal modal logics, and use them to clarify structural connections between relevant and modal logic, obtain a few corollary results, and raise questions for future work.

0

cs.LO 2026-07-01

Modal logics axiomatize a-connected and connected metric spaces

by John Harding (New Mexico State University), Ilya Shapirovsky (New Mexico State University)

On Modal Logics of Connectedness in Metric Spaces

Complete systems given for distance-modality language on a-connected spaces and for topological-plus-distance language on classically connec

abstract click to expand

For a positive number a, each metric space carries the relation D_a consisting of those pairs that are of distance less than a apart. A space X is said to be a-connected, if the graph (X,D_a) is connected (that is, there is a D_a-path between every pair of points in X). We give a complete axiomatization of a-connected metric spaces in the language with a family of distance modalities and the universal modality. Then we give a complete axiomatization of the logic of connected (in the classical topological sense) metric spaces in the language with the topological modality, universal modality, and a single distance modality. We also show that these logics have the finite model property.

0

math.LO 2026-07-01

Intuitionistic K matches the bisimulation-invariant fragment of intuitionistic FOL

by Jim de Groot, João Marcos +1 more

Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

IK formulas are exactly those first-order properties preserved under the defined IK-bisimulations on relational models.

abstract click to expand

We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic. En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Los's Theorem, elementary embeddings and countable saturation.

0

cs.LO 2026-07-01

KSP oracle lifts CEGAR-tableaux past pure methods

by Rajeev Goré (Faculty of Information Technology, Monash University +2 more

Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

Hybrid modal solver outperforms standalone tableaux and standalone resolution on large satisfiable problems.

abstract click to expand

We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.

0

cs.LO 2026-07-01

Shallow calculus bounds FIK decision problem to EXPSPACE

by Han Gao (Institute of Computer Science, Czech Academy of Sciences) +2 more

Taming Complexity in Intuitionistic Modal Logic: The Case of FIK and Its Shallow Calculus

Nested sequents limited to one level of nesting establish the EXPSPACE upper bound for this logic between CCDL and IK.

abstract click to expand

Intuitionistic modal logics (IMLs) comprise many systems: from constructive modal logics such as CK and Wijesekera's CCDL to Fischer Servi/Simpson's IK, as well as some recently introduced variants. All of them are characterized by bi-relational semantics and have complete axiomatisations. However, from the perspective of proof theory and complexity, there are strong differences: while for constructive modal logics simple Gentzen calculi suffice, for IK more complex calculi, based on nested or labelled sequents, are needed. As a consequence, the decision problem for constructive modal logics has a PSPACE upper bound, whereas for IK is not known and it is even conjectured to be non-elementary. We study here the proof theory and complexity of FIK, a natural intuitionistic modal logic recently introduced. FIK is strictly in between CCDL and IK, yet it has the same forcing conditions as IK. We define a "shallow" sequent calculus for FIK which is a nested sequent calculus where sequents have at most one level of nesting. We prove its syntactic completeness by showing the admissibility of cut. By means of this calculus we show that decision problem for FIK is in EXPSPACE, whence significantly lower than the complexity conjectured for IK.

0

cs.LO 2026-07-01

Axioms complete for path-reachability in T1 and metric spaces

by Aleksandr Gagarin, David Fernández-Duque

Topological Logics of Path-Reachability

One system is sound and complete for both classes and decidable via an equivalent neighborhood semantics.

abstract click to expand

The topological semantics of modal logic has been an active area of research ever since their introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. In particular, an Until-like path-reachability modality has recently been studied in Bezhanishvili et al. (2024) in polyhedral semantics; this paper investigates its topological counterpart. Focusing on the language combining said modality with the classical Cantor derivative modality, we exhibit an axiomatic system sound and complete both for the class of T1 topologies and for the class of all metric spaces, and establish its decidability. We also axiomatize the logic of all topological models in a weaker language obtained by substituting the closure modality for the Cantor derivative. To prove our results, we introduce an equivalent neighborhood-like semantics allowing for the finite model property.

0

cs.LO 2026-07-01

B-Box closed under modal-nesting substitutions

by Thomas Macaulay Ferguson (Rensselaer Polytechnic Institute), Shay Allen Logan (Kansas State University)

Hyperformalism for Relevant Modal Logics

MPos-hyperformalism extends hyperformalism to relevant modal logics, with K-MPos as largest sublogic of K.

abstract click to expand

The property of hyperformalism has proven to be a powerful tool in the analysis of relevant logics, revealing that increasingly weak relevant logics are closed under increasingly strong classes of non-uniform substitutions. In such substitutions, two instances of the same atom may be treated independently in virtue of syntactic features of their appearances in a complex. In this work, we extend the scope of hyperformalism to relevant modal logics by considering MPos-hyperformalism, that is, a property in which relevant modal logics are closed under substitutions in which nesting within the scope of modal operators is taken into account. We prove that the weak relevant modal logic B-Box is MPos-hyperformal and investigate the classes of non-uniform substitutions under which several extensions are closed. We then consider corresponding refinements of the variable sharing property that hold of such logics. We conclude by introducing a modal logic K-MPos that constitutes the largest MPos-hyperformal sublogic of the classical modal logic K and provide soundness and completeness results.

0

cs.LO 2026-07-01

Calculus for intuitionistic monotone modal logic proves decidability

by Tiziano Dalmonte, Jim de Groot

Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

Adapting the classical M system yields cut-elimination, neighbourhood semantics for extensions, and an analogy with intuitionistic K.

abstract click to expand

We study the recently introduced intuitionistic monotone modal logic IM. We first provide a semantic characterisation for a family of natural extensions of IM in terms of constructive neighbourhood models. We then present a calculus for IM and its extensions, obtained by adapting a structured calculus for the classical monotone modal logic M. Based on the calculus, we prove some preliminary results for IM, including its decidability. Our calculus also reveals an interesting analogy between constructive and intuitionistic variants of M and the corresponding variants of K, thereby further justifying IM as a faithful intuitionistic variant of M.

0

math.LO 2026-07-01

Quasivarieties with infinite irreducibles lack strong structural completeness

by Alex Citkin (Metropolitan Telecommunications, NewYork USA)

On Strong Structural Completeness of Varieties and Quasivarieties

Finite-type quasivarieties generated by finite algebras and having the CEP cannot be generated as a prevariety by free algebras when they co

abstract click to expand

We study structural completeness in the infinitary sense (strong structural completeness) in an algebraic setting. A variety is structurally complete (SCpl) if it is generated, as a quasivariety, by its free algebras, and it is strongly structurally complete (SSCpl) if it is generated, as a prevariety, by its free algebras. A quasivariety is SSCpl if it is generated, as a prevariety, by its free algebras. We prove that every quasivariety of finite type with the CEP that is generated by finite algebras and contains an infinite irreducible algebra is not SSCpl. Moreover, every congruence meet-semidistributive variety of finite type generated by finite algebras is SSCpl if and only if it is tabular. Thus, Dummett's and Medvedev's logics are SCpl but not SSCpl. A variety is primitive if it is SCpl and all its subvarieties are SCpl; it is strongly primitive if it is SSCpl and all its subvarieties are SSCpl. We prove that in primitive congruence-distributive varieties of finite type, the tabular subvarieties, and only those, are strongly primitive. This observation also yields a criterion for strong primitivity.

0

cs.LO 2026-07-01

Labelled sequents yield complete proof system for inquisitive modal logic

by Ivano Ciardelli (University of Padua), Simone Conti (University of Padua)

Labelled Sequents for Inquisitive First-Order Modal Logic

Extension of prior calculus establishes strong completeness plus rule invertibility and cut admissibility.

abstract click to expand

In recent work, an inquisitive first-order modal logic has been proposed to reason about relations of modal dependence, including the notion of global supervenience (functional dependence among the extensions of predicates relative to a space of possibilities). At present, no proof system exists for this logic. We provide a complete labelled sequent calculus, extending a calculus developed by Litak and Sano for a weak version of inquisitive first-order logic. We prove strong completeness for the calculus and show that it enjoys desirable structural properties, including the invertibility of its rules and the admissibility of cut.

0

cs.LO 2026-07-01

Logic models what agents determine as well as what they force

by Ivano Ciardelli (University of Padua)

Inquisitive Action Logic

InqAL uses questions over concurrent game structures, matches a coalition logic fragment, and is decidable.

abstract click to expand

We introduce inquisitive action logic, InqAL, a multi-agent modal logic for reasoning about action. While traditional approaches focus on what properties of the outcome an agent can force, InqAL also captures what aspects of the outcome an agent determines through their actions. As we argue, such claims of agentive determination are naturally analyzed as modal claims involving questions. Technically, InqAL is a multi-agent extension of inquisitive neighborhood logic based on concurrent game structures. With respect to statements, it is expressively equivalent to the individual-agent fragment of the socially friendly coalition logic recently proposed by Goranko and Enqvist. We present an axiomatization of InqAL and prove completeness and decidability via the finite model property. Along the way, we establish a representation theorem for actual effectivity functions, associating to an agent the sets of outcomes corresponding to their possible actions; we give exact conditions under which a multi-agent neighborhood frame arises from a concurrent game structure.

0

cs.LO 2026-07-01

Most properties undecidable for transitive tense logics

by Qian Chen (The Tsinghua-UvA JRC for Logic, Department of Philosophy +5 more

Most Properties are Undecidable for Transitive Tense Logics

Adapting Minsky machine reductions shows no algorithm decides Kripke completeness or finite model property in NExt(K4t).

abstract click to expand

A logics' property is decidable in a class of logics if there exists an algorithm that decides whether a finitely axiomatizable logic in the class has the property. Many properties are undecidable for bimodal logics but decidable for linear tense logics, which leads to a general question on how the interactions of modalities affect the decidability of properties. In this paper, we study the decidability of properties for transitive tense logics and show that most properties are undecidable in the lattice NExt(K4t) of transitive tense logics, including Kripke completeness, the finite model property, and decidability. Our proof method adapts Chagrov's approach of constructing a reduction from an undecidable problem of Minsky machines to the decision problem for logics' properties, yielding a general scheme of proving the undecidability of these properties.

0

math.LO 2026-07-01

Modal measurable logics complete via Loomis-Sikorski extension

by Nick Bezhanishvili, Jim de Groot +1 more

Modal Measurable Logics via a Modal Loomis-Sikorski Representation Theorem

The result equips logics with countable operations for use in measure theory and ergodic theory with a sound and complete semantics.

abstract click to expand

We investigate a modal extension of the infinitary classical logic with countable meets and joins, formulated with an eye toward measure-theoretic work in dynamical systems and in point-free ergodic theory. We define a modal formalism in this language, which we call modal measurable logics. We also introduce a Kripke-like semantics for these logics in measurable spaces taking a designated modal sigma-ideal into consideration. Using a restriction of Jonsson-Tarski duality and a modal extension of the Loomis-Sikorski theorem, we prove completeness of modal measurable logics with respect to this new semantics.

0

cs.LO 2026-07-01

Belief contraction defined on standard Kripke models

by Gaia Belardinelli (Stanford University), Snow Zhang (University of Berkeley +1 more

Belief Contraction in Dynamic Epistemic Logic

Direct mechanism on unconstrained models handles cases like hedged announcements that plausibility models cannot.

abstract click to expand

Dynamic epistemic logic represents belief change via model transformations induced by epistemic events. Its standard formulation (Baltag, Moss, Solecki, 1998) provides a natural account of belief expansion through the elimination of possibilities, but it cannot model belief contraction about factual propositions. A classic response enriches Kripke models with plausibility orderings, representing contraction as an update that promotes certain possibilities over others. We show that this approach has expressive limitations. In particular, the approach cannot model belief that violates positive introspection and contraction dynamics in response to a hedged public announcement that phi might be false. Motivated by these considerations, we introduce a mechanism for belief contraction defined directly on standard Kripke models, without any constraints on the doxastic accessibility relation. We show that it satisfies some of the standard properties of belief contraction but not others, study the conditions under which contraction may be unsuccessful, and provide a sound and complete axiomatization of the logic via reduction axioms. We also define a more general dynamic logic that is an extension of standard DEL and accommodates belief contractions due to events such as private or semi-private announcements, and provide a complete and sound axiomatization of the general logic.

0

cs.LO 2026-07-01

Labelled calculi prove four team logics sound and complete

by Fausto Barbero, Marianna Girlando +2 more

Labelled Sequent Calculi for Propositional Team Logics

The systems cover basic inquisitive logic, intuitionistic dependence logic and both with tensor disjunction, all restricted to finite atoms.

abstract click to expand

Team semantics is a general framework where formulas are not interpreted with respect to a single point of evaluation, but with respect to sets of such points. Team semantics is used in dependence logic, to reason about dependencies between variables, and in inquisitive logic, to formalize the meaning of questions. We provide sound and complete labelled sequent calculi for four logics based on team semantics: basic inquisitive logic, propositional intuitionistic dependence logic, and their respective extensions with tensor disjunction. For technical reasons, we restrict ourselves to languages with finitely many propositional atoms. The rules of weakening, contraction and cut are shown to be admissible in each of our calculi. In the last part of the paper, we present terminating proof search procedures for variants of our proof systems, in which labels have a simplified structure.

0

math.LO 2026-07-01

iEx-logic extensions form product of intermediate and orthomodular lattices

by Juan P. Aguilera (TU Wien), Guillaume Massas (Chapman University)

Conditionals and Modalities in Constructive Quantum Logics

Any extension arises by independent choice of one intermediate logic and one orthomodular logic.

abstract click to expand

We investigate logics that generalize both intuitionistic logic and quantum logic. In earlier work, we introduced Ex-logic, an extension of Holliday's fundamental logic that coincides with the intersection of orthologic and the implication-free fragment of intuitionistic logic. In this paper, we add an implication connective to Ex-logic and axiomatize iEx-logic, the intersection of full intuitionistic logic and orthomodular logic with the implication connective interpreted as the Sasaki hook. As a consequence, we obtain a characterization of the lattice of logics extending iEx-logic as the product of the lattice of intermediate logics and the lattice of orthomodular logics. We also explore the robustness of our algebraic approach by briefly discussing extensions of iEx-logic with modal operators.

0

cs.CR 2026-07-01

LLM attacks organized across eight lifecycle stages

by Seyed Bagher Hashemi Natanzi, Bo Tang

A Lifecycle and Application-Stack Survey of Large Language Model Vulnerabilities: Attacks, Risks, Defenses, and Open Problems

Mapping vulnerabilities from data collection to deployment shows why isolated defenses fail to protect systems that use tools and memory.

abstract click to expand

Large language models are no longer only text generators. They are increasingly embedded in retrieval pipelines, enterprise assistants, coding environments, robotic systems, security-operation workflows, and autonomous agents that can read private data, call tools, write files, execute code, and act across organizational boundaries. This shift changes the security problem: risks do not arise from the model weights alone, but from the full lifecycle and application stack through which data, prompts, model outputs, tools, memories, and user authority interact. This paper systematizes the literature on vulnerabilities in large language model systems through a lifecycle and application-stack lens. We organize attacks across eight stages: data collection, pretraining, post-training alignment, model packaging and supply chain, retrieval and memory, prompting and inference, tool/agent execution, and deployment/maintenance. For each stage, we analyze attacker capabilities, affected security objectives, representative attacks, practical risks, evaluation practices, and defenses. We further map LLM-specific vulnerabilities to confidentiality, integrity, availability, safety, privacy, fairness, accountability, and agency-control objectives. Unlike taxonomies that list isolated attack names, the proposed systematization emphasizes where trust boundaries fail, how untrusted data becomes executable instruction, how delegated authority amplifies model errors, and why point defenses rarely compose. We close with a research agenda for secure LLM systems, including compositional security, provenance-aware retrieval, tool-call containment, long-horizon agent evaluation, privacy-preserving adaptation, realistic red teaming, and deployment-grade incident response.

0

cs.LO 2026-07-01

Encoding maps spatial closure models to transition systems for CoPa minimisation

by Vincenzo Ciancia, Jan Friso Groote +3 more

Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

Branching bisimilarity algorithms then compute the correct partitions, enabling faster spatial property checking on large images.

abstract click to expand

Spatial models are of increasing interest in traditional computer science domains and beyond. Spatial minimisation procedures are crucial for efficient model checking of such models that are often large in size. For the recent notion of spatial bisimilarity for quasi-discrete closure models, called `Compatible Paths' (CoPa) bisimilarity, an effective minimisation method is proposed, and shown to be correct. Reasoning about space represented by quasi-discrete closure models involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality, representing the fact that a point can be reached from another point, under certain conditions. The core of our minimisation method is the encoding of closure models as labelled transition systems, enabling minimisation algorithms for branching bisimilarity to compute CoPa equivalence classes. A prototype toolchain, VoxMinX, is proposed to validate the minimisation method. VoxMinX preserves the relationship between equivalence classes and sets of pixels in the original image. Experimental validation of the toolchain via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.

0

cs.LO 2026-07-01

Equation encoding plus intervention finds causes beyond but-for in argumentation

by Siyi Liu, Muyun Shao +1 more

Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)

New operator handles preemption and overdetermination by fixing witnesses and changing argument sets simultaneously.

abstract click to expand

Counterfactual explanation in abstract argumentation calls for an answer to the what-if query: would the topic argument still be accepted if the status of certain other arguments were changed? Existing approaches are limited to the but-for test and fail to accommodate more refined counterfactual conditions. To overcome these limitations, we introduce an intervention-based counterfactual reasoning framework in abstract argumentation. Our approach encodes the acceptance conditions of arguments as equations, then defines an intervention operator that supports (1) changing sets of arguments simultaneously, and (2) fixing witness arguments to their actual labels. Guided by the refined counterfactual condition introduced in the Halpern-Pearl definition, our method goes beyond the but-for test, thereby correctly identifying causes in argumentation structures such as Preemption and Overdetermination. Through comparison, we show that our method surpasses prior methods in both expressiveness and reliability.

0

cs.AI 2026-07-01

Lean agents compile 89.5% but only 60.5% are faithful

by Ke Zhang, Patricio Gallardo Candela +4 more

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Compilation checks miss statements that omit hypotheses or change meaning, leaving a 29-point gap on a 400-problem graduate benchmark.

abstract click to expand

Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400-entry graduate-level benchmark spanning real analysis, complex analysis, topology, and algebra, our protocol combines Lean compilation, cross-model semantic judging, and human expert calibration. The resulting picture is different from compile-rate evaluation: a full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap. Targeted human audits support the metric as a conservative decision boundary: across available case-level audits, 96.0% of consensus-positive outputs are human-confirmed faithful, while 82.4% of compile-pass consensus-negative outputs are human-confirmed semantic failures. Under this metric, existing one-shot formalizer models and prover-oriented Lean models remain low, suggesting that formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately. We then use a full $2^3$ factorial design to decompose three recurring interventions in formalization pipelines: parametric expert drafting, Mathlib/context search, and Lean elaboration feedback. Elaboration feedback is the largest validity intervention, but it also exposes a larger compile-pass semantic-failure bucket; search mainly improves grounding and selectivity; and fine-tuned drafting is largely substitutable in this tool stack once feedback and grounding are available.

0

cs.AI 2026-06-30

HyperLTL guides multi-agent RL under partial views

by Arshia Rafieioskouei, Tzu-Han Hsu +2 more

HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation

HyPOLE combines hyperproperty specifications with CTDE and reports gains over baselines on SMAC and WildFire tasks.

abstract click to expand

Formal specification is a powerful tool to guide the learning process and provides significant advantages over reward shaping: (1) mathematical rigor; (2) expressiveness to specify objectives and constraints, and (3) the ability to define tactics to achieve objectives. However, these benefits remain largely unexplored in the context of Multi-Agent Reinforcement Learning (MARL). This paper introduces HyPOLE, a novel framework for MARL under partial observability, where learning is guided by the expressive power of the so-called hyperproperties and, in particular, the temporal logic HyperLTL. We integrate Centralized Training for Decentralized Execution (CTDE) techniques with HyPOLE to synthesize decentralized policies, and our evaluation on SMAC, MessySMAC, and WildFire benchmark demonstrates clear advantages over baselines.

0

cs.LO 2026-06-30

Decision procedure for nested datatypes proven correct

by Tomer Hakak, Yoni Zohar +3 more

Automated Reasoning with Nested Datatypes

Restricting datatype and array mixes avoids bad models and yields a decidable theory.

abstract click to expand

We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging. A decision procedure for the theory is given and proven correct. Finally, we describe an implementation of the procedure, as well as an evaluation over both real-world and crafted benchmarks.

0

cs.FL 2026-06-30

DLSL phase expansions equal fiber-linear graph-respecting transducers

by Reda Belaiche

Destination-Labeled Self-Looping Systems with Dwell: Intrinsic Characterization, Realization Cost, and Recognition

Visible transduction fixes dwells and decisions; realizations need exactly sum of dwell values in states.

abstract click to expand

We study a finite-state symbolic controller for systems in which the admissible visible transitions are fixed in advance and each visible state carries a minimum dwell requirement. The resulting model, which we call a destination-labeled self-looping system with dwell (DLSL system), records the visible graph together with local decision maps; dwell memory appears only after phase expansion. The main structural issue is that, once dwell is imposed, the current visible state no longer determines whether a departure is allowed. This leads to the converse problem: which deterministic transducers arise as phase-expanded realizations of DLSL systems over a fixed visible graph? We show that the answer is exactly the class of fiber-linear graph-respecting transducers. Under natural reachability and realizable-departure assumptions, equivalent accessible realizations over the same visible graph are isomorphic; in particular, the visible transduction determines the dwell vector and the local decision maps. We also prove that any graph-preserving deterministic realization enforcing dwell values $(d_i)$ requires exactly $\sum_i d_i$ control states. Finally, we give an $O(|Q||\Omega|)$ recognition and reconstruction procedure, and extend the analysis to an edge-entry variant in which transitions may enter interior phases of successor fibers.

0

cs.LO 2026-06-30

Lean 4 formalizes Scott's 1972 continuous lattices

by Lars Warren Ericson

A Lean 4 Formalization of Scott's Continuous Lattices (1972)

Machine-checked proofs cover the 43 results establishing a model for the untyped lambda calculus.

abstract click to expand

We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \emph{Continuous Lattices} \textbf{[Sco72]}, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in \textbf{[Sco72]} (pp.~135--136). Scott's paper develops a model for $\lambda$-calculus from a topological starting point. He defines \emph{injective} $T_0$-spaces -- those with a strong extension property for continuous maps -- and shows that they are exactly the \emph{continuous lattices}: complete lattices whose Scott topology is determined by the order via the way-below relation ($\ll$). On this foundation he studies projections, retractions, products, function spaces, and inverse limits. The capstone (Theorem 4.4) constructs an inverse limit $D_\infty$ of function-space approximants and proves $D_\infty \cong [D_\infty \to D_\infty]$, yielding a purely mathematical model for Church's untyped $\lambda$-calculus. Our development formalizes \textbf{43 numbered results} from Scott's Sections 1--4 (Propositions, Corollaries, Lemmas, and Theorems), each as a sorry-free Lean theorem, together with supporting infrastructure (step functions, the $\Uparrow a$ basis of Scott opens, Milner's coarser-than-Scott hypothesis, the function-space tower, and the $i_\infty$/$j_\infty$ pair). The formalization is \textbf{classical} (uses \texttt{Classical.choice} transitively) and follows Scott's proof dependency order. Where the Lean proof required choices not visible in the original -- or where dead ends were encountered -- we record detailed notes in Section 5. All proofs check with the standard footprint $\texttt{[propext, Classical.choice, Quot.sound]}$.

0

cs.LO 2026-06-30

LTL ∩ PCTL is decidable via DBW equivalence

by Massimo Benerecetti, Dario Della Monica +3 more

Deciding the Common Fragment of CTL with Past and LTL

An LTL formula lies in PCTL exactly when it is recognized by a deterministic Büchi word automaton, making the common fragment decidable.

abstract click to expand

A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determining the \emph{common fragment} of two formalisms $F_1$ and $F_2$, that is, effectively characterise the class $F_1\cap F_2$ of properties that can be expressed in both formalisms. A question closely related to this is the \emph{membership problem}, denoted $F_1 \membership F_2$, which asks whether a property expressed in $F_1$ can be also expressed in $F_2$. These problems become particularly difficult when \emph{branching-time} formalisms are involved. In this work, we prove that $\LTL \cap \PCTL$ is decidable, where \PCTL denotes \CTL extended with \emph{past operators}. We do this by showing that both membership problems, $\LTL \membership \PCTL$ and $\PCTL \membership \LTL$, are decidable. The direction $\PCTL \membership \LTL$ follows from suitable combinations of known results. The converse direction, $\LTL \membership \PCTL$, requires an automata-theoretic characterisation of $\PCTL$. Specifically, we introduce a new class of automata, called \emph{counter-free hesitant weak tree automata} ($\HWTcf$) that capture precisely the expressiveness of $\PCTL$, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, \emph{counter-free hesitancy} and \emph{weakness}. We prove that, for every word language $L$ defined by an \LTL formula, the associated tree language $\triangle[L]$ is recognisable by an \HWTcf if and only if $L$ is recognized by a \DBW. Since the latter recognisability problem is decidable, so is the former. This result advances the longstanding open problem of deciding $\LTL \cap \CTL$. Indeed, that problem can now be reduced to $\PCTL \membership \CTL$, that is, the question of when past operators can be eliminated.

0

cs.LO 2026-06-30

GKAT equivalence stays nearly linear-time decidable with Hoare hypotheses

by Jurriaan Rot, Todd Schmid +1 more

GKAT with Hoare Hypotheses

The extension lets users record pre- and post-condition assumptions while the automata check keeps its original speed bound.

abstract click to expand

Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the current paper, we address the challenge of reasoning under assumptions about these programs. In particular, we develop a form of Hoare hypotheses, which allow modelling basic domain knowledge on pre- and post-conditions of uninterpreted basic programs, and which are well-developed for classical Kleene algebra but not yet for GKAT. We show that the resulting axiomatisation is sound and complete. We then extend Hoare hypotheses to the more general form of word hypotheses. Based on an automata-theoretic approach, we show that equivalence of GKAT under word hypotheses is as efficiently decidable as for plain GKAT.

0

cs.LO 2026-06-30

Rejection sets validate weak-negation axioms in modal CLoN

by Mahan Vaz, Daniel Skurt

Modal Extensions of CLoN with Bi-neighborhood Semantics

Bi-neighborhood semantics for CLoN extensions supports deontic logics that accommodate dilemmas without trivialization.

abstract click to expand

In this paper we will present neighborhood semantics for non-normal modal extensions of $\clon$, which is a sublogic of {\sf FDE}. Our framework is built upon earlier work on {\sf FDE}-based non-normal modal logics and employs two different neighborhood functions for each modal operator. Despite being a logic with a very weak negation operator, we will show that with the right definition of the rejection sets of the modal operators, we can validate non-trivial axioms that contain the weak negation operator. The philosophical aim of our approach is to construct the basis for deontic logics that are able to accommodate both the usual deontic principles and moral dilemmas, without resulting in trivialization of the system.

0

cs.LO 2026-06-30

New reductions reach non-linear interpretations beyond absolute positiveness

by Carsten Fuhs

Beyond Absolute Positiveness for Universally Quantified Non-Linear Polynomial Constraints

They solve more universally quantified polynomial constraints used to prove termination of term rewrite systems.

abstract click to expand

Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for termination analysis and complexity analysis of term rewrite systems. Finding such polynomial interpretations for a given set of term constraints involves solving a set of $\exists\forall$ inequalities over the natural numbers. Conventionally, the absolute positiveness criterion is used to reduce $\exists\forall$ inequalities to $\exists$ inequalities. This extended abstract reports on work in progress to go beyond absolute positiveness, allowing for finding non-linear polynomial interpretations that were outside the reach of existing techniques.

0

cs.AI 2026-06-30

Neural net safety bounds hold for imprecise input probabilities

by Francesc Pifarre-Esquerda (LIX), Eric Goubault (X-DEP-INFO) +1 more

Propagation of~Interval Belief Structures and~Imprecise Copulas for~Neural Network Verification

Interval belief structures and imprecise copulas propagate to give guaranteed lower and upper bounds valid for all compatible models.

abstract click to expand

Quantitative verification of neural networks requires reasoning about probabilities under substantial uncertainty in both input distributions and their dependence structure. In realistic settings, this information is often only partially specified, and assuming precise probabilistic models can lead to unreliable results. We propose a sound framework for quantitative verification under imprecise probabilistic information, combining interval belief structures to represent marginal uncertainty with imprecise copulas to model uncertain dependence. We develop a propagation method for imprecisely coupled interval belief structures through feed-forward neural networks. Using mixed imprecise copula volumes, we derive sound push-forward constructions through affine transformations and activation functions. The resulting output can provide guaranteed lower and upper bounds on probabilistic safety properties, valid for all probability models compatible with the specified imprecise inputs.

0

cs.FL 2026-06-30

CVASS reachability AC1 in 1D

by Michal Ajdarów, A. R. Balasubramanian +1 more

Reachability in Fixed-Dimensional Continuous VASS

All eight variants show the split, with hardness even on acyclic automata.

abstract click to expand

Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is $\mathsf{NP}$-complete. In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in $\mathsf{AC}^1$, whereas for any dimension at least 2, all of the eight problems are $\mathsf{NP}$-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this result, we present a new technique called the Egyptian prime fractions technique. Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in $\mathsf{AC}^1$, whereas for dimensions 3 and above, all of the problems are $\mathsf{NP}$-complete.

0

cs.AI 2026-06-30

Tensor networks gain first-order temporal logic and quantifiers

by Luca Boscarato, Ivan Donadello +3 more

First-Order Temporal Logic Tensor Networks

FOT-LTN keeps full differentiability while adding always, eventually and time-varying predicates for dynamic knowledge tasks.

abstract click to expand

Most of the existing neuro-symbolic AI methods focus on the scenario of static knowledge where objects do not change according to a temporal dimension. Temporal neuro-symbolic works are still under explored and are mainly developed for time-interval logic or propositional linear temporal logic. There is a lack of models studying linear temporal logics with predicates that deal with objects whose properties and relations change through the time. We present First-Order Temporal Logic Tensor Networks (FOT-LTN) that is an extension of Logic Tensor Networks (LTN) that fills this gap by considering a linear-temporal dimension. In particular, FOT-LTN joins the syntax of First-Order Linear Temporal Logic with the fuzzy (and real-valued) semantics of LTN obtaining a framework that supports both temporal operators and quantifiers and is totally differentiable. A first evaluation regards a temporal knowledge graph completion task on two synthetic datasets showing better performance of FOT-LTN with respect to dedicated (purely neural) methods.

0

math.LO 2026-06-30

Modal translations embed fundamental logic fully into orthologic and intuitionistic varian

by Wesley H. Holliday, Guillaume Massas

Fundamental Logic Through the Lens of Modality

GMT and Goldblatt maps prove full and faithful connections between the systems, allowing direct translation of theorems.

abstract click to expand

Fundamental logic is a non-classical logic based only on the introduction and elimination rules for conjunction, disjunction, negation, and the quantifiers in a Fitch-style natural deduction system. In this paper, we attempt to obtain a better understanding of fundamental logic and its semantics through the lens of modality. Using modal logic, we develop means of mutual understanding between the fundamental logician, on the one hand, and the orthologician and intuitionistic logician, on the other: we prove that the G\"odel-McKinsey-Tarski (GMT) translation of intuitionistic logic into the classical modal logic $\mathsf{S4}$ is a full and faithful embedding of fundamental logic into the orthological version of $\mathsf{S4}$; that the Goldblatt translation of orthologic into the classical modal logic $\mathsf{KTB}$ is a full and faithful embedding of fundamental logic into an intuitionistic version of $\mathsf{KTB}$; and that the GMT translation is a full and faithful embedding of intuitionistic logic into a modal extension of fundamental logic.

0

cs.LO 2026-06-30

Kleene theorem extends to many-sorted algebras

by Lü Gong, Raúl Ruiz Mora +2 more

A Kleene theorem for free many-sorted algebras

A language of one sort is recognizable precisely when regular, given finitary assumptions on the free algebra.

abstract click to expand

In this work, we generalize Kleene's theorem from free single-sorted algebras to free many-sorted algebras. Our main result establishes that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra is recognizable if and only if it is regular.

0

quant-ph 2026-06-30

ZX diagram reduces soft-photon normalization to bare wire

by Soo-Jong Rey

Infrared Safety from ZX-Diagrams: A Categorical Proof of Soft-QED as Open Quantum System

The doubled displacement collapses under unitarity and discard rules, proving the hard QED channel is trace-preserving.

abstract click to expand

The discard ZX-calculus, a diagrammatic language for mixed-state quantum mechanics, is used to give a nonperturbative, categorical proof of the Bloch-Nordsieck cancellation of infrared divergences in QED. Soft photons are treated as an open quantum system: the resolved charged particles and hard photons form the system, while photons below a detector resolution form the environment. The reduced hard channel is a completely positive trace-preserving (CPTP) map, and the soft-photon theorem replaces the full S-matrix by a controlled displacement operator whose Feynman-Vernon influence functional satisfies the equal-history normalization ${\cal F}[J,J]=1 $. In the ZX-calculus, this normalization is a single diagrammatic identity: the doubled displacement diagram collapses to the bare wire under the unitarity, cyclicity, and discard rules. The proof therefore serves as a categorical consistency check on the open-system treatment of soft QED given in a companion paper; it confirms that the physical derivation is logically complete and free of hidden assumptions about the infrared limit. For off-diagonal hard-state elements, the same diagram yields the coherent-state overlap, giving a first-principles account of soft-cloud decoherence. The soft-shell coarse graining is then constructed as a CPTP Schur channel whose infinitesimal limit produces the exact Lindblad generator with jump operators determined by the eikonal emission amplitudes. Finally, a local CPTP-certification pipeline is developed for non-Markovian process tensors, enabling constant-time verification of trace preservation in open quantum simulations. The framework bridges categorical quantum semantics, non-equilibrium field theory, and practical open-system compilation.

1 0

0

quant-ph 2026-06-30

Machine verifies exact QAOA ratio on ring problem

by Uri Kol, Maor Ben-Shahar +2 more

A Machine-Verified Proof of a Quantum-Optimization Conjecture

Depth-p QAOA attains approximation ratio (2p+1)/(2p+2) exactly, as shown by a Lean-certified proof.

abstract click to expand

We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-$p$ Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio $(2p+1)/(2p+2)$ exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.

0

cs.LO 2026-06-29

16th AiML conference proceedings published open access

by Marta Bílková, Malvin Gattinger +3 more

Proceedings of the Sixteenth International Conference on Advances in Modal Logic

The volume gathers invited abstracts and full papers from the 2026 Amsterdam meeting.

abstract click to expand

Advances in Modal Logic (AiML) was founded in 1995 as an initiative devoted to presenting an up-to-date picture of research in modal logic and its many applications. It combines a conference series with volumes arising from the conferences, and has become the flagship international forum for work on all aspects of modal logic. Over the past three decades, AiML has both recorded and helped shape developments across the field, bringing together semantic, proof-theoretic, algebraic, topological, computational, philosophical, and applied perspectives on modal and related logics. Exactly thirty years after the first AiML conference, AiML 2026, the sixteenth conference in the series, is organized by the Institute of Logic, Language and Computation (ILLC) of the University of Amsterdam. The conference takes place in Amsterdam, the Netherlands, from 29 June to 3 July 2026. This volume contains abstracts of invited talks and full papers accepted for the conference. Beginning with AiML 2026, the proceedings are published open access via Electronic Proceedings in Theoretical Computer Science (EPTCS).

0

cs.LO 2026-06-29

Syntactic separation blocks Skolem equivalence proofs

by Fabio F.G. Buono

Syntactic Separation Implies Computational Indistinguishability: An Abstract Obstruction Theorem

In local model-free systems, separated functions demand linear or exponential derivation steps and unify several proof barriers.

abstract click to expand

We prove that syntactic separation implies computational indistinguishability. A local syntactic system R acts on terms within radius r0 without consulting any model; when two Skolem functions are syntactically separated in R, no derivation can prove their equivalence (Case 1), and any sound local extension requires Omega(n) steps, improving to Omega(2^n) under clause-per-configuration encoding (Case 2). Both bounds are new: the derivation-length lower bound does not appear in prior work on Skolemization or saturation proving, and the cryptographic reading, syntactic separation as ciphertext indistinguishability, derivation cost as negligible advantage, is original. The same obstruction, as formal instances of Case 1 and Case 2, governs the Natural Proofs barrier of Razborov and Rudich, the Type Omitting Theorem, and the unconditional AC^0 barrier of Loff et al. (2026).

0

cs.LO 2026-06-29

LAMP agents prove 96.7% of CoW theorems in Lean

by Santhana Srinivasan R, Maithilee Patawar

LAMP: Lean-based Agentic framework with MCP and Proof Repair

Ontology delivered at inference time lets Planner-Builder-Verifier team succeed without fine-tuning

abstract click to expand

Large language models are increasingly capable of mathematical reasoning, but the proofs they generate are often unreliable and hard to verify. Interactive theorem provers such as Lean 4 address this by accepting only kernel-checked proofs; however, their reach is bounded by the formalized knowledge available. While Mathlib, a repository of formalized Lean 4 theorems that covers diverse mathematical areas, certain specialized areas remain underrepresented; notably, the domain of Combinatorics on Words (CoW). CoW studies sequences, exploring their properties such as periodicity, borders, conjugacy, and morphisms. As a result, specialized provers, trained on Mathlib-centered data, lack the lemmas to operate in CoW. We present two contributions. First, we introduce a Lean 4 formalization of CoW containing eight modules and \textbf{93} declarations of core definitions and foundational lemmas. Second, we present LAMP, a multi-agent framework that synthesizes kernel-verified Lean 4 proofs by providing explicit, structured domain knowledge at inference time through an ontology, rather than by fine-tuning a prover. LAMP coordinates a Planner, Builder, and Verifier with Model Context Protocol based access to a domain-specific CoW ontology. In a suite of 90 CoW theorems that span all eight modules and three difficulty levels, LAMP synthesizes verified proofs for 96.7% of theorems, substantially exceeding both an unscaffolded baseline and existing specialized provers. An ablation shows that removing LAMP's tool-grounded architecture or its Planner/Builder separation each cost roughly 12 percentage points, even with the backbone model held fixed.

0

cs.LO 2026-06-29

SAT-IT stages SAT solving from backtracking to full CDCL

by Wilber Bermeo, Jordi Coll +2 more

SAT-IT: an Online Interactive SAT Tracer

Users set literal breakpoints, run automatically, and step backward to test alternative decisions on any instance.

abstract click to expand

Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression: from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

0

cs.LO 2026-06-29

AGI alignment unverifiable in general due to undecidability

by Jose Pascual Gumbau Mezquita

The Undecidability of Artificial General Intelligence (AGI) Alignment

Two theorems reduce verification to known logical barriers, forcing tradeoffs in soundness, completeness or tractability.

abstract click to expand

This article establishes the foundational mathematical limits of Artificial General Intelligence (AGI) safety, proving that the core barrier is not the impossibility of an aligned state, but its structural unverifiability. We formalize this boundary through two central impossibility results: the Unverifiability Theorem of Alignment and the Theorem of Finite Structural Unverifiability of AGI Alignment. We ground this boundary at Trakhtenbrot's Wall, demonstrating that contemporary engineering defenses relying on finite hardware or halting architectures fail to escape logical obstructions. This failure manifests as an inescapable triad of containment failures: open domains yield fundamental undecidability (Rice and G\"odel); universal finite verification collapses into algorithmic incomputability (Trakhtenbrot); and particular bounded environments trap the supervisor within intractable bounds in the worst case. As a direct structural corollary of these results, we derive the Soundness--Completeness--Tractability Trilemma, establishing that the mutual incompatibility of these three properties is a necessary consequence of descriptive complexity rather than an empirical anomaly. Finally, we map these theoretical bounds onto practical AI engineering, demonstrating that modern containment strategies are not temporary patches, but mandatory sacrifices of logical expressivity required to secure decidable fragments of safety.

0

cs.LG 2026-06-29

Embeddings reveal axiom of choice through declining anomaly scores

by Rodrigo Mendoza-Smith

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

The geometric signal separates classical from constructive proofs at close dependency but fades beyond distance nine.

abstract click to expand

The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space that obeys a one-parameter mixture law and has operational consequences for neural theorem provers. To do this, we partition $471{,}260$ declarations of Mathlib by transitive dependence on the axiom of choice and represent a filtered population of $42{,}355$ traced theorems by their sequences of tactic invocations. We use the constructive proofs in this dataset to train a self-supervised proof encoder and show that when using it to measure classical proofs, three complementary measurements (anomaly score, reconstruction loss, and density-superlevel containment) exhibit a common decline with the proof's distance from the axiom in the dependency graph, from sharp separation at the shallow boundary (AUC $0.847$ at distance $2$) to indistinguishability at distance~$9{+}$. Robustness controls show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source. Operationally, we show that on an evaluation sample of $251$ Mathlib theorems, Lean's \texttt{aesop} tactic solves constructive theorems at $13\times$ the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to $5\times$. The geometric anomaly score predicts \texttt{aesop} failure beyond proof length, providing an operational link between the geometric signature and prover performance.

0

cs.LO 2026-06-29

KoAT infers runtime bounds for integer programs automatically

by Nils Lommen, Éléanore Meyer +1 more

KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Modular analysis of subprograms with multiple techniques yields termination proofs and complexity results for recursive code.

abstract click to expand

KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, KoAT uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

0

quant-ph 2026-06-29

Quantum instruments compose by integrating channel-valued functions

by Robert I. Booth, Dominik Leichtle +2 more

Composing Quantum Instruments

The Okamura-Ozawa extension supplies monad multiplication, identifying quantum Markov kernels as the Kleisli category.

abstract click to expand

We study the composition of classically-controlled quantum instruments--the natural quantum analogue of Markov kernels. Classically, Markov kernels compose by integrating one kernel against another. Defining this composition for quantum instruments with continuous outcomes requires an integral of quantum channel-valued functions with respect to a quantum instrument. We construct this integral in the Heisenberg picture using the Okamura-Ozawa normal extension to a von Neumann tensor product. This integral recovers the expected finite formula, preserves normal complete positivity and subunitality, and provides the multiplication for a monad governing the composition of quantum instruments. As an immediate consequence, we identify the category of quantum Markov kernels as the Kleisli category of this monad.

0

cs.LO 2026-06-29

Two limits restore decidability for opacity in timed automata

by Étienne André, Sarah Dépernet +1 more

Buffered control for opacity in timed automata

Buffered observations make control undecidable generally, but decidable with bounded strategy switches or full observability of actions, wit

abstract click to expand

Timed automata are an extension of finite automata that can measure and react to the passage of time, handling real-time constraints by using clocks. The timed opacity problem, where an attacker attempts to infer from observed actions and timestamps whether a secret location was visited, was shown undecidable for timed automata. Execution-time opacity is a decidable though limited setting in which the attacker attempts to detect whether the secret location was visited, by only relying on the run duration. Here, we significantly extend this setting, by allowing the attacker to observe all observable actions, in the right order though with only the integral parts of their timestamps, which we call buffered observations. We consider the controlled setting, in which we aim at dynamically defining a sequence of sets of enabled actions ensuring opacity with buffered observations. We first prove the inter-reducibility of full opacity (observations must not leak the visit of the secret location) and weak opacity (the attacker might prove that the location was not visited, but not that it was visited) in this new controlled setting. Then, we prove the undecidability of the problem of existence of a sequential control strategy ensuring opacity under buffered observations. Finally and most importantly, we prove that decidability is retrieved in two independent cases, with their tight theoretical complexities, with and without control. These two assumptions express realistic limitations of the controller. The first case is when the strategy of the controller changes at most an a priori fixed number of times per time unit, which is not a strong practical assumption. The second case is when all controllable actions are observable and distinguishable by an attacker.

0

cs.LO 2026-06-29

Four logics characterize when a relation simulates a program

by Suha Orhun Mutluergil, Alperen Dogan

Combining Axiomatic Models for Refinement Proofs

Refinement proofs reduce to checking Hoare or Incorrectness triples when using forward or backward simulations.

abstract click to expand

Refinement proofs verify an implementation by showing that its behaviours are subsumed by a simpler specification, on which safety properties are easier to establish. We study how such proofs interact with the axiomatic program logics used to verify the specification. We first give a uniform account of Hoare, Incorrectness, Lisbon, and Necessary-Preconditions logic, classified by the direction in which each constrains a transition and by whether it over- or under-approximates its target set. We then show that simulation relations transfer state-based safety properties: a forward simulation carries a Hoare (inductive) invariant of the specification to one of the implementations, and forward and backward simulations both carry ordinary invariants, via the pre-image of the relation. Finally, we characterize, within these logics, when a relation is a simulation, forward simulations by the validity of Hoare or Lisbon triples, backward simulations by Necessary-Preconditions or Incorrectness triples, so that the simulation obligation reduces to a triple in an off-the-shelf functional logic. We illustrate the development with a concurrent counter, transporting a safety bound from an atomic sequential specification to a Left--Right implementation through an intermediate nondeterministic-concurrent counter, with a forward simulation on one side and a backward simulation on the other.

0

cs.LO 2026-06-29

Round-based algorithms reduce to finite-counter LTL checking

by Nathalie Bertrand, Pranav Ghorpade +1 more

Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

Sound complete reduction lets existing model checkers verify any number of processes with unbounded rounds.

abstract click to expand

Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker.

0

cs.LO 2026-06-29

Quantum instrument monad generalizes state monad to quantum systems

by Tobias Fritz

The quantum instrument monad

It models computation-quantum interactions via a new integral on type I algebras and is shown to be a strong monad in both finitary and meas

abstract click to expand

Monads are a ubiquitous structure in functional programming used for modelling computational effects. For example, the state monad models the effect of a computation interacting with a memory system. Here we introduce the quantum instrument monad $\mathcal{I}_\mathcal{A}$, which models the effect of a computation interacting with a quantum system with algebra of observables $\mathcal{A}$. It can be thought of as a noncommutative generalization of the state monad. We construct this quantum instrument monad in two versions: a finitary version on the category of sets and a measure-theoretic version on the category of measurable spaces (the latter under the assumption that $\mathcal{A}$ is a type I von Neumann algebra with separable predual). Both versions are strong monads. The construction of the measure-theoretic version is based on a new notion of integral of a quantum-operation-valued function against a state-valued measure.

0

cs.LO 2026-06-26

Monotonic accumulators yield quantitative STL-GO semantics

by Sheryl Paul, Vidisha Kudalkar +4 more

An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators

Layered algebra separates temporal and graph aggregation so counting constraints receive sound numerical values

abstract click to expand

Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO's graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.

0

cs.LO 2026-06-26

Agreement with baseline certifies invalid actions 42% of time

by Sidnei Barbieri, Wellington Vargas +1 more

Auditing AI Investment Recommendations as Executable Actions

A protocol auditing AI investment advice for executability shows agreement metrics endorse unfeasible trades nearly half the time.

abstract click to expand

AI systems increasingly produce investment recommendations, yet the usual evaluations ask the wrong question. Realized return is noisy and easy to overfit, and agreement with a reference portfolio can reward advice that cannot be executed. We argue that an AI-generated recommendation should first be audited as an executable financial action, and only then judged on return. We make this concrete with a deterministic, replayable baseline and a protocol that scores any advisor on three properties a single number conflates: validity under portfolio and fee constraints, stability across repeated runs, and agreement with the baseline. These properties separate cleanly, and agreement is the most misleading in isolation: across a 120-scenario bank, the control that agrees most with the baseline (0.94) is admissible in only 0.58 of its runs, so agreement certifies an invalid action in 42% of them. On an adversarial set, two frontier models are admissible in barely half of their bare-prompt runs and fail on order arithmetic, not judgment; supplying the fee arithmetic deterministically lifts both to near-perfect validity. We make no alpha claim: the baseline is a transparent verifier whose guardrails follow from the fee schedule and whose decisions replay from frozen inputs, and every figure and table regenerates offline from the artifact.

0

cs.LO 2026-06-26

Markov chains equivalent to lower-dimensional linear systems

by Mihir Vahanwala

Equivalence of Continuous-Time Markov Chains and Linear Dynamical Systems

The known discrete-time link between d-state chains and (d-1)-dim systems carries over to continuous time.

abstract click to expand

The purpose of this short note is to record that an analogue of the following result, which is known for discrete-time linear dynamical systems, also holds in the continuous-time setting. The dynamics of a $d$-state Markov chain is governed by that of a linear dynamical system of dimension at most $d-1$; conversely, a linear dynamical system of dimension $d-1$ can be "embedded" into a Markov chain with $d$ states.

0

cs.LO 2026-06-26

Neuro-symbolic pipeline hits 0.98 logic accuracy in one call

by Carlos Ramírez Ovalle, Abel Alvarez

Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

VFR-LLM replaces five sampling calls with one verifiable formalization step on precedence and deduction tasks for small local models.

abstract click to expand

Small language models can run locally on consumer hardware, but structured reasoning often pushes users toward repeated sampling or larger models. This article studies a bounded neuro-symbolic alternative for local inference: a model translates a problem into typed finite-domain rules and constraints, a symbolic layer checks traceability and consistency, and a deterministic solver performs the reasoning step. The resulting Verifiable Formalization and Repair pipeline (VFR-LLM) tests when symbolic verification can replace repeated sampling without weakening accuracy. We evaluate it through LM Studio on Apple Silicon, using Qwen3-4B-2507 as the primary model, with Phi-4-mini-reasoning and Gemma-3n-E4B as robustness checks. On 120 generated pure-precedence problems, Qwen VFR-LLM achieves 0.983 accuracy, versus 0.700 for serial self-consistency using one model call instead of five. On a 120-instance BBH-derived extended logical-deduction subset, it reaches 0.933 versus 0.283. The advantage persists against a stronger cost-aware adaptive self-consistency baseline, which lowers sampling cost but not the single-call accuracy gap. Gemma reproduces the same model-dependent boundaries and Phi is negative on typed constraints. The contribution is bounded: finite-domain logic can replace repeated local sampling for some structured tasks, saving model calls and serial latency, with stratum-dependent token savings.

0

cs.LO 2026-06-26

On the Continuity of the Probabilistic Bisimilarity Distance

by Syyeda Zainab Fatmi, Stefan Kiefer +2 more

States keep small distance under any small probability change exactly when they are robustly bisimilar, with a fast algorithm to check it.

abstract click to expand

The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we (CAV 2025) introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.

0

cs.LO 2026-06-26

Fixed phases make tree safety checking EXPSPACE-complete

by Romain Delpy, Anca Muscholl +1 more

On Parameterized Verification Over Tree Topologies

Alternation bounds between upward and downward synchronizations decide safety on arbitrary-depth trees.

abstract click to expand

Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).

0

cs.LO 2026-06-26

Forward-only construction yields semilinear invariants for VAS

by Clotilde Bizière, Jérôme Leroux +1 more

A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Builds from source alone without backward steps to create structure-aligned invariants, including periodic ones for periodic systems.

abstract click to expand

The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An alternative, conceptually simpler approach introduced by Leroux shows that non-reachability is always witnessed by semilinear inductive invariants, yielding a decision procedure by combining an enumeration of runs with a search for such invariants. However, the construction of these invariants relies on a back-and-forth scheme that depends symmetrically on the source and the target. As a result, the invariants are not guaranteed to reflect the structural properties of the VAS, and the construction is difficult to extend to asymmetric models such as Branching VAS. We introduce a new forward-only construction of semilinear inductive invariants for VAS. Our method builds invariants from the source configuration alone and avoids the need for backward reasoning. This yields invariants that are more canonical and better aligned with the structure of the system. In particular, our method produces periodic inductive invariants for periodic VAS. Beyond its intrinsic interest, our approach provides a step toward extending invariant-based techniques to Branching VAS.

0

cs.LO 2026-06-26

PaJAM steps extracted from intersection type derivations

by Stefano Catozi, Ugo Dal Lago +1 more

On Jumps, Interactions, and Intersection Types

For any finite backtracking depth the machine is polynomial in weak head beta steps

abstract click to expand

The Jumping Abstract Machine (JAM), an evaluation mechanism for the $\lambda$-calculus, was introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM), itself an operational counterpart to Girard's Geometry of Interaction and Abramsky $\textit{et al}$. game semantics. Moreover, the JAM is isomorphic to the Pointer Abstract Machine (PAM), the syntactical counterpart of Hyland and Ong's game semantics. We study a generalization of the JAM, that we call the Parametric Jumping Abstract Machine (PaJAM) and show that there is a tight correspondence between the PaJAM and non-idempotent intersection types: given a normalizing term $t$, the number of steps taken by the PaJAM when evaluating $t$ can be extracted from its non-idempotent intersection type derivation. Remarkably, fixing the backtracking depth of the PaJAM, one can easily recover both the JAM/PAM, when the depth is constrained to be zero, and the IAM, when it is instead unconstrained. Exploiting type-theoretic machinery, we analyze the complexity of the PaJAM, showing that it is $\textit{polynomial}$ in the number of weak head $\beta$ steps, giving rise to a $\textit{reasonable}$ cost model, for each $\textit{finite}$ bound on the backtracking depth.

0