Ernest Schimmerling

Mathematical logic seminar - April 6, 2004

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.