https://arxiv.org/api/HVB9mbfYUtFxsjUHIx4as8ilWCA 2026-07-21T22:12:22Z 19781 135 15 http://arxiv.org/abs/2112.06339v3 2026-07-08T10:00:36Z

We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted in using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. The notion of equality has to be interpreted in the Boolean algebra and when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.

2021-12-12T22:26:22Z 41 pages, no figures, journal version for GandALF'25 Robert Furber Radu Mardare Prakash Panangaden Dana Scott http://arxiv.org/abs/2607.07164v1 2026-07-08T08:56:24Z

Logic Equivalence Checking (LEC), a fundamental hardware verification task, is often bottlenecked by synthesis-induced structural perturbations and XOR-dense regions that degrade SAT solver performance. We contend that the modeling of the miter is as critical as the SAT solver itself. To this end, we introduce a miter-aware mapping framework that strategically formulates the problem before solving. By constructing a LUT-based miter -- instead of a traditional, flat netlist -- our approach preserves critical structural correspondence between the two designs while making high-level logic relations explicit. Our framework uniquely integrates three techniques: equivalence-preserving mapping to structurally align the two circuits, Gaussian-guided XOR modeling to algebraically simplify dense arithmetic, and solver-oriented LUT selection to generate a representation optimized for efficient SAT reasoning. Evaluated on comprehensive datasets, our method achieves up to a \textbf{92.1\%} reduction across state-of-the-art SAT solvers. This demonstrates that a solver-aware modeling paradigm, which unifies structural mapping with SAT reasoning, can fundamentally enhance LEC efficiency.

2026-07-08T08:56:24Z 7 pages, 4 figures Jiaying Zhu Zhengyuan Shi Mengxia Tao Kezhi Li Min Li Qiang Xu http://arxiv.org/abs/2607.07126v1 2026-07-08T08:14:15Z

High-Level Synthesis leverages loop unrolling and array partitioning, but scheduling concurrent accesses is challenging when indices contain non-affine arithmetic. Conventional polyhedral frameworks systematically over-approximate these non-linear transformations, forcing conservative serialization that degrades performance. To minimize this bottleneck, we present a spatial verification framework operating at the LLVM Intermediate Representation (IR) level. By extracting flat arithmetic expressions from "getelementptr" instructions, it models memory banks as polymorphic spatial predicates to handle non-affine terms. Structural safety is enforced via a Conflict-Free Unrolling condition using Separation Logic's separating conjunction; concurrent operations targeting the same bank trigger an automatic spatial contradiction. This disjointness requirement is reduced to a matrix of pairwise inequalities over immutable Static Single Assignment (SSA) variables for a Satisfiability Modulo Theories (SMT) oracle. To guarantee safety against undecidable non-linear arithmetic, we implement a deterministic sequential fallback. Finally, a theorem of soundness bridges algebraic SMT verification with Register Transfer Level trace safety, ensuring physical hardware immune to structural memory collisions.

2026-07-08T08:14:15Z 14 pages, 4 figures Yeonseok Lee http://arxiv.org/abs/2607.05701v2 2026-07-08T03:30:15Z

We study sets and functions definable in the three additive theories $\FO(\Z,+,\leq)$, $\FO(\R,+,\leq)$, and $\FO(\R,\Z,+,\leq)$. The Ginsburg--Spanier theorem~\cite{GS66} characterizes $\FO(\Z,+,\leq)$-definable sets as exactly the semi-linear sets. We extend this characterization in two directions. First, we show that $\FO(\Z,+,\leq)$-definable \emph{functions} are exactly the piecewise linear functions (Theorem~\ref{thm:integer}), and that $\FO(\R,+,\leq)$-definable functions are also exactly the piecewise linear functions (Theorem~\ref{thm:real}). The proofs are direct algebraic arguments using only a stability lemma and the Ginsburg--Spanier theorem. Second, we introduce \emph{semi-polinear sets} as the $\FO(\R,\Z,+,\leq)$ analogue of semi-linear sets, and prove that the class of mixed-linear sets and the class of semi-polinear sets coincide (Theorem~\ref{thm:mixed-sets}). We further show that $\FO(\R,\Z,+,\leq)$-definable functions are exactly the \emph{piecewise-simple} functions (Theorem~\ref{thm:mixed-functions}), a new class of functions that are linear in the integer part and in the fractional part of the argument, but with potentially different linear coefficients for each. These algebraic characterizations unify the three theories in a single framework, and the proofs are purely algebraic, without reference to automata or machines.

2026-07-06T23:47:19Z 12 pages, 1 table LMCS format Alain Finkel Jérôme Leroux http://arxiv.org/abs/2607.00795v2 2026-07-07T23:15:11Z

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 the present authors 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.

2026-07-01T11:24:56Z Submitted to Communications in Mathematical Physics Nadish de Silva Santanil Jana Ming Yin http://arxiv.org/abs/2405.14678v2 2026-07-07T17:26:55Z

In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples.

2024-05-23T15:13:33Z 98 pages, to appear in the proceedings of CATMI 2023 (Category Theory at Work in Computational Mathematics and Theoretical Informatics) Lukas Mulder Paige Randall North Maximilien Péroux http://arxiv.org/abs/2607.06446v1 2026-07-07T16:11:23Z

We study solution discovery in the token-sliding model from a logical and cost-value optimization perspective. In solution discovery, we are given a graph, an initial placement of $k$ tokens, and a movement budget $b$. The task is to find a reachable target configuration satisfying a prescribed condition. Our results are inspired by \textsc{Partial Vertex Cover Discovery}, where the condition is that the~$k$ tokens cover at least $t$ edges of the input graph. This objective is not merely a sum of independent occupied vertex contributions: each selected vertex contributes its degree, but edges with both endpoints selected have to be subtracted once. To capture this phenomenon, we introduce \textsc{FO Value Discovery}, an optimization problem in which the value of a selected tuple is given by unary vertex weights together with first-order definable correction terms. We further generalize the setting to \textsc{FO Cost-Value Decision}, where vertices carry both costs and values, and the task is to decide whether there is a tuple whose first-order value expression reaches a prescribed value threshold while respecting a cost bound. Finally, we study the parameterized complexity of \textsc{Partial Vertex Cover Discovery} and \textsc{Vertex Cover Discovery}. As a consequence of the logical meta-theorems, we obtain fixed-parameter tractability of \textsc{Partial Vertex Cover Discovery} on several graph classes, including classes of locally bounded cliquewidth. We also show that \textsc{Partial Vertex Cover Discovery} is W[1]-hard parameterized by $k+b$ and fixed-parameter tractable on $d$-degenerate graphs parameterized by $k+d$. For \textsc{Vertex Cover Discovery}, we prove NP-hardness on planar graphs, W[1]-hardness parameterized by the clique cover number, even when a clique cover is supplied with the input, and W[1]-hardness with respect to parameter cutwidth.

2026-07-07T16:11:23Z Enna Gerhard Stephanie Maaz Pascale Schott Sebastian Siebertz Jan Wodkte http://arxiv.org/abs/2607.06379v1 2026-07-07T15:18:50Z

Mathematicians have embraced interactive theorem provers with growing enthusiasm -- building large shared libraries and machine-checking a string of landmark results. Theoretical physics is different: most of its results are not theorems but justified by arguments the community trusts without a rigorous proof. For many -- the one we treat here among them -- no rigorous proof is within reach. For 4d Yang--Mills theory, deriving exact rigorous results from first principles would first require constructing the interacting theory nonperturbatively, which is a sizable piece of one of the Clay Millennium prize problems. We argue here that an interactive theorem prover can be used to verify some non-rigorous physics arguments. The method is to postulate a short list of explicit, named physical postulates, which imply the physical results by virtue of a machine-checkable proof. The trust that remains then rests on that short, inspectable list, and the prover can report, for any downstream result, exactly which assumptions it used. We carry this out for the Seiberg--Witten solution of ${N}=2$ $SU(2)$ super-Yang--Mills -- the genus-one case -- formalized in Lean 4; the higher-genus $SU(N)$ generalization is developed in the same repository as an axiomatized skeleton and left to future work. We describe what is proved, what is assumed, how the assumptions are checked -- external review and an independent numerical oracle -- and why this discipline is a sound standard for validating AI-generated results in theoretical physics. What we offer is a discipline, reviewable on its own terms: a reader may take the Seiberg--Witten mathematics on trust and still assess the formalization method.

2026-07-07T15:18:50Z 18 pages; companion github repo mrdouglasny/seiberg-witten Michael R. Douglas http://arxiv.org/abs/2603.20893v2 2026-07-07T14:57:58Z

Formal mathematics is mathematics done within the framework of a formal logic. It offers major benefits to mathematicians as well as to computing professionals, engineers, and scientists who use mathematics in their work. The standard approach to formal mathematics, in which mathematics is done with the help of a proof assistant and all details are formally proved and mechanically checked, achieves these benefits and offers a very high level of assurance that the results produced are correct. However, since the main goal of the standard approach is certification, the proof assistants supporting the standard approach are generally complex, based on unfamiliar logics, difficult to learn how to use, and far removed from mathematical practice. Thus the standard approach does not adequately serve mathematics practitioners who are more interested in communicating mathematical ideas than in formally certifying their correctness or who prefer not to make the investment needed to gain proficiency in the use of a proof assistant. This paper presents an alternative to the standard approach that focuses on communication and accessibility, the two weaknesses of the standard approach. It is called the free approach to formal mathematics since it is free of the obligation to formally prove and mechanically check all details of a mathematical development. The paper argues that the free approach would serve the needs of the average mathematics practitioner much better than the standard approach. It describes an implementation of the free approach based on a logic named Alonzo, a practice-oriented version of Alonzo Church's formulation of simple type theory. And it calls for the mathematics community to develop logics, software, and libraries of formal mathematical knowledge to support the free approach and to train mathematics practitioners to use them.

2026-03-21T17:47:06Z 20 pages William M. Farmer http://arxiv.org/abs/2607.03777v2 2026-07-07T08:26:27Z

The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear integer and real arithmetic. In this paper we revisit the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat. By closely formalizing the implementation of MCSat within the Yices2 SMT solver, we incorporate design decisions that diverge from those in the seminal MCSat paper and thereby capture the current state-of-the-art in MCSat-based SMT reasoning. We present a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions. We provide several detailed examples to illustrate the applicability of the presented calculus.

2026-07-04T08:59:01Z to be published in the proceedings of the 24th International Workshop on Satisfiability Modulo Theories Thomas Hader Theo Jauschneg Daniela Kaufmann Laura Kovacs http://arxiv.org/abs/2607.05987v1 2026-07-07T08:18:43Z

We formalize in Lean 4 a complete combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and to the existence of mixed Nash equilibria in finite games. The development follows Ivanov's indexed-order formulation of Scarf's theorem, formalizes the room--door incidence structure and parity argument, instantiates the theorem on finite grids of the standard simplex, and carries out the compactness and continuity argument needed to obtain a fixed point. We then extend the result to finite products of simplices by an explicit embedding--projection construction and use this product theorem to prove mixed Nash equilibrium existence via the Nash map. As a secondary by-product, we derive BrouwerBench, a preliminary 80-item Lean-grounded benchmark for probing proof-structure understanding within this single formal development.

2026-07-07T08:18:43Z 18 pages, 11 tables. Accepted at the 3rd AI for Math Workshop: Toward Self-Evolving Scientific Agents Yuwei Lyu Kai Li http://arxiv.org/abs/2607.05907v1 2026-07-07T07:02:13Z

Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and $ω$-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and Python interface also make it an attractive platform for \emph{teaching} the connections between temporal logic formulas and the $ω$-automata that give them their semantics.

2026-07-07T07:02:13Z Demonstration for TEAL'26 Alexandre Duret-Lutz http://arxiv.org/abs/2508.11449v3 2026-07-06T19:04:03Z

We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.

2025-08-15T12:56:54Z The article will appear in Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter, editors. Theory and Applications of Craig Interpolation. Ubiquity Press, 2026 Patrick Koopmann Christoph Wernhard Frank Wolter http://arxiv.org/abs/2507.01577v3 2026-07-06T18:24:33Z

We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where first an essentially propositional ground interpolant is calculated that is then lifted to a quantified first-order formula. We discuss two possibilities to obtain a ground interpolant from a proof: with clausal tableaux, and with resolution. Established preprocessing techniques for first-order proving can also be applied for Craig interpolation if they are restricted in specific ways. Equality encodings from automated reasoning justify strengthened variations of Craig interpolation. Contributions to Craig interpolation that emerged from automated reasoning include variations for logics used in databases and logic programming. As an approach to uniform interpolation we introduce second-order quantifier elimination with examples and describe the basic algorithms DLS and SCAN.

2025-07-02T10:52:24Z This is a chapter of the forthcoming book "Theory and Applications of Craig Interpolation", edited by Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter Christoph Wernhard http://arxiv.org/abs/2607.05336v1 2026-07-06T17:16:53Z

We solve a long standing open problem, showing that the query answering for conjunctive queries with safe negation, over DL-Lite$_{core}$ knowledge bases, is undecidable.

2026-07-06T17:16:53Z Jerzy Marcinkowski Piotr Ostropolski-Nalewaja