Course Notes on First Order Logic

This node contains two installments of the notes describing basic results on first order logic. The first gives the basic syntax and sematics of the language. It gives a complete set of inference rules derived from general rules given in the installment on semantics. It proves the compactness theorem from the completeness theorem for the given rule set. There are many problems at the end of the installment which give applications of the compactness theorem. The second installment contained here gives the basic results of resolution theorem proving.

postscript for first order logic.

postscript for resolution theorem proving.

The course no longer follows these notes very closely. Lectures now start with the syntax and semantics. They then explain Skolem normal form and clausal normal form for fist order theories. They then given Herbrand's theorem, making an explicit analogy with the free graph theorem for STRIPS planning given in the installment on graph search and STRIPS planning. After presenting Herbrand's theorem we prove the completeness of Robinson's binary resolution rule (with factoring treated as a seperate rule). It is then shown how the completeness of resolution implies the compactness theorem. The importance of the compactness theorem in establishing the expressive weakness of first order logic is emphasized.