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

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

Latest revision as of 20:22, 12 July 2024

scientific article
Language Label Description Also known as
English
Proving tight bounds on univariate expressions with elementary functions in Coq
scientific article

    Statements

    Proving tight bounds on univariate expressions with elementary functions in Coq (English)
    0 references
    0 references
    0 references
    27 October 2016
    0 references
    0 references
    0 references
    0 references
    0 references
    interval arithmetic
    0 references
    formal proof
    0 references
    decision procedure
    0 references
    Coq proof assistant
    0 references
    floating-point arithmetic
    0 references
    nonlinear arithmetic
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references