Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
DOI10.1007/978-3-031-19992-9_9zbMATH Open1522.68716OpenAlexW4312267877MaRDI QIDQ6160909FDOQ6160909
Authors: Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani 
Publication date: 2 June 2023
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://hdl.handle.net/11572/369588
Recommendations
- Satisfiability modulo transcendental functions via incremental linearization
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- dReal: an SMT solver for nonlinear theories over the reals
- Subtropical satisfiability
- Deciding polynomial-transcendental problems
Nonlinear programming (90C30) Degree, winding number (55M25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Algorithm 852
- dReal: an SMT solver for nonlinear theories over the reals
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- The MathSAT5 SMT solver
- Introduction to Interval Analysis
- Some undecidable problems involving elementary functions of a real variable
- \(\delta \)-complete decision procedures for satisfiability over the reals
- A Model-Constructing Satisfiability Calculus
- Title not available (Why is that?)
- Quasi-decidability of a fragment of the first-order theory of real numbers
- Topological degree theory and applications.
- Title not available (Why is that?)
- Understanding the Hastings Algorithm
- Computation of Topological Degree Using Interval Arithmetic, and Applications
- Interval Methods for Systems of Equations
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Effective topological degree computation based on interval arithmetic
- raSAT: an SMT solver for polynomial constraints
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Safety verification of non-linear hybrid systems is quasi-decidable
This page was built for publication: Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160909)
