The International Conference on Automated Deduction


CADE is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974. Previous CADEs were mostly biennial, and annual conferences started in 1996. Since 2001 CADE has participated in the International Joint Conference on Automated Reasoning (IJCAR).

Future Conferences

The CADE/IJCAR Conference Management Notes and Schedule

Previous Conferences

Notes on the Early History of CADE

Wolfgang Bibel provided many details of the early CADEs, which have been integrated into the list above

Peter Andrews provided many details of the early CADEs. He noted ...

Evidently the conference at Versailles, France, in 1968 was not considered part of the CADE sequence of conferences by the early CADE organizers (one of whom was Wolfgang Bibel).

Gérard Huet recalls ...

CADE was created probably at the 1977 meeting. Retroactivally, the meetings of Argonne and Oberworlfach were christened CADE-1 and CADE-2, consistently with the fact that they were organized by the automated deduction community (Wos, Robinson, Bledsoe, Loveland, Andrews, Bibel, etc).

The 1968 meeting was organized by the mathematician Marcel-Paul Schützenberger, one of the founders of formal language theory, the logician Daniel Lacombe and the computer scientist Louis Nolin. It occurred at the just created IRIA (Institut de Recherche en Informatique et en Automatique) in Rocquencourt, near Versailles. This was actually the first scientific meeting organized at IRIA (to become INRIA in 1984 when it became a national institute). Schützenberger was the father of the Parisian school of theoretical computer science, and one of the founding scientific directors of IRIA. G. Kreisel came, probably invited by D. Lacombe, a specialist of recursive functions theory, and Jean-Louis Krivine, who had been working with him on axiomatic set theory. de Bruijn gave one of the first presentations of Automath. D. Scott discussed a notion of constructive validity. Several pioneers of automated theorem-proving participated, such as Hao Wang, R. Kowalski, D. Loveland, D. Luckham and L. Wos.