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 / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B35
@@ Property / Mathematics Subject Classification ID: 03B35 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6585552
@@ Property / zbMATH DE Number: 6585552 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+nonlinear arithmetic
@@ Property / zbMATH Keywords: nonlinear arithmetic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+decision procedure
@@ Property / zbMATH Keywords: decision procedure / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+prototype verification system (PVS)
@@ Property / zbMATH Keywords: prototype verification system (PVS) / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+polynomial inequalities
@@ Property / zbMATH Keywords: polynomial inequalities / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Sturm's theorem
@@ Property / zbMATH Keywords: Sturm's theorem / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Tarski's theorem
@@ Property / zbMATH Keywords: Tarski's theorem / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+automated theorem proving
@@ Property / zbMATH Keywords: automated theorem proving / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+interactive theorem proving
@@ Property / zbMATH Keywords: interactive theorem proving / 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 @@
+Publication
@@ Property / MaRDI profile type: Publication / 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
@@ links / mardi / name / links / mardi / name @@
+Publication:287269