| 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. |