Solovyev, Alexey
(2013)
Formal Computations and Methods.
Doctoral Dissertation, University of Pittsburgh.
(Unpublished)
This is the latest version of this item.
Abstract
We present formal verification methods and procedures for finding bounds of linear programs and proving nonlinear inequalities. An efficient implementation of formal arithmetic computations is also described. Our work is an integral part of the Flyspeck project (a formal proof of the Kepler conjecture) and we show how developed formal procedures solve formal computational problems in this project. We also introduce our implementation of SSReflect language (originally developed by G. Gonthier in Coq) in HOL Light.
Share
| Citation/Export: |
|
| Social Networking: |
|
Details
| Item Type: |
University of Pittsburgh ETD
|
| Status: |
Unpublished |
| Creators/Authors: |
| Creators | Email | Pitt Username | ORCID  |
|---|
| Solovyev, Alexey | ays9@pitt.edu | AYS9 | |
|
| ETD Committee: |
|
| Date: |
30 January 2013 |
| Date Type: |
Publication |
| Defense Date: |
28 November 2012 |
| Approval Date: |
30 January 2013 |
| Submission Date: |
30 November 2012 |
| Access Restriction: |
No restriction; Release the ETD for access worldwide immediately. |
| Number of Pages: |
119 |
| Institution: |
University of Pittsburgh |
| Schools and Programs: |
Dietrich School of Arts and Sciences > Mathematics |
| Degree: |
PhD - Doctor of Philosophy |
| Thesis Type: |
Doctoral Dissertation |
| Refereed: |
Yes |
| Uncontrolled Keywords: |
Formal Proof, Verification, HOL, Kepler Conjecture, Flyspeck |
| Date Deposited: |
30 Jan 2013 19:12 |
| Last Modified: |
15 Nov 2016 14:07 |
| URI: |
http://d-scholarship.pitt.edu/id/eprint/16721 |
Available Versions of this Item
-
Formal Computations and Methods. (deposited 30 Jan 2013 19:12)
[Currently Displayed]
Metrics
Monthly Views for the past 3 years
Plum Analytics
Actions (login required)
 |
View Item |
![[feed]](/images/feed-icon-32x32.png){kind=icon}