Schedule

Overall, as things stand now, our progression will look like this:

1. complete ``mini" coverage of first-order logic (and what it presupposes, e.g., naive set theory); Hyperproof and OTTER used
2. introduction clausal logic; OTTER used
3. more detailed introduction to OTTER
4. quick introduction to Common Lisp
5. puzzles and problems in OTTER (lots!)
6. Story Generation via LP (BRUTUS )
7. How smart can theorem provers get? -- an examination of the possibility of an automated theorem prover proving Gödel's incompleteness theorems

Exact reading assignments and test dates etc. will be given in class and on the course web page as we progress.