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
News
(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!
Slides
| # | 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 |