arXiv cs.LO bot

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Commutation Groups and State-Independent Contextuality
Samson Abramsky, Serban-Ion Cercelescu, Carmen-Maria Constantin
https://arxiv.org/abs/2603.12197 @arXiv_quantph_bot@mastoxiv.page

toXiv_bot_toot

Incremental Neural Network Verification via Learned Conflicts

Raya Elsaleh, Liam Davis, Haoze Wu, Guy Katz
https://arxiv.org/abs/2603.12232 https://arxiv.org/pdf/2603.12232 https://arxiv.org/html/2603.12232

arXiv:2603.12232v1 Announce Type: new
Abstract: Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to $1.9\times$ over a non-incremental baseline.

toXiv_bot_toot

Coalgebraic Path Constraints

Todd Schmid
https://arxiv.org/abs/2603.12204 https://arxiv.org/pdf/2603.12204 https://arxiv.org/html/2603.12204

arXiv:2603.12204v1 Announce Type: new
Abstract: Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques come from coalgebraic modal logic, pattern avoidance specifications, and hidden algebra. We introduce equational path constraints, a well-behaved and relatively easy to describe class of finitary behavioural properties that provide an algebra-flavoured alternative to coequations. The basic idea is to assign a pair of values to each path through a coalgebra and posit that the two values coincide. We show that equational path constraints define covarieties and construct final coalgebras relative to equational path constraints in some concrete cases. We connect equational path constraints to coequations when values computed from paths live in a monad, and we compute an upper bound on the number of colours needed to express the coequation. One of our constructions is reminiscent of the initial/terminal sequences of (Ad\'amek, 1974) and (Barr, 1993). Motivating examples include commutativity conditions in automata theory, differential equations, bi-infinite streams, and frame conditions.

toXiv_bot_toot

When do modal definability and preservation theorems transfer to the finite?

Johan van Benthem, Balder ten Cate, Xi Yang
https://arxiv.org/abs/2603.12171 https://arxiv.org/pdf/2603.12171 https://arxiv.org/html/2603.12171

arXiv:2603.12171v1 Announce Type: new
Abstract: We study which classic modal definability and preservation results survive when attention is restricted to finite structures, where many first-order transfer theorems are known to break down. Several semantic characterizations for modal formula classes survive the passage to the finite, while a number of first-order preservation theorems for basic frame operations fail. Our main positive result is that the Bisimulation Safety Theorem does transfer to finite structures. We also discuss computability aspects, and analogues in the finite for the Goldblatt-Thomason theorem and for modal correspondence theory.

toXiv_bot_toot

Witnesses for Fixpoint Games on Lattices

Barbara K\"onig, Karla Messing
https://arxiv.org/abs/2603.11908 https://arxiv.org/pdf/2603.11908 https://arxiv.org/html/2603.11908

arXiv:2603.11908v1 Announce Type: new
Abstract: We construct witnesses that can be used to derive strategies in fixpoint games and provide proof that the least fixpoint of a function is either above or not below some given bound. We rely on a lattice-theoretical approach, including a Galois connection that connects a lattice representing the "logic universe", where the witness lives, with another lattice representing the "behaviour universe", over which the function is defined. In fact we consider two types of games -- primal and dual games -- and in both cases show how to derive winning strategies in the game from witnesses and construct witnesses from strategies. The two games differ wrt. their rules and the choice of basis of the lattice.
The theory can be instantiated to well-known examples: in particular we compare with the construction of distinguishing formulas in standard bisimilarity and behavioural metrics for probabilistic systems. As a new case study we consider witnesses for certifying lower bounds for the termination probability for Markov chains.

toXiv_bot_toot

Probabilistic Disjunctive Normal Forms in Temporal Logic and Automata Theory

Alexander Kuznetsov
https://arxiv.org/abs/2603.11083 https://arxiv.org/pdf/2603.11083 https://arxiv.org/html/2603.11083

arXiv:2603.11083v1 Announce Type: new
Abstract: This article introduces probabilistic disjunctive normal forms (PDNFs) as a framework for representing and reasoning about uncertainty in logical systems. Unlike classical DNFs, PDNFs assign real-valued weights to variables, encoding probabilistic information about their presence, absence, or negation. Then we construct a vector space of PDNFs that allows algebraic evidence combination. PDNFs are interpreted as probability distributions over venjunctions (temporal logic constructs) and as integrable functions over partitioned intervals, where the integrals determine variable probabilities. This dual perspective allows for a Banach space structure and the application of functional analysis. We demonstrate that, under exponential parametrisation, PDNF addition aligns with Bayesian evidence fusion and derive bounds for outcome identification from random samples. The formalism thus bridges logic, numerical methods, and continuous probability.

toXiv_bot_toot

[2026-03-13 Fri (UTC), 5 new articles found for cs.LO Logic in Computer Science]

toXiv_bot_toot

Replaced article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Towards a Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Stefan Milius, Lutz Schr\"oder, Stelios Tsampas, Henning Urbat
https://arxiv.org/abs/2210.13387

- A Graded Modal Type Theory for Pulse Schedules
Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, Jeremy Pope
https://arxiv.org/abs/2510.03130 @arXiv_csLO_bot@mastoxiv.page

- The Skolem Problem in rings of positive characteristic
Ruiwen Dong, Doron Shafrir
https://arxiv.org/abs/2510.27603 @arXiv_csLO_bot@mastoxiv.page

- Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in No...
Leiva, Ngu, Kricheli, Taparia, Senanayake, Shakarian, Bastian, Corcoran, Simari
https://arxiv.org/abs/2505.19361 @arXiv_csAI_bot@mastoxiv.page

- Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
Arun Govindankutty, Sudarshan K. Srinivasan
https://arxiv.org/abs/2603.08762 @arXiv_quantph_bot@mastoxiv.page

toXiv_bot_toot

A Formalization of Abstract Rewriting in Agda

Sam Arkle, Andrew Polonsky
https://arxiv.org/abs/2603.10936 https://arxiv.org/pdf/2603.10936 https://arxiv.org/html/2603.10936

arXiv:2603.10936v1 Announce Type: new
Abstract: We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus.

toXiv_bot_toot

WME: Extending CDCL-based Model Enumeration with Weights

Giuseppe Spallitta, Moshe Y. Vardi
https://arxiv.org/abs/2603.10236 https://arxiv.org/pdf/2603.10236 https://arxiv.org/html/2603.10236

arXiv:2603.10236v1 Announce Type: new
Abstract: In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking and keeps the clause database compact, thereby reducing memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best. This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations.

toXiv_bot_toot

[2026-03-12 Thu (UTC), 2 new articles found for cs.LO Logic in Computer Science]

toXiv_bot_toot

Replaced article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- LLM2SMT: Building an SMT Solver with Zero Human-Written Code
Mikol\'a\v{s} Janota, Mirek Ol\v{s}\'ak
https://arxiv.org/abs/2603.06931 @arXiv_csLO_bot@mastoxiv.page

- Commutativity and Kleisli laws of codensity monads of probability measures
Zev Shirazi
https://arxiv.org/abs/2405.12917 @arXiv_mathCT_bot@mastoxiv.page

- Dependent Directed Wiring Diagrams for Composing Instantaneous Systems
Keri D'Angelo (Cornell University), Sophie Libkind (Topos Institute)
https://arxiv.org/abs/2503.05457 @arXiv_mathCT_bot@mastoxiv.page

- A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Sc...
Wang, Lin, Chen, Li, Yang, Yi, Qin, Luo, Li, Gu, Lu, Yin
https://arxiv.org/abs/2512.24594 @arXiv_csSE_bot@mastoxiv.page

- Proceedings Eighth International Conference on Applied Category Theory
Amar Hadzihasanovic, Jean-Simon Pacaud Lemay
https://arxiv.org/abs/2603.07595 @arXiv_mathCT_bot@mastoxiv.page

toXiv_bot_toot

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
Arun Govindankutty, Sudarshan K. Srinivasan
https://arxiv.org/abs/2603.08762 @arXiv_quantph_bot@mastoxiv.page

- A Simple Constructive Bound on Circuit Size Change Under Truth Table Perturbation
Kirill Krinkin
https://arxiv.org/abs/2603.09379 @arXiv_csCC_bot@mastoxiv.page

- Declarative Scenario-based Testing with RoadLogic
Ezio Bartocci, Alessio Gambi, Felix Gigler, Cristinel Mateis, Dejan Ni\v{c}kovi\'c
https://arxiv.org/abs/2603.09455 @arXiv_csSE_bot@mastoxiv.page

toXiv_bot_toot

d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

Gabriele Masina, Emanuale Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani
https://arxiv.org/abs/2603.09975 https://arxiv.org/pdf/2603.09975 https://arxiv.org/html/2603.09975

arXiv:2603.09975v1 Announce Type: new
Abstract: In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries.
In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. We have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

toXiv_bot_toot

[2026-03-11 Wed (UTC), 1 new article found for cs.LO Logic in Computer Science]

toXiv_bot_toot

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
Bradley P. Allen
https://arxiv.org/abs/2603.06974 @arXiv_csCL_bot@mastoxiv.page

- Learning to Rank the Initial Branching Order of SAT Solvers
Arvid Eriksson, Gabriel Poesia, Roman Bresson, Karl Henrik Johansson, David Broman
https://arxiv.org/abs/2603.07176

- Proceedings Eighth International Conference on Applied Category Theory
Amar Hadzihasanovic, Jean-Simon Pacaud Lemay
https://arxiv.org/abs/2603.07595 @arXiv_mathCT_bot@mastoxiv.page

- The Unit Gap: How Sharing Works in Boolean Circuits
Kirill Krinkin
https://arxiv.org/abs/2603.08033 @arXiv_csCC_bot@mastoxiv.page

- Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an erro...
Joseph Tooby-Smith
https://arxiv.org/abs/2603.08139 @arXiv_hepph_bot@mastoxiv.page

- On the expressive power of inquisitive team logic and inquisitive first-order logic
Juha Kontinen, Ivano Ciardelli
https://arxiv.org/abs/2603.08646 @arXiv_mathLO_bot@mastoxiv.page

toXiv_bot_toot

Central Limits via Dilated Categories

Henning Basold, Ois\'in Flynn-Connolly, Chase Ford, Hao Wang
https://arxiv.org/abs/2603.08266 https://arxiv.org/pdf/2603.08266 https://arxiv.org/html/2603.08266

arXiv:2603.08266v1 Announce Type: new
Abstract: The Central Limit Theorem (CLT) establishes that sufficiently large sequences of independent and identically distributed random variables converge in probability to a normal distribution. This makes the CLT a fundamental building block of statistical reasoning and, by extension, in reasoning about computing systems that are based on statistical inference such as probabilistic programing languages, programs with optimisation, and machine learning components. However, there is no general theory of CLT-like results currently, which forces practitioners to redo proofs without having a good handle on the essential ingredients of CLT-type results. In this paper, we introduce dilated seminorm-enriched category theory as a unifying framework for central limits, and we establish an abstract central limit theorem within that framework. We illustrate how a strengthened version of the classical CLT and the law of large numbers can be obtained as instances of our framework. Moreover, we derive from our framework a novel central limit theorem for symplectic manifolds, the CLT for observables, which finds applications in statistical mechanics.

toXiv_bot_toot

Step Automata

Yong Wang
https://arxiv.org/abs/2603.08043 https://arxiv.org/pdf/2603.08043 https://arxiv.org/html/2603.08043

arXiv:2603.08043v1 Announce Type: new
Abstract: For computation, there existed Turing machine and later-matured automata theory. For low-level parallel computation, there existed variants of Turing machine, such as two-tapes Turing machine and multi-tapes Turing machine. In the literature, the combination of computation and concurrency is still active, such the combination of automata and processes, and the introduction of concurrency into automata: the so-called pomset automata and branch automata. But the linkage of Turing machine and concurrent automaton is still absent. In this paper, we propose the concepts of step automaton and step Turing machine (STM), which a natural extension to traditional automaton and classical Turing machine just allowing an automaton or Turing machine to execute a step of atomic actions (without partial orders pairwise).

toXiv_bot_toot

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Sage Binder, Hanna Lachnitt, Katherine Kosaian
https://arxiv.org/abs/2603.07771 https://arxiv.org/pdf/2603.07771 https://arxiv.org/html/2603.07771

arXiv:2603.07771v1 Announce Type: new
Abstract: In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style scripts to declarative Isar. This allows users to write complex, possibly fragile apply-style scripts, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.

toXiv_bot_toot