Automated Deduction CADE-22

This volume contains the proceedings of the 22nd International Conference on Automated Deduction (CADE-22). The conference was hosted by the School of Computer Science at McGill University, Montreal, Canada, during August 2-7, 2009. CADE is the major forum for the presentation of research in all aspects of automated deduction. Within this general topic the conference is devoted to foundations, applications, implementations and practical experiences. CADE was founded in 1974 when it was held in Argonne, USA. Since then CADE has been organized ?rst on a bi-annual basis mostly and since 1996 on an annual basis, in 2001, 2004, 2004, 2006 and 2008 as a constituent of IJCAR. This year the Program Committee selected 32 technical contributions out of 77 initial submissions. Of the selected papers 27 were regular papers and 5 were system papers. Each paper was refereed by at least three reviewers on its sign- icance, technical quality, originality, quality of presentation and relevance to the conference. The refereeing process and the Program Committee meeting were conducted electronically via the Internet using the EasyChair conference m- agement system. The program included three invited lectures by distinguished experts in the area: Instantiation-Based Automated Reasoning: From Theory to Practice by Konstantin Korovin(The Universityof Manchester,UK),Integrated Reasoning and Proof Choice Point Selection in the Jahob System: Mechanisms for Program Survival by Martin Rinard (Massachusetts Institute of Technology, USA),and Building Theorem Provers byMarkStickel(SRIInternational,USA).