Introduction

Recall of First-Order Logic, part 1

Recall of First-Order Logic, part 2

Recall of First-Order Logic, not to forget

exercises

Standardization of Formulæ

Off-Topic Notes

exercises

Standardization of Interpretations

exercises

Herbrand's Theorem

exercises

Implementations of Herbrand's Theorem

exercises

Unification and Resolution

exercises

Resolution Strategies

Automated Theorem Proving

exercises

Extraction of Answers

SLD resolution

Introduction to Logic Programming