Using Herbrand's theorem to reduce first-order logic problems to propositional logic:

• Quiz question for invariants containing relations
• Set-Valued Fields Paper

Compactness Theorem for Propositional Logic

Semidecision Procedure for First-Order Logic (without Equality)

Definition of Propositional Resolution

Deriving Propositional Resolution

Continued in Lecture 12