**DATE: Tuesday, December 2****TIME: 11:30 AM****DURATION: 3 hours****ROOM: ARC 108****YOU WILL BE ALLOWED TO USE ONE 8.5"x11" TWO-SIDED FORMULA SHEET****OFFICE HOURS:**Mon(Dec.1) 2-3

- Equivalence; Adequate systems of connectives (2.4)
- Semantic tableaux; Gentzen proof system (2.6,3.2)
- Hilbert proof system (3.3)
- CNF; Resolution (4.1)

- Interpretations, satisfiability and validity (5.3)
- Equivalence (5.4)
- Semantic tableaux (5.5)

- Gentzen proof system (6.1)
- Hilbert proof system (6.2)

- Functions and terms (7.1)
- Clausal form (7.2)
- Herbrand models (7.3)
- Ground resolution (7.5)
- Substitution (7.6)
- Unification (7.7)
- General resolution (7.8)
- SLD-resolution (8.2)

**NOTE: the final exam will emphasize the material covered after the midterm (Chapters 5-8).
Roughly 2/3 of the exam (or more) will be based on the content of these chapters. **

Back to MTH714 homepage.