| Time: | 12 - 1:30 p.m. |
| Room: |
Wean Hall 7220
|
| Speaker: | Thomas Hales Mellon Professor Department of Mathematics University of Pittsburgh |
| Title: | Formal Proofs in Geometry w/ HOL
|
| Abstract: |
HOL is a computer program that is used to give formal verifications of
theorems. This lecture will report on the experiences that I have had
with a version of HOL called HOL-Light. Particular attention will be
given to recent work, which has been focused on verifications about
topological spaces, metric spaces & Euclidean geometry.
|