arXiv cs.LO bot

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

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

[2026-04-14 Tue (UTC), 3 new articles 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]:
- Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer
Jonathan P. Bowen, Henri Habrias
https://arxiv.org/abs/2604.07353 https://mastoxiv.page/@arXiv_csGL_bot/116379255256673345

- Munkres' General Topology Autoformalized in Isabelle/HOL
Dustin Bryant, Jonathan Juli\'an Huerta y Munive, Cezary Kaliszyk, Josef Urban
https://arxiv.org/abs/2604.07455

- Capture-Quiet Decomposition: A Verification Theorem for Chess Endgame Tablebases
Alexander Pavlov
https://arxiv.org/abs/2604.07907

- Coexact completion of profinite Heyting algebras and uniform interpolation
Lingyuan Ye
https://arxiv.org/abs/2604.08267 https://mastoxiv.page/@arXiv_mathLO_bot/116379350640119978

- Metacat: a categorical framework for formal systems
Paul Wilson
https://arxiv.org/abs/2604.08331 https://mastoxiv.page/@arXiv_mathCT_bot/116379446065169962

toXiv_bot_toot

[2026-04-13 Mon (UTC), 1 new article found for cs.LO Logic in Computer Science]

toXiv_bot_toot

On the Decompositionality of Neural Networks

Junyong Lee, Baek-Ryun Seong, Sang-Ki Ko, Andrew Ferraiuolo, Minwoo Kang, Hyuntae Jeon, Seungmin Lim, Jieung Kim
https://arxiv.org/abs/2604.07868 https://arxiv.org/pdf/2604.07868 https://arxiv.org/html/2604.07868

arXiv:2604.07868v1 Announce Type: new
Abstract: Recent advances in deep neural networks have achieved state-of-the-art performance across vision and natural language processing tasks. In practice, however, most models are treated as monolithic black-box functions, limiting maintainability, component-wise optimization, and systematic testing and verification. Despite extensive work on pruning and empirical decomposition, the field still lacks a principled semantic notion of when a neural network can be meaningfully decomposed.
We introduce neural decompositionality, a formal notion defined as a semantic-preserving abstraction over neural architectures. Our key insight is that decompositionality should be characterized by the preservation of semantic behavior along the model's decision boundary, which governs classification outcomes. This yields a semantic contract between the original model and its components, enabling a rigorous formulation of decomposition.
Building on this foundation, we develop a boundary-aware framework, SAVED (Semantic-Aware Verification-Driven Decomposition), which operationalizes the proposed definition. SAVED combines counterexample mining over low logic-margin inputs, probabilistic coverage, and structure-aware pruning to construct decompositions that preserve decision-boundary semantics.
We evaluate our approach on CNNs, language Transformers, and Vision Transformers. Results show clear architectural differences: language Transformers largely preserve boundary semantics under decomposition, whereas vision models frequently violate the decompositionality criterion, indicating intrinsic limits. Overall, our work establishes decompositionality as a formally definable and empirically testable property, providing a foundation for modular reasoning about neural networks.

toXiv_bot_toot

Formally Guaranteed Control Adaptation for ODD-Resilient Autonomous Systems

Gricel V\'azquez, Calum Imrie, Sepeedeh Shahbeigi, Nawshin Mannan Proma, Tian Gan, Victoria J Hodge, John Molloy, Simos Gerasimou
https://arxiv.org/abs/2604.07414 https://arxiv.org/pdf/2604.07414 https://arxiv.org/html/2604.07414

arXiv:2604.07414v1 Announce Type: new
Abstract: Ensuring reliable performance in situations outside the Operational Design Domain (ODD) remains a primary challenge in devising resilient autonomous systems. We explore this challenge by introducing an approach for adapting probabilistic system models to handle out-of-ODD scenarios while, in parallel, providing quantitative guarantees. Our approach dynamically extends the coverage of existing system situation capabilities, supporting the verification and adaptation of the system's behaviour under unanticipated situations. Preliminary results demonstrate that our approach effectively increases system reliability by adapting its behaviour and providing formal guarantees even under unforeseen out-of-ODD situations.

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

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 https://mastoxiv.page/@arXiv_csLO_bot/115326156109378477

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

- 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 https://mastoxiv.page/@arXiv_csAI_bot/114578736547839729

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

toXiv_bot_toot

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
Dominik Blain
https://arxiv.org/abs/2604.12172 https://mastoxiv.page/@arXiv_csCR_bot/116407703793850484

- Technical Report -- A Context-Sensitive Multi-Level Similarity Framework for First-Order Logic Ar...
Victor David, J\'er\^ome Delobelle, Jean-Guy Mailly
https://arxiv.org/abs/2604.12534 https://mastoxiv.page/@arXiv_csAI_bot/116407927276210342

- Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Exte...
Haselwarter, Aguirre, Gregersen, Li, Tassarotti, Birkedal
https://arxiv.org/abs/2604.12713 https://mastoxiv.page/@arXiv_csPL_bot/116407593036588681

toXiv_bot_toot

Replaced article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Towards Efficient Matching of Regexes with Backreferences using Register Set Automata (Technical ...
Havlena, Hol\'ik, Leng\'al, Va\v{s}\'ak, Gul\v{c}\'ikov\'a
https://arxiv.org/abs/2205.12114

- The Temporal Logic Synthesis Format TLSF v1.2
Swen Jacobs, Guillermo A. Perez, Philipp Schlehuber-Caissier
https://arxiv.org/abs/2303.03839

- Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
\'Etienne Andr\'e, Didier Lime, Olivier H. Roux
https://arxiv.org/abs/2310.09109 https://mastoxiv.page/@arXiv_csLO_bot/111242836200967705

- Computation by infinite descent made explicit
Sebastian Enqvist
https://arxiv.org/abs/2506.22206 https://mastoxiv.page/@arXiv_csLO_bot/114771395219732779

- A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
Kyveli Doveri, Pierre Ganty, B. Srivathsan
https://arxiv.org/abs/2601.15104 https://mastoxiv.page/@arXiv_csFL_bot/115937686699646733

- Decidable By Construction: Design-Time Verification for Trustworthy AI
Houston Haynes
https://arxiv.org/abs/2603.25414 https://mastoxiv.page/@arXiv_csPL_bot/116300008810122807

- Exact Structural Abstraction and Tractability Limits
Tristan Simas
https://arxiv.org/abs/2604.07349 https://mastoxiv.page/@arXiv_csCC_bot/116373589641392287

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

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

Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model

Daniel O. Martinez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
https://arxiv.org/abs/2604.12981 https://arxiv.org/pdf/2604.12981 https://arxiv.org/html/2604.12981

arXiv:2604.12981v1 Announce Type: new
Abstract: Martinez-Rivillas and de Queiroz gave extensional Kan semantics for the untyped lambda-calculus and later constructed the concrete K-infinity homotopy-model. The two main mathematical results of the present paper are these. First, we show that a smaller front-seed coherence package (WL, WR) together with an inner-right-front pentagon contraction already suffices to recover the associator comparison, semantic pentagon, and bridge theorems used in the later semantic arguments. Second, we prove explicit global reify, reflect, and application formulas for K-infinity, with exact coordinatewise identities at every finite stage. We also record two structural clarifications: the recursive all-dimensional continuation of the explicit low-dimensional tower is obtained by a finite packaging phase followed by a uniform equality-generated recursion; and, on a deliberately fixed forward witness language for the classical separation span, the canonical identity-type higher tower on K-infinity forces all higher non-connection once the two witness classes land at distinct points. The paper is fully formalized in Lean 4, and the project sources contain no local uses of sorry, admit, or axiom.

toXiv_bot_toot

[2026-04-15 Wed (UTC), 2 new articles found for cs.LO Logic in Computer Science]

toXiv_bot_toot

Neuro-Symbolic Strong-AI Robots with Closed Knowledge Assumption: Learning and Deductions

Zoran Majkic
https://arxiv.org/abs/2604.09567 https://arxiv.org/pdf/2604.09567 https://arxiv.org/html/2604.09567

arXiv:2604.09567v1 Announce Type: new
Abstract: Knowledge representation formalisms are aimed to represent general conceptual information and are typically used in the construction of the knowledge base of reasoning agent. A knowledge base can be thought of as representing the beliefs of such an agent. Like a child, a strong-AI (AGI) robot would have to learn through input and experiences, constantly progressing and advancing its abilities over time. Both with statistical AI generated by neural networks we need also the concept of \textsl{causality} of events traduced into directionality of logic entailments and deductions in order to give to robots the emulation of human intelligence. Moreover, by using the axioms we can guarantee the \textsl{controlled security} about robot's actions based on logic inferences.
For AGI robots we consider the 4-valued Belnap's bilattice of truth-values with knowledge ordering as well, where the value "unknown" is the bottom value, the sentences with this value are indeed unknown facts, that is, the missed knowledge in the AGI robots. Thus, these unknown facts are not part of the robot's knowledge database, and by learn through input and experiences, the robot's knowledge would be naturally expanded over time.
Consequently, this phenomena can be represented by the Closed Knowledge Assumption and Logic Inference provided by this paper.
Moreover, the truth-value "inconsistent", which is the top value in the knowledge ordering of Belnap's bilattice, is necessary for strong-AI robots to be able to support such inconsistent information and paradoxes, like Liar paradox, during deduction processes.

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 https://mastoxiv.page/@arXiv_csCL_bot/116204505028693110

- 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 https://mastoxiv.page/@arXiv_mathCT_bot/116203781487933863

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

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

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

toXiv_bot_toot

Replaced article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-s...
Junle Li, Siqi Chen, Jiakai Li, Meiqi Tian, Bingzhuo Zhong
https://arxiv.org/abs/2503.15840 https://mastoxiv.page/@arXiv_csLO_bot/114199204034892273

- Proving Circuit Functional Equivalence in Zero Knowledge
Sirui Shen, Zunchen Huang, Chenglu Jin
https://arxiv.org/abs/2601.11173 https://mastoxiv.page/@arXiv_csCR_bot/115921096042252298

- Profunctorial algebras
Quentin Aristote, Umberto Tarantino
https://arxiv.org/abs/2601.22721 https://mastoxiv.page/@arXiv_mathCT_bot/116000072697273863

- SuperDP: Differential Privacy Refutation via Supermartingales
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, {\DJ}or{\dj}e \v{Z}ikeli\'c
https://arxiv.org/abs/2603.26215 https://mastoxiv.page/@arXiv_csPL_bot/116317023927234974

toXiv_bot_toot

When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions

David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
https://arxiv.org/abs/2604.07626 https://arxiv.org/pdf/2604.07626 https://arxiv.org/html/2604.07626

arXiv:2604.07626v1 Announce Type: new
Abstract: Ordinary algebraic equality is not a sound rewrite principle for measurement-bearing expressions. Reuse of the same observation matters, and division can make algebraically equal forms differ on where they are defined. We present a unified semantics that tracks both provenance and definedness. Token-sensitive enclosure semantics yields judgments for one-way rewriting and interchangeability. An admissible-domain refinement yields a domain-safe rewrite judgment, and support-relative variants connect local and global admissibility. Reduction theorems recover the enclosure-based theory on universally admissible supports. Recovery theorems internalize cancellation, background subtraction, and positive-interval self-division. Strictness theorems show that reachable singularities make simplification one-way and make common-domain equality too weak for licensed replacement. An insufficiency theorem shows that erasing token identity collapses distinctions that definedness alone cannot recover. All definitions and theorems are formalized in sorry-free Lean 4.

toXiv_bot_toot

A Domain-Theoretic Foundation for Imprecise Probability and Credal Sets

Abbas Edalat, Pietro Di Gianantonio, Amin Farjudian
https://arxiv.org/abs/2604.09272 https://arxiv.org/pdf/2604.09272 https://arxiv.org/html/2604.09272

arXiv:2604.09272v1 Announce Type: new
Abstract: We develop a domain-theoretic framework for imprecise probability reasoning and inference on general topological spaces with a countably based continuous lattice of open sets. We address two distinct forms of uncertainty: partial or incomplete event descriptions, and sets of probability distributions as represented by credal sets -- as well as their combination. Within this framework, we construct a theory of conditional probability and derive novel inference rules for performing Bayesian updating in the presence of these two complementary types of imprecision. These results are extended to a theory of conditional independence for imprecise probabilistic events. We also formulate logical predicates for conditional probability, Bayesian updating, and conditional independence, and we obtain the relevant soundness and completeness results. A key contribution is the construction of a Scott-continuous mapping from any credal set to the domain of intervals, providing a domain-theoretic realisation of classical results from capacity theory and Choquet integration. Finally, we introduce and study a new family of credal sets generated by iterated function systems with imprecise probability weights, broadening the scope of computationally tractable imprecise probabilistic models. The resulting computable framework unifies logical, topological, and measure-theoretic perspectives on uncertainty, supporting robust probabilistic inference under partial and set-valued information.

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

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 https://mastoxiv.page/@arXiv_csLO_bot/116203950574784496

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

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

- 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 https://mastoxiv.page/@arXiv_csSE_bot/115819382474114704

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

toXiv_bot_toot

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology

Ond\v{r}ej Huvar, Martin Jon\'a\v{s}, Samuel Pastva
https://arxiv.org/abs/2604.07496 https://arxiv.org/pdf/2604.07496 https://arxiv.org/html/2604.07496

arXiv:2604.07496v1 Announce Type: new
Abstract: The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand.
We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

toXiv_bot_toot

A Linear Temporal Logic of Frequencies on Series of Events

Melissa Antonelli, Leonardo Ceragioli, Alessandro Buda, Giuseppe Primiero
https://arxiv.org/abs/2604.10669 https://arxiv.org/pdf/2604.10669 https://arxiv.org/html/2604.10669

arXiv:2604.10669v1 Announce Type: new
Abstract: This paper introduces LTLF, a temporal logic designed to express the frequency properties of event series in a natural but rigorous manner. By introducing novel, measure-sensitive operators, LTLF allows for the evaluation of frequencies and the prediction of future occurrences, thus providing a formal framework to monitor and control quantitative systems, such as machine learning classifiers. The core novelty lies in the introduction of original modal quantifiers associated with a standard Kripke-style semantics. These quantifiers enable the explicit formalization of event series properties and the investigation of the relationship between actual observed frequencies and ideal distributions within a single logical structure. This framework bridges the gap between formal logical reasoning and empirical observation.

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

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

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Hypergraph Neural Networks Accelerate MUS Enumeration
Hiroya Ijima, Koichiro Yawata
https://arxiv.org/abs/2604.09001 https://mastoxiv.page/@arXiv_csAI_bot/116396227087175533

- A Deductive System for Contract Satisfaction Proofs
Arthur Correnson, Haoyi Zeng, Jana Hofmann
https://arxiv.org/abs/2604.09165 https://mastoxiv.page/@arXiv_csPL_bot/116396271652378265

toXiv_bot_toot

Simple Types for Polymorphic Functions

Barry Jay, Johannes Bader
https://arxiv.org/abs/2604.12194 https://arxiv.org/pdf/2604.12194 https://arxiv.org/html/2604.12194

arXiv:2604.12194v1 Announce Type: new
Abstract: This paper introduces a simple type system for combinatory logic in which combinators have at most one type, whose polymorphism is revealed by application. The combinatory types exactly describe the structure of their values, which may be hidden by abstract types, such as list types and function types. Even without any quantified types, it supports polymorphism beyond that of the Hindley-Milner type system that underpins functional programming, and an effective type inference algorithm. Also, the simplicity of the formalism should make other static program analyses easier.

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 https://mastoxiv.page/@arXiv_quantph_bot/116209540267130692

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

- 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 https://mastoxiv.page/@arXiv_csSE_bot/116209858098118901

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

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

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

toXiv_bot_toot

[2026-03-11 Wed (UTC), 1 new article 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]:
- The calculus of neo-Peircean relations
Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, Pawel Sobocinski
https://arxiv.org/abs/2505.05306 https://mastoxiv.page/@arXiv_csLO_bot/114476657102287099

- PROMISE: Proof Automation as Structural Imitation of Human Reasoning
Youngjoo Ahn, Sangyeop Yeo, Gijung Im, Jongmin Lee, Jinyoung Yeo, Jieung Kim
https://arxiv.org/abs/2604.05399 https://mastoxiv.page/@arXiv_csLO_bot/116367942424089193

toXiv_bot_toot

Knowledge on a Budget

Ondrej Majer, Krishna Manoorkar, Wolfgang Poiger, Igor Sedl\'ar
https://arxiv.org/abs/2604.11245 https://arxiv.org/pdf/2604.11245 https://arxiv.org/html/2604.11245

arXiv:2604.11245v1 Announce Type: new
Abstract: In various computational systems, accessing information incurs time, memory or energy costs. However, standard epistemic logics usually model the acquisition of evidence as a cost-free process, which restricts their applicability in environments with limited resources. In this paper, we bridge the gap between qualitative epistemic reasoning and quantitative resource constraints by introducing semiring-annotated topological spaces (seats). Building on Topological Evidence Logic (TEL), we extend the representation of evidence as open sets, adding an annotation function that maps evidence to semiring ideals, representing the resource budgets sufficient for observation. This framework allows us to reason not only about what is observable in principle, but also about what is affordable given a specific budget. We develop a family of seat-based epistemic logics with resource-indexed modalities and provide sound, strongly complete axiomatisations for these logics. Furthermore, we introduce suitable notions of bisimulation and disjoint union to delineate the expressive power of our framework.

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

Crosslisted article(s) found for cs.LO. https://arxiv.org/list/cs.LO/new
[1/1]:
- Factorizing formal contexts from closures of necessity operators
Roberto G. Arag\'on, Jes\'us Medina, Elo\'isa Ram\'irez-Poussa
https://arxiv.org/abs/2604.09582 https://mastoxiv.page/@arXiv_csAI_bot/116401907108404515

- Complexity of Consistency Testing for the Release-Acquire Semantics
R. Govind, S. Krishna, Sanchari Sil, B. Srivathsan
https://arxiv.org/abs/2604.09589 https://mastoxiv.page/@arXiv_csCC_bot/116401888758368052

- A formal proof of the Ramanujan--Nagell theorem in Lean 4
Barinder S. Banwait
https://arxiv.org/abs/2604.09808 https://mastoxiv.page/@arXiv_mathNT_bot/116402005116657220

- Planted-solution SAT and Ising benchmarks from integer factorization
Itay Hen
https://arxiv.org/abs/2604.09837 https://mastoxiv.page/@arXiv_quantph_bot/116402150279561530

- Intent-aligned Formal Specification Synthesis via Traceable Refinement
Ye, Yang, Su, Liao, Tenka, Qin, Ghai, Song, Kong
https://arxiv.org/abs/2604.10392 https://mastoxiv.page/@arXiv_csLG_bot/116402477283967424

- THEIA: Learning Complete Kleene Three-Valued Logic in a Pure-Neural Modular Architecture
Augustus Haoyang Li
https://arxiv.org/abs/2604.11284 https://mastoxiv.page/@arXiv_csLG_bot/116402567071585915

toXiv_bot_toot

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 https://mastoxiv.page/@arXiv_quantph_bot/116220940765105596

toXiv_bot_toot