Material for the course Automated Theorem Proving at Carnegie Mellon University, Fall 1999, revised Spring 2004. This includes revised excerpts from the course notes on Linear Logic (Spring 1998) and Computation and Deduction (Spring 1997). Material