Introduction

Recall of First-Order Logic

Standardization of Formulæ

Standardization of Interpretations

Herbrand's Theorem

Implementations of Herbrand's Theorem

Unification and Resolution

Resolution Strategies

SLD resolution

Extraction of Answers

Introduction to Logic Programming

Automated Theorem Proving