Satisfiability modulo exponential integer arithmetic

DOI10.1007/978-3-031-63498-7_21MaRDI QIDQ7034855zbMATH OpenFDO

Authors Florian Frohn, Jürgen Giesl

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_21

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• -complete decision procedures for satisfiability over the reals
• Abstract acceleration of general linear loops
• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• Fast acceleration of ultimately periodic relations
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• MetiTarski: An automatic theorem prover for real-valued special functions
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
• Satisfiability modulo exponential integer arithmetic
• Smt-Switch: a solver-agnostic C++ API for SMT solving
• Termination of triangular Integer loops is decidable
• Termination of triangular polynomial loops
• The complexity of Presburger arithmetic with power or powers
• The MathSAT5 SMT solver
• Under-approximating loops in C programs for fast counterexample detection

Cited in

(4)

• Formal languages and arithmetic theories: recent results and open problems
• Integer linear-exponential programming in NP by quantifier elimination
• Satisfiability modulo exponential integer arithmetic
• One-parametric Presburger arithmetic has quantifier elimination

This page was built for publication: Satisfiability modulo exponential integer arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034855)