A search-based procedure for nonlinear real arithmetic (Q518407): Difference between revisions

@@ Property / author @@
-Ashish Kumar Tiwari
@@ Property / author: Ashish Kumar Tiwari / rank @@
-Normal rank
@@ Property / author @@
-Patrick D. Lincoln
@@ Property / author: Patrick D. Lincoln / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+JBernstein
@@ Property / describes a project that uses: JBernstein / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+EFSMT
@@ Property / describes a project that uses: EFSMT / rank @@
+Normal rank
@@ Property / author @@
+Ashish Kumar Tiwari
@@ Property / author: Ashish Kumar Tiwari / rank @@
+Normal rank
@@ Property / author @@
+Patrick D. Lincoln
@@ Property / author: Patrick D. Lincoln / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10703-016-0245-8
+Normal rank
@@ Property / OpenAlex ID @@
+W2340960908
@@ Property / OpenAlex ID: W2340960908 / rank @@
+Normal rank
@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+Buchberger's algorithm: A constraint-based completion procedure
+Normal rank
@@ Property / cites work @@
+On the combinatorial and algebraic complexity of quantifier elimination
+Normal rank
@@ Property / cites work @@
+Q4210476
@@ Property / cites work: Q4210476 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial cylindrical algebraic decomposition for quantifier elimination
+Normal rank
@@ Property / cites work @@
+Q4079605
@@ Property / cites work: Q4079605 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Real quantifier elimination is doubly exponential
@@ Property / cites work: Real quantifier elimination is doubly exponential / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+Fast linear algebra is stable
@@ Property / cites work: Fast linear algebra is stable / rank @@
+Normal rank
@@ Property / cites work @@
+Q5457277
@@ Property / cites work: Q5457277 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+δ-Complete Decision Procedures for Satisfiability over the Reals
+Normal rank
@@ Property / cites work @@
+dReal: An SMT Solver for Nonlinear Theories over the Reals
+Normal rank
@@ Property / cites work @@
+Complexity of deciding Tarski algebra
@@ Property / cites work: Complexity of deciding Tarski algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Constraint-Based Approach for Analysis of Hybrid Systems
+Normal rank
@@ Property / cites work @@
+Variant real quantifier elimination
@@ Property / cites work: Variant real quantifier elimination / rank @@
+Normal rank
@@ Property / cites work @@
+An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesis for Polynomial Lasso Programs
@@ Property / cites work: Synthesis for Polynomial Lasso Programs / rank @@
+Normal rank
@@ Property / cites work @@
+A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
+Normal rank
@@ Property / cites work @@
+Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
+Normal rank
@@ Property / cites work @@
+Semidefinite programming relaxations for semialgebraic problems
+Normal rank
@@ Property / cites work @@
+Transcendental inductive invariants generation for non-linear differential and hybrid systems
+Normal rank
@@ Property / cites work @@
+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
+Normal rank
@@ Property / cites work @@
+Hybrid Systems: Computation and Control
@@ Property / cites work: Hybrid Systems: Computation and Control / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing invariants for hybrid systems
@@ Property / cites work: Constructing invariants for hybrid systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verification and synthesis using real quantifier elimination
+Normal rank
@@ Property / cites work @@
+Synthesizing Switching Logic Using Constraint Solving
+Normal rank
@@ Property / cites work @@
+Q5792485
@@ Property / cites work: Q5792485 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid Systems: Computation and Control
@@ Property / cites work: Hybrid Systems: Computation and Control / rank @@
+Normal rank