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

@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+A58
@@ Property / Mathematics Subject Classification ID: 41A58 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+G50
@@ Property / Mathematics Subject Classification ID: 65G50 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6644464
@@ Property / zbMATH DE Number: 6644464 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+interval arithmetic
@@ Property / zbMATH Keywords: interval arithmetic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+formal proof
@@ Property / zbMATH Keywords: formal proof / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+decision procedure
@@ Property / zbMATH Keywords: decision procedure / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Coq proof assistant
@@ Property / zbMATH Keywords: Coq proof assistant / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+floating-point arithmetic
@@ Property / zbMATH Keywords: floating-point arithmetic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+nonlinear arithmetic
@@ Property / zbMATH Keywords: nonlinear arithmetic / 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 @@
+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
@@ links / mardi / name / links / mardi / name @@
+Publication:331615