Course in the winter semester 2002/03 - within the MMISS project
Lecture: Mon 13--15h, MZH 1400
Exercises: Thu 10-12h (group 1) and 17-19h (group 2), P2 (computer pool in the 0th floor)
Start: Mon 21st Oct 2002 and Thu 24th Oct 2002
Attention! The following exercises are cancelled: 23.01., 30.01. und 06.02.
Instead: Thu 20.02., 6., 13., 27. 03. 15-17h in P2 time has changed!!!!
Please fill out evaluation form (in German)!
Logic is used in computer science at many places. It is needed when something (e.g. programs, languages, graphs, networks, agents, ...) shall be described formally in its properties. Based on such logical descriptions it is then also possible to do proofs (besides the proofs that you know from the mathematics, also e.g. program or protocol verification is possible). In addition, one can program even in logic directly (Prolog), and this in a very problem-oriented manner.
This lecture introduces first-order predicate logic, which is basic in many respects. Topics are: propositional and predicate logic, logical formalization, logical inference, games for finding out truth values, what is a proof?, proof calculus, soundness, completeness, computer science applications (program verification, Prolog).
The lecture will be based on the book "Language, Proof, and Logic'' by Jon Barwise und John Etchemendy (CSLI Stanford). It is didactically very well written, and moreover comes with a CD containing four programs. These programs allow students to do exercises with their computers. Furthermore, there is a server in Stanford that automatically gives direct feedback to the solutions. The book and the software have been used very successfully at a lot of universities (both nationally and internationally). While the book is written in English, the lecture will be in German.
Local information about the book and the software (only locally accessible!)
Proofs in fitch General help with the LPL software
Slides for the lecture
English literature German literature German slides about Language, proof and logic more slides