# Lectures 13 and 13a: Resolution Marathon

## Propositional Resolution

## Herbrand Theorem

Normal Forms for First-Order Logic

Preliminary Discussion on Models

Semidecision Procedure for First-Order Logic (without Equality)

Instantiation plus Ground Resolution

Non-Ground Instantiation and Resolution

## Decidability Questions

## References

- Slides for the course "Logic for Computer Science", Summer 2002, held by Harald Ganzinger (see chapter 1.7 onward)
- Handbook of Practical Logic and Automated Reasoning, Chapter 3