Seminars

3pm Thursday 26 February 2009, Seminar room M345
School of Mathematical Sciences Colloquium
Automated deduction and research mathematics
Petr Vojtechovsky, University of Denver

Automated deduction has improved substantially in the last 3 years or so, mainly due to new kinds of proof-searching methods that attempt to mimic what (some) humans do. Consequently, in several fields of mathematics, automated deduction has become a standard and often indispensable tool. I will review some of the new methods, give concrete examples of successes of automated deduction, show you typical proofs, and hopefully demonstrate automated deduction in real time. Is this mathematics? Should it be published? How? We will talk about that, too. By the way, I am a research mathematician, not a developer of automated deduction software, so this will not be a sales pitch.