Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TPHOL

2005

IEEE

2005

IEEE

We describe a formalization of the elementary algebra, topology and analysis of ﬁnite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is RN with the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimension N in a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitrary N-dimensional Euclidean space, e.g. Brouwer’s ﬁxpoint theorem and the differentiability of inverse functions.1 1 The problem with RN Since the pioneering work of Jutting [9], several people i...

Related Content

Added |
25 Jun 2010 |

Updated |
25 Jun 2010 |

Type |
Conference |

Year |
2005 |

Where |
TPHOL |

Authors |
John Harrison |

Comments (0)