Buchumschlag

MCSAT Modulo Transcendental Arithmetics

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Gallego-Hernández, Jorge, Lipparini, Enrico, Mansutti, Alessio
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
von: Lipparini, Enrico, et al.
Veröffentlicht: (2023)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
von: Lipparini, Enrico, et al.
Veröffentlicht: (2025)

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number
von: Gallego-Hernández, Jorge, et al.
Veröffentlicht: (2025)

Optimization Modulo Integer Linear-Exponential Programs
von: Hitarth, S, et al.
Veröffentlicht: (2025)

One-Parametric Presburger Arithmetic has Quantifier Elimination
von: Mansutti, Alessio, et al.
Veröffentlicht: (2025)

Satisfiability Modulo Exponential Integer Arithmetic
von: Frohn, Florian, et al.
Veröffentlicht: (2024)

How (and when) can you fit examples to logic-based hypothesis classes over infinite structures?
von: Benedikt, Michael, et al.
Veröffentlicht: (2026)

A theory of Lending Protocols in DeFi
von: Bartoletti, Massimo, et al.
Veröffentlicht: (2025)

On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
von: Haase, Christoph, et al.
Veröffentlicht: (2024)

The complexity of Presburger arithmetic with power or powers
von: Benedikt, Michael, et al.
Veröffentlicht: (2023)

Integer Linear-Exponential Programming in NP by Quantifier Elimination
von: Chistikov, Dmitry, et al.
Veröffentlicht: (2024)

KindHML: formal verification of smart contracts based on Hennessy-Milner logic
von: Bartoletti, Massimo, et al.
Veröffentlicht: (2026)

Unravelling Cyclic First-Order Arithmetic
von: Leigh, Graham E., et al.
Veröffentlicht: (2025)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
von: Ding, Tianyi, et al.
Veröffentlicht: (2025)

The Arithmetical Hierarchy: A Realizability-Theoretic Perspective
von: Kihara, Takayuki
Veröffentlicht: (2024)

On proving consistency of equational theories in Bounded Arithmetic
von: Beckmann, Arnold, et al.
Veröffentlicht: (2022)

Generalized Optimization Modulo Theories
von: Tsiskaridze, Nestan, et al.
Veröffentlicht: (2024)

Congruence Closure Modulo Groups
von: Kim, Dohan
Veröffentlicht: (2023)

Satisfiability Modulo Theories for Verifying MILP Certificates
von: Wood, Kenan, et al.
Veröffentlicht: (2023)

Integer Reasoning Modulo Different Constants in SMT
von: Pertseva, Elizaveta, et al.
Veröffentlicht: (2025)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
von: Preiner, Mathias, et al.
Veröffentlicht: (2026)

An Effective Orchestral Approach to Satisfiability Modulo Prime Fields
von: Isabel, Miguel, et al.
Veröffentlicht: (2026)

Modulo quantifiers over functional vocabularies extending addition
von: Baskar, A., et al.
Veröffentlicht: (2017)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
von: Feng, Nick, et al.
Veröffentlicht: (2024)

Proofs for Free in the $λΠ$-Calculus Modulo Theory
von: Traversié, Thomas
Veröffentlicht: (2024)

Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
von: Caires-Santos, Ali K., et al.
Veröffentlicht: (2025)

Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti
von: Traversié, Thomas
Veröffentlicht: (2024)

Peano Arithmetic and $μ$MALL
von: Manighetti, Matteo, et al.
Veröffentlicht: (2023)

Towards an Analysis of Proofs in Arithmetic
von: Leitsch, Alexander, et al.
Veröffentlicht: (2025)

ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures
von: Asor, Ohad
Veröffentlicht: (2026)

From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory
von: Blot, Valentin, et al.
Veröffentlicht: (2024)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
von: Komel, Anja Petković, et al.
Veröffentlicht: (2025)

The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract)
von: Aceto, Luca, et al.
Veröffentlicht: (2025)

Nonlinear Arithmetic with SMTLIB Division is Undecidable
von: Jovanovic, Dejan
Veröffentlicht: (2026)

On the Decidability of Monadic Theories of Arithmetic Predicates
von: Berthé, Valérie, et al.
Veröffentlicht: (2024)

On the Decidability of Presburger Arithmetic Expanded with Powers
von: Karimov, Toghrul, et al.
Veröffentlicht: (2024)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
von: Faella, Marco, et al.
Veröffentlicht: (2024)

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
von: Grabmayer, Clemens
Veröffentlicht: (2022)

Incorrectness Separation Logic with Arrays and Pointer Arithmetic
von: Lee, Yeonseok, et al.
Veröffentlicht: (2025)

Canonical Decision Diagrams Modulo Theories
von: Michelutti, Massimo, et al.
Veröffentlicht: (2024)