- First-order logic: syntax and semantics (recall)
- Standardization of formulae
- Herbrand universe, Herbrand base, Herbrand interpretations
- Automatic proof techniques
- Theory: semantic trees, Herbrand's
theorem
- Ground methods: Gilmore, Davis-Putnam,
Robinson's resolution
- Resolution with unification
- Resolution strategies
- Extra (1): automated theorem proving
- Implementations
- Applications
- Extra (2): towards logic programming
- Horn clauses, SLD resolution, logic
programs
- Applications