|Time:|| 12 - 1:20 p.m.
|Speaker:|| Sean McLaughlin
Graduate Student in Computer Science
Carnegie Mellon University
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.|