The HOL Light Theory of Euclidean Space
The HOL Light Theory of Euclidean Space
About this item
Full title
Author / Creator
Publisher
Dordrecht: Springer Netherlands
Journal title
Language
English
Formats
Publication information
Publisher
Dordrecht: Springer Netherlands
Subjects
More information
Scope and Contents
Contents
We describe the library of theorems about N-dimensional Euclidean space that has been formalized in the HOL Light prover. This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic a...
Alternative Titles
Full title
The HOL Light Theory of Euclidean Space
Authors, Artists and Contributors
Author / Creator
Identifiers
Primary Identifiers
Record Identifier
TN_cdi_proquest_journals_1366364344
Permalink
https://devfeature-collection.sl.nsw.gov.au/record/TN_cdi_proquest_journals_1366364344
Other Identifiers
ISSN
0168-7433
E-ISSN
1573-0670
DOI
10.1007/s10817-012-9250-9
