Zobrazeno 1 - 5 of 5 pro vyhledávání: '"ROLAND ZUMKELLER"'
1
Akademický článek
A FORMAL PROOF OF THE KEPLER CONJECTURE
Autor: THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TAT THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
Publikováno v: Forum of Mathematics, Pi, Vol 5 (2017)
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
Externí odkaz: https://doaj.org/article/0dae9a3d3e584c73a937daefc20afe3b
Zobrazit plný text záznamu
2
A FORMAL PROOF OF THE KEPLER CONJECTURE
Autor: Roland Zumkeller, Ky Khac Vu, Joseph Pleso, Tobias Nipkow, Truong Le Hoang, Truong Quang Nguyen, Sean McLaughlin, Steven Obua, Jason Rute, An Hoai Thi Ta, Mark Adams, Alexey Solovyev, Thang Tat Nguyen, Trung Nam Tran, Cezary Kaliszyk, Dat Tat Dang, John Harrison, Victor Magron, Gertrud Bauer, Diep Thi Trieu, Josef Urban, Thomas C. Hales
Publikováno v: Forum of Mathematics. Pi, 5, 1-29
Forum of Mathematics. Pi, 5, pp. 1-29
Forum of Mathematics, Pi
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a280db53ee95a279e1aa5fc6830335ea
https://hdl.handle.net/2066/176365
Zobrazit plný text záznamu
4
A revision of the proof of the Kepler conjecture
Autor: Sean McLaughlin, Roland Zumkeller, Tobias Nipkow, John Harrison, Steven Obua, Thomas C. Hales
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex.
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::01cbc61b43c4078259ef06dfaa2d4f04
Zobrazit plný text záznamu
5
Formal Global Optimisation with Taylor Models
Autor: Roland Zumkeller
Publikováno v: Automated Reasoning ISBN: 9783540371878
IJCAR
Formal proofs and global optimisation are two research areas that have been heavily influenced by the arrival of computers. This article aims to bring both further together by formalising a global optimisation method based on Taylor models: a set of
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b5683296ece68f3848b53f8323fe836c
https://doi.org/10.1007/11814771_35
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje