Departament de Llenguatges i
Sistemes Informàtics
Universitat Politècnica
de Catalunya
11am Friday 20th September 2002
Room 2511, JCMB, King's Buildings
The purpose of this talk is to discuss the motivations and goals of a branch of the research in propositional proof complexity called Automatization. Our goal is to introduce the concept for the non-expert audience, and argue its potential usefulness in the rigorous analysis of SAT-heuristics. We also overview some of the positive and negative results, and discuss its connection with interpolation theorems and consistency proofs.