LASER Summer School Course

General Information

This course gives an introduction to first-order automated reasoning and the use of the first-order theorem prover Vampire. The course was given at the 8th LASER Summer School on Software Engineering


(06/09/2011, evening) Sections 4-7 were added.
(06/09/2011) Slides were improved and re-organised by the subject. Sections 1-3 were added.
(04/09/2011) This page was created!


# subject slides
1 Introduction slides
2 First-Order Logic and TPTP slides
3 Inference Systems slides
4 Saturation Algorithms slides
5 Redundancy Elimination slides
6 Equality Reasoning slides
7 Unification and Lifting slides
8 Colored Proofs, Interpolation and Symbol Elimination slides
9 From Theory to Practice slides
10 Sorts and Theories slides
11 Satisfiability Checking slides
12 Cookies slides