The course will follow to a large extent the course notes from Frank Pfenning on Constructive Logic(CL) and on Automated Theorem proving(ATP). Both course notes are available in pdf-format. We will post more detailled notes on WebCT.
The QED Manifesto, appeared in "Automated Deduction - CADE 12", Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994.