Link to the University of Pittsburgh Homepage
Link to the University Library System Homepage Link to the Contact Us Form

Formal Computations and Methods

Solovyev, Alexey (2013) Formal Computations and Methods. Doctoral Dissertation, University of Pittsburgh. (Unpublished)

This is the latest version of this item.

Primary Text

Download (728kB) | Preview


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.


Social Networking:
Share |


Item Type: University of Pittsburgh ETD
Status: Unpublished
CreatorsEmailPitt UsernameORCID
Solovyev, Alexeyays9@pitt.eduAYS9
ETD Committee:
TitleMemberEmail AddressPitt UsernameORCID
Committee ChairHales, Thomashales@pitt.eduHALES
Committee MemberConstantine, Gregorygmc@pitt.eduGMC
Committee MemberIon, Bogdanbion@pitt.eduBION
Committee MemberAvigad,
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

Available Versions of this Item

  • Formal Computations and Methods. (deposited 30 Jan 2013 19:12) [Currently Displayed]


Monthly Views for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item