On Wed 2013-11-13 and Wed 2013-11-20 I am giving a course on logic, proof and theorem proving to current PhD students. The following is my rough plan for the two sessions (each 1 hour long). Students are expected to read material beforehand.
* basic background http://www.paultaylor.eu/stable/prot.pdf Ch.s 1-5 (4 is slightly less important for theorem proving) http://en.wikipedia.org/wiki/Logical_connective http://en.wikipedia.org/wiki/Natural_deduction http://en.wikipedia.org/wiki/Sequent_calculus * intro to proof theory: http://plato.stanford.edu/entries/proof-theory-development/ * the system LJ: http://www.normalesup.org/~saurin/Enseignement/Proof_Theory_CMI/cours3.pdf
1st session =========== Connectives Propositional logic Meaning of propositional statements, truth tables Propositional proofs Two types of proof: ND, sequent calculus Quantifiers Meaning of statements involving quantifiers, models First-order proofs (ND, sequent calculus) System G3i The cut rule Proof and types
2nd session =========== Introduction to HOL Basic steps with HOL Simple proofs First-order automated proof Simplification Induction