Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615): Difference between revisions

@@ Property / describes a project that uses @@
+MetiTarski
@@ Property / describes a project that uses: MetiTarski / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flocq
@@ Property / describes a project that uses: Flocq / 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 @@
+Sollya
@@ Property / describes a project that uses: Sollya / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1915348541
@@ Property / OpenAlex ID: W1915348541 / rank @@
+Normal rank
@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+Certification of Bounds of Non-linear Functions: The Templates Method
+Normal rank
@@ Property / cites work @@
+Formalization of Bernstein polynomials and applications to global optimization
+Normal rank
@@ Property / cites work @@
+Horner's rule for interval evaluation revisited
@@ Property / cites work: Horner's rule for interval evaluation revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient and accurate computation of upper bounds of approximation errors
+Normal rank
@@ Property / cites work @@
+Sollya: An Environment for the Development of Numerical Codes
+Normal rank
@@ Property / cites work @@
+Verified Real Number Calculations: A Library for Interval Arithmetic
+Normal rank
@@ Property / cites work @@
+Q4808034
@@ Property / cites work: Q4808034 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Nonlinear Real Formulas Via Sums of Squares
+Normal rank
@@ Property / cites work @@
+Proving Bounds on Real-Valued Functions with Computations
+Normal rank
@@ Property / cites work @@
+Floating-point arithmetic in the Coq system
@@ Property / cites work: Floating-point arithmetic in the Coq system / rank @@
+Normal rank
@@ Property / cites work @@
+Q5566070
@@ Property / cites work: Q5566070 / rank @@
+Normal rank
@@ Property / cites work @@
+Handbook of Floating-Point Arithmetic
@@ Property / cites work: Handbook of Floating-Point Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Table-driven implementation of the exponential function in IEEE floating-point arithmetic
+Normal rank
@@ Property / cites work @@
+Fast evaluation of elementary mathematical functions with correctly rounded last bit
+Normal rank