en | de



VO2  WS 2007/2008  703501

Lecture Notes

Lecture notes for the full course are now available: pdf (last updated 13 May 2008)


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).