Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(8 intermediate revisions by 4 users not shown) | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68T15 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 41A58 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 65G50 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
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 | |||
Property / describes a project that uses: MetiTarski / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: PVS / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Flocq / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Coq / rank | |||
Normal rank | |||
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 | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 03:03, 20 March 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
27 October 2016
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