Lecturer: Chris Fermüller.
This course will be held in English.
Contents:
Basic knowledge about classical propositional and first-order logic as covered, e.g., in "Theoretische Informatik und Logik".
TEST YOURSELF whether you are fit for this course:
You should be able to prove without handwaving (and
preferably without consulting any book or notes)
that (forall x) (exists y) P(x,y) is a logical consequence of
(exists x) (forall y) P(y,x), and to (rigorously) show that
the converse does not hold.
In particular you should be able to present a formal definition
of the (logical) consequence relation and of a (formal)
model/interpretation of a classical first-order formula.
The course will take place in slightly blocked form on 9 or 10 Mondays.
Various course material - in particular copies of the lecture slides, including the homework problems ('exercises') - will be made available here (and/or in the lecture) to all participants.
I strongly recommend the use of LaTeX.
Useful style files are available from
Latex for Logicians.
For drawing graphs and automata - and thus also Kripke models -
the LaTeX package
VauCanSon-G should be useful. More options for automata/graph drawing
with LaTeX can be found at MET - Automata in LaTeX.
Also the TeX/LaTeX extension PGF/TikZ is well worth exploring.
Include the problem statement, its number (`Exercise X: ... ') and your name in the submitted solution files. Send corresponding (uncompressed) PDF files via email to Chris Fermüller using "NCL exercises" as subject line.
The evaluation will be based on the amount and quality of submitted solutions to the exercises (as assigned during the course).