The course consists of the following topics: (1) Automated theorem proving for
first-order logic using resolution and superposition. (2) Automated theorem
proving in propositional logic. (3) Interactive theorem proving in higher-
order logic, using Isabelle. (4) Logics with partial functions.
1. For theorem proving in first-order logic, the most succesful technique is resolution, combined with superposition. I discuss the clausal normal form, the transformation to clausal normal form, and the reasoning rules.
2. Next topic is DPLL with Conflict-Driven Clause Learning. We apply it to toy examples, and to circuit verification. In the last 15 years, very big progress has been made in propositional theorem proving, and big propositional formulas can now be verified in reasonable time.
3. If one wants to verify a mathematical theory, or prove a functional program correct one needs higher-order logic, for induction and for the definition of recursive functions. Isabelle is probably the interactive prover that is used most often. It is not based on ideology, but on effectiveness. If you want some theory verified in shortest possible time, Isabelle is the right choice.
4. I explain PCL (Partial Classical Logic), and how I expect that it can be used in interactive verification.
