Ernest Schimmerling

Mathematical logic seminar - December 2, 2004

Time: 12 - 1:20 p.m.

Room: BH 150

Speaker: Sean McLaughlin
Graduate Student in Computer Science
Carnegie Mellon University

Title: An Introduction to Quantifier Elimination

Abstract:     In theorem proving, decision procedures are a practical necessity. Quantifier elimination methods are a rich and interesting class of decision procedures. In this talk, I give an introduction to the theory of quantifier elimination and survey some particularly beautiful algorithms, including procedures for deciding linear arithmetic, algebraically closed fields, and real closed fields. Implementations of some of these examples will be demonstrated with the interactive theorem prover HOL-Light.