Lecture Notes
Lecture notes for the full course are now available:
pdf (last updated 13 May 2008)
Schedule
January 24
Exam. See the
exams page.
January 17
Discussion of exercises.
January 10
Application of compactness, first-order logic with equality, paramodulation, second-order logic.
December 13
Unification, full first-order resolution.
December 6
Theorem of Löwenheim-Skolem for infinite universes, first-order compactness, soundness and completeness of ground resolution.
November 29
Prenex and Skolem form, Herbrand interpretation. Herbrand models are sufficient to characterise satisfiability of sentences in Skolem form.
November 22
Semantics of first-order logic.
November 15
First-order modelling, natural deduction.
November 9
Completeness of resolution, syntax of first-order logic, substitution.
October 25
Propositional modelling, soundness of resolution, semantic trees.
October 18
Isabelle, propositional modelling.
Please note that Isabelle only runs on
zid-gpl.uibk.ac.at. Use
ssh zid-gpl.uibk.ac.at to log onto this machine from other terminals.
October 11
Propositional logic (semantics, resolution).
October 4
Introduction, propositional logic (syntax, natural deduction).