Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269): Difference between revisions

@@ Property / author @@
-César A. Muñoz
@@ Property / author: César A. Muñoz / rank @@
-Normal rank
@@ Property / author @@
+César A. Muñoz
@@ Property / author: César A. Muñoz / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVSio
@@ Property / describes a project that uses: PVSio / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MetiTarski
@@ Property / describes a project that uses: MetiTarski / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RealPaver
@@ Property / describes a project that uses: RealPaver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gappa
@@ Property / describes a project that uses: Gappa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+dReal
@@ Property / describes a project that uses: dReal / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / 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/s10817-015-9320-x
+Normal rank
@@ Property / OpenAlex ID @@
+W1978149312
@@ Property / OpenAlex ID: W1978149312 / rank @@
+Normal rank
@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+Formalization and Execution of Linear Algebra: From Theorems to Algorithms
+Normal rank
@@ Property / cites work @@
+Algorithms in real algebraic geometry
@@ Property / cites work: Algorithms in real algebraic geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
+Normal rank
@@ Property / cites work @@
+Q4079605
@@ Property / cites work: Q4079605 / rank @@
+Normal rank
@@ Property / cites work @@
+Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
+Normal rank
@@ Property / cites work @@
+Verified Real Number Calculations: A Library for Interval Arithmetic
+Normal rank
@@ Property / cites work @@
+A Refinement-Based Approach to Computational Algebra in Coq
+Normal rank
@@ Property / cites work @@
+The Fundamental Theorem of Algebra Made Effective: An Elementary Real-algebraic Proof via Sturm Chains
+Normal rank
@@ Property / cites work @@
+dReal: An SMT Solver for Nonlinear Theories over the Reals
+Normal rank
@@ Property / cites work @@
+Application of Bernstein expansion to the solution of control problems
+Normal rank
@@ Property / cites work @@
+Subresultants revisited.
@@ Property / cites work: Subresultants revisited. / rank @@
+Normal rank
@@ Property / cites work @@
+Point-Free, Set-Free Concrete Linear Algebra
@@ Property / cites work: Point-Free, Set-Free Concrete Linear Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithm 852
@@ Property / cites work: Algorithm 852 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Nonlinear Real Formulas Via Sums of Squares
+Normal rank
@@ Property / cites work @@
+Implementing the cylindrical algebraic decomposition within the Coq system
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Bounds on Real-Valued Functions with Computations
+Normal rank
@@ Property / cites work @@
+On the Generation of Positivstellensatz Witnesses in Degenerate Cases
+Normal rank
@@ Property / cites work @@
+Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
+Normal rank
@@ Property / cites work @@
+Formalization of Bernstein polynomials and applications to global optimization
+Normal rank
@@ Property / cites work @@
+Combined Decision Techniques for the Existential Theory of the Reals
+Normal rank
@@ Property / cites work @@
+Q5807665
@@ Property / cites work: Q5807665 / rank @@
+Normal rank