https://arxiv.org/api/cVk/HWVc9I90a/U9DfoZnlqAAZ4 2026-03-24T09:45:30Z 18920 75 15 http://arxiv.org/abs/2603.15675v1 2026-03-13T18:11:39Z

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.

2026-03-13T18:11:39Z Debjyoti Bera Tim A. C. Willemse http://arxiv.org/abs/2603.13181v1 2026-03-13T17:14:38Z

Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed, but in practice policies are developed iteratively, composed from independently maintained components, and extended as organisational structures evolve. We introduce robust property verification: the problem of determining what a policy's structure commits it to regardless of how pending decisions are resolved and regardless of subsequent extension. We define a support judgment $\Vdash_{P}φ$ stating that policy $P$ has robust property $φ$, with connectives for implication, conjunction, disjunction, and negation, prove that it is compositional (verified properties persist under policy extension by a monotonicity theorem), and show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language. Soundness and completeness of this reduction are established, yielding a finitary and executable verification procedure for robust security properties.

2026-03-13T17:14:38Z Alexander V. Gheorghiu http://arxiv.org/abs/2603.13454v1 2026-03-13T16:29:21Z

Quantum control is an important logical primitive of quantum computing programs, and an important concept for equational reasoning in quantum graphical calculi. We show that controlled diagrams in the ZXW-calculus admit rich algebraic structure. The perspective of the higher-order map Ctrl recovers the standard notion of quantum controlled gates, while respecting sequential and parallel composition and multiple-control. In this work, we prove that controlled square matrices form a ring and therefore satisfy powerful rewrite rules. We also show that controlled states form a ring isomorphic to multilinear polynomials. Putting these together, we have completeness for polynomials over same-size square matrices. These properties supply new rewrite rules that make factorisation of arbitrary qubit Hamiltonians achievable inside a single graphical calculus.

2026-03-13T16:29:21Z Edwin Agnew Lia Yeh Richie Yeung http://arxiv.org/abs/2603.13058v1 2026-03-13T15:07:21Z

We present an algorithm that, given an index $t$, produces the $t$-th (lexicographically ordered) answer of an MSO query over a string. The algorithm requires linear-time preprocessing, and builds a data structure that answers each of these calls in logarithmic time. We then show how to extend this algorithm for a string that is compressed by a straight-line program (SLP), also with linear-time preprocessing in the (compressed encoding of the) string, and maintaining direct access in logtime of the original string. Lastly, we extend the algorithm by allowing complex edits on the SLP after the direct-access data structure has been processsed, which are translated into the data structure in logtime. We do this by adapting a document editing framework introduced by Schmid and Schweikardt (PODS 2022). This work improves on a recent result of dynamic direct access of MSO queries over strings (Bourhis et. al., ICDT 2025) by a log-factor on the access procedure, and by extending the results to SLPs.

2026-03-13T15:07:21Z Martín Muñoz http://arxiv.org/abs/2603.13018v1 2026-03-13T14:24:04Z

Sandqvist's base-extension semantics for intuitionistic propositional logic defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global question: which formulae are valid? This paper addresses the local question: given a fixed base, what does support in that base correspond to? We show that support in a fixed base coincides with proof-search in a second-order hereditary Harrop logic program, via an encoding of formulae as logic-programming goals. This encoding proceeds by reading the semantic clauses in continuation-passing style, revealing that the universal quantifiers over base extensions and atoms appearing in those clauses are not domain-ranging quantifiers over a completed totality, but eigenvariables governed by a standard freshness discipline. Base-extension semantics thereby admits a fully constructive and computationally transparent interpretation: support is proof-search. The result complements Sandqvist's global theorem with a local correspondence, vindicates the anti-realist foundations of the framework on its own terms, and opens the way for implementing the semantics in modelling tasks.

2026-03-13T14:24:04Z Alexander V. Gheorghiu http://arxiv.org/abs/2603.12197v2 2026-03-13T13:57:17Z

We introduce an algebraic structure for studying state-independent contextuality arguments, a key form of quantum non-classicality exemplified by the well-known Peres-Mermin magic square, and used as a source of quantum advantage. We introduce \emph{commutation groups} presented by generators and relations, and analyse them in terms of a string rewriting system. There is also a linear algebraic construction, a directed version of the Heisenberg group. We introduce \emph{contextual words} as a general form of contextuality witness. We characterise when contextual words can arise in commutation groups, and explicitly construct non-contextual value assignments in other cases. We give unitary representations of commutation groups as subgroups of generalized Pauli $n$-groups.

2026-03-12T17:26:19Z Updated version of paper published in Proceedings of FSCD 2024 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), pp. 28-1 Samson Abramsky Serban-Ion Cercelescu Carmen-Maria Constantin http://arxiv.org/abs/2603.20264v1 2026-03-13T13:35:10Z

How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, distributed protocol synthesis, and recursive function synthesis. For each domain, we choose a state-of-the-art symbolic tool and compare it to an open-source, 32 billion parameter version of the Qwen LLM and the proprietary, frontier LLM GPT-5. We couple Qwen with a symbolic verifier and run it repeatedly until it either produces a solution that passes the verifier, or until there is a timeout, for each benchmark. We run GPT-5 once per benchmark and verify the generated output. In all domains, the symbolic tools solve more benchmarks than Qwen and either outperform or are about on par with GPT-5. In terms of execution time, the symbolic tools outperform GPT-5 in all domains, and either outperform or are very close to Qwen, despite the fact that the LLMs are run on significantly more powerful hardware.

2026-03-13T13:35:10Z Derek Egolf Yuhao Zhou Stavros Tripakis http://arxiv.org/abs/2512.21137v2 2026-03-13T13:23:13Z

We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.

2025-12-24T12:07:25Z Murdoch J. Gabbay http://arxiv.org/abs/2504.15844v3 2026-03-13T13:02:16Z

Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data structures. We present time-indexed heap invariants, a novel invariant-based heap encoding leveraging uninterpreted predicates and prophecy variables to reduce verification of heap-manipulating programs to verification of programs over integers only. Our encoding of heap is general and agnostic to specific data structures. To the best of our knowledge, our approach is the first heap invariant-based method that achieves both soundness and completeness. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation, we demonstrate that time-indexed heap invariants significantly extend the capability of existing verification tools, allowing automatic verification of programs with heap that were previously out of reach for state-of-the-art tools.

2025-04-22T12:40:21Z 39 pages, 6 figures. To appear in Proceedings of the ACM on Programming Languages (PACMPL), Volume 10, Issue OOPSLA1, 2026. This version includes a 10-page appendix containing detailed proofs and extended experimental evaluation results Zafer Esen Philipp Rümmer Tjark Weber 10.1145/3798228 http://arxiv.org/abs/2603.12953v1 2026-03-13T12:54:35Z

Neuro-symbolic reasoning increasingly demands frameworks that unite the formal rigor of logic with the interpretability of large language models (LLMs). We introduce an end to end explainability by construction pipeline integrating the Automated Theorem Generator Delta1 based on the full triangular standard contradiction (FTSC) with LLMs. Delta1 deterministically constructs minimal unsatisfiable clause sets and complete theorems in polynomial time, ensuring both soundness and minimality by construction. The LLM layer verbalizes each theorem and proof trace into coherent natural language explanations and actionable insights. Empirical studies across health care, compliance, and regulatory domains show that Delta1 and LLM enables interpretable, auditable, and domain aligned reasoning. This work advances the convergence of logic, language, and learning, positioning constructive theorem generation as a principled foundation for neuro-symbolic explainable AI.

2026-03-13T12:54:35Z 12 pages, 1 figure, 3 tables, accepted oral presentation at AAAI2026 Bridge Program on Logic & AI Yang Xu Jun Liu Shuwei Chen Chris Nugent Hailing Guo http://arxiv.org/abs/2603.12926v1 2026-03-13T12:09:22Z

The ODRL language has become the standard for representing policies and regulations for digital rights. However its complexity is a barrier to its usage, which has caused many related theoretical and practical works to focus on different, and not interoperable, fragments of ODRL. Moreover, semantically equivalent policies can be expressed in numerous different ways, which makes comparing them and processing them harder. Building on top of a recently defined semantics, we tackle these problems by proposing an approach that involves a parametrised normalisation of ODRL policies into its minimal components which reformulates policies with permissions and prohibitions into policies with permissions exclusively, and simplifies complex logic constraints into simple ones. We provide algorithms to compute a normal form for ODRL policies and simplifying numerical and symbolic constraints. We prove that these algorithms preserve the semantics of policies, and analyse the size complexity of the result, which is exponential on the number of attributes and linear on the number of unique values for these attributes. We show how this makes complex policies representable in more basic fragments of ODRL, and how it reduces the problem of policy comparison to the simpler problem of checking if two rules are identical.

2026-03-13T12:09:22Z Accepted at the 23rd European Semantic Web Conference (ESWC), ESWC 2026 Jaime Osvaldo Salas Paolo Pareti George Konstantinidis http://arxiv.org/abs/2311.15675v9 2026-03-13T10:57:51Z

We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is $Σ_1^2$-complete, and finite-state satisfiability and model-checking are equivalent to truth in second-order arithmetic. Finally, we also introduce closed-world semantics for second-order HyperLTL, where set quantification ranges only over subsets of the model, while set quantification in standard semantics ranges over arbitrary sets of traces. Here, satisfiability for the least fixed point fragment becomes $Σ_1^1$-complete, but all other results are unaffected.

2023-11-27T10:03:40Z Logical Methods in Computer Science, Volume 22, Issue 1 (March 16, 2026) lmcs:16039 Hadar Frenkel Gaëtan Regaud Martin Zimmermann 10.46298/lmcs-22(1:26)2026 http://arxiv.org/abs/2602.23389v2 2026-03-13T09:45:01Z

Inductive invariants are crucial in model checking, yet generating effective inductive invariants automatically and efficiently remains challenging. A common approach is to iteratively analyze counterexamples to induction (CTIs) and derive invariants that rule them out, as in IC3. However, IC3's clause-based learning is limited to a CNF representation. For some designs, the resulting invariants may require a large number of clauses, which hurts scalability. We present CIll, a CTI-guided framework that leverages LLMs to synthesize invariants for model checking. CIll alternates between (bounded) correctness checking and inductiveness checking for the generated invariants. In correctness checking, CIll uses BMC to validate whether the generated invariants hold on reachable states within a given bound. In inductiveness checking, CIll checks whether the generated invariants, together with the target property, become inductive under the accumulated strengthening. When inductiveness fails, CIll extracts CTIs and provides them to the LLM. The LLM inspects the design and the CTI to propose new invariants that invalidate the CTIs. The proposed invariants are then re-validated through correctness and inductiveness checks, and the loop continues until the original property strengthened by the generated invariants becomes inductive. CIll also employs IC3 to work with the LLM for automatically discovering invariants, and uses K-Induction as a complementary engine. To improve performance, CIll applies local proof and reuses invariants learned by IC3, reducing redundant search and accelerating convergence. In our evaluation, CIll proved full compliance within RISCV-Formal framework and full accuracy of all non-M instructions in NERV and PicoRV32, whereas M extensions are proved against the RVFI ALTOPS substitute semantics provided by RISCV-Formal.

2026-02-21T00:19:48Z Yuheng Su Tianjun Bu Qiusong Yang Yiwei Ci Enyuan Tian http://arxiv.org/abs/2603.12827v1 2026-03-13T09:31:24Z

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry this embedding in the Lisa proof assistant. On top of this foundation, we implement a proof-producing bidirectional type-checking tactic to compute proofs for typing judgements, with partial support for subtyping. We present examples showing how our approach enables automated reasoning for dependent types that is fully verified from set-theoretic axioms and deduction rules for schematic first-order logic with equality. Because types are merely sets, the resulting formalism supports equality that applies to all types and values and permits the usual substitution rules.

2026-03-13T09:31:24Z 7 pages. Mechanized proofs and source code available at Zenodo: https://doi.org/10.5281/zenodo.18997443 Yunsong Yang Simon Guilloud Viktor Kunčak http://arxiv.org/abs/2602.12891v2 2026-03-13T08:52:55Z

This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer Science). The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn't present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS (optimization theory, matroid theory, and the theory of grammars). In the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. In search for beauty, we focus on the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, most importantly, beauty is the means for shaping our place in the world and a source of redemption, where it can be viewed as a substitute for religion.

2026-02-13T12:56:08Z Please report any errors to martin.dvorak@matfyz.cz as I intend to upload corrected versions here ISTA Ph.D. Thesis (2026); ISSN: 2663-337X; ISBN: 978-3-99078-074-9 Martin Dvorak