# 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 |