A search-based procedure for nonlinear real arithmetic
From MaRDI portal
Publication:518407
DOI10.1007/s10703-016-0245-8zbMath1358.68149OpenAlexW2340960908MaRDI QIDQ518407
Patrick D. Lincoln, Ashish Kumar Tiwari
Publication date: 28 March 2017
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-016-0245-8
Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints, The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MetiTarski: An automatic theorem prover for real-valued special functions
- Real quantifier elimination is doubly exponential
- On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
- Partial cylindrical algebraic decomposition for quantifier elimination
- Complexity of deciding Tarski algebra
- Semidefinite programming relaxations for semialgebraic problems
- Fast linear algebra is stable
- Constructing invariants for hybrid systems
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems
- Variant real quantifier elimination
- δ-Complete Decision Procedures for Satisfiability over the Reals
- Solving Non-linear Arithmetic
- Synthesis for Polynomial Lasso Programs
- Transcendental inductive invariants generation for non-linear differential and hybrid systems
- Constraint-Based Approach for Analysis of Hybrid Systems
- Synthesizing Switching Logic Using Constraint Solving
- On the combinatorial and algebraic complexity of quantifier elimination
- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
- Buchberger's algorithm: A constraint-based completion procedure
- Verification and synthesis using real quantifier elimination
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Computer Aided Verification
- Computer Science Logic
- A machine program for theorem-proving
- Computer Aided Verification
