Buchumschlag

Nonlinear Arithmetic with SMTLIB Division is Undecidable

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
1. Verfasser:	Jovanovic, Dejan
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

Undecidability of theories of semirings with fixed points
von: Das, Anupam, et al.
Veröffentlicht: (2025)

The Undecidability of Quantified Announcements
von: Ågotnes, Thomas, et al.
Veröffentlicht: (2024)

Undecidability of Linear Logics without Weakening
von: Suzuki, Jun, et al.
Veröffentlicht: (2025)

Improving NLSAT for Nonlinear Real Arithmetic
von: Wang, Zhonghan
Veröffentlicht: (2024)

Systemic Constraints of Undecidability
von: Bulin, Seth
Veröffentlicht: (2025)

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

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
von: Dudenhefner, Andrej
Veröffentlicht: (2026)

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

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
von: Chodil, Miroslav, et al.
Veröffentlicht: (2025)

HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder
von: Fortin, Marie, et al.
Veröffentlicht: (2023)

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)

An Undecidability Proof for the Plan Existence Problem
von: Achilleos, Antonis
Veröffentlicht: (2026)

On Formally Undecidable Traits of Intelligent Machines
von: Fox, Matthew
Veröffentlicht: (2024)

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
von: Kobayashi, Naoki
Veröffentlicht: (2024)

Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops
von: Nakamura, Yoshiki
Veröffentlicht: (2025)

MCSAT Modulo Transcendental Arithmetics
von: Gallego-Hernández, Jorge, et al.
Veröffentlicht: (2026)

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)

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

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

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

Teaching Divisibility and Binomials with Coq
von: Boldo, Sylvie, et al.
Veröffentlicht: (2024)

Language Equivalence is Undecidable in VASS with Restricted Nondeterminism
von: Czerwiński, Wojciech, et al.
Veröffentlicht: (2025)

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

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
von: Su, Wanyun, et al.
Veröffentlicht: (2024)

RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics
von: Yamaguchi, Tomoya, et al.
Veröffentlicht: (2025)

Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy
von: Bonakdarpour, Borzoo, et al.
Veröffentlicht: (2024)

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
von: Ito, Sohei, et al.
Veröffentlicht: (2025)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
von: Hozzová, Petra, et al.
Veröffentlicht: (2024)

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

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
von: Habermehl, Peter, et al.
Veröffentlicht: (2024)

Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
von: Wolter, Frank, et al.
Veröffentlicht: (2024)

The Constraint Satisfaction Problem Over Multisorted Cores
von: Delic, Dejan, et al.
Veröffentlicht: (2025)

Verifying Global Two-Safety Properties in Neural Networks with Confidence
von: Athavale, Anagha, et al.
Veröffentlicht: (2024)

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

The General and Finite Satisfiability Problems for PCTL are Undecidable
von: Chodil, Miroslav, et al.
Veröffentlicht: (2024)

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
von: Bryce, Aaron, et al.
Veröffentlicht: (2026)

Complex Algebras of Arithmetic
von: Düntsch, Ivo, et al.
Veröffentlicht: (2009)

Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability
von: Akshay, S., et al.
Veröffentlicht: (2026)