Computer Science Colloquium

A Set-Theoretically Oriented Proof Verifier

Jack Schwartz
Courant Institute, NYU

Friday, December 3, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Hosts:

Zvi Kedem kedem@cs.nyu.edu, (212) 998-3101

Abstract

This talk, representing joint work with Eugenio Omodeo and Domenico Cantone over the past decade, will describe the syntax, semantics, and structure of a set-theoretically oriented proof verifier, tentatively named 'Referee', which, though still not quite complete, has substantial functionality, and has already been used to verify about 600 fundamental theorems of set theory and analysis. The whole foundational part of analysis up to the construction of real numbers (currently in progress) has been verified. The algorithmic core of the verifier incorporates various decision algorithms for fragments of set theory developed at NYU over this period, which help to attain a substantial degree of expressive efficiency. The way in which these decision algorithms are extended and optimized to fit the for practical application will be described.