Lecturer: Agata Ciabattoni
The aim of this course is to describe some major results of mathematical logic and mention (some of) their connections to computer science. To this end the following topics will be presented:
Introduction to Propositional (Classical) Logic: Syntax and Semantics, Functional Completeness of connectives, Normal forms.
(Course's notes written by a former student).
Compactness theorem.
Hints on P and NP Problems , Turing Machines . Proof of Cook's theorem . (see Cook's original paper ).
Lukasiewicz logic and Ulam's game (D. Mundici's paper here ).
( Here some notes on Lukasiewicz logic and the proof of the Compactness theorem written by a former student). My slides .
Introduction to Intuitionistic Logic (see e.g. here for some introductory pages or here for a good on-line book) and Kripke Models . Introduction to Deductive Systems. My slides .
Introduction to Natural Deduction and Axiomatic Systems. Equivalence between the two formalisms. My slides .
(Course's notes written by a former student: T. Krennwallner)
Introduction to Sequent Calculus. Calculi LJ, LK and LK'. Soundness and Completeness. My slides .
(Course's notes written by a former student)
Equivalence of Axiomatic Systems and Sequent calculus. Use of LK' for finding a formula in CNF equivalent to a given formula (cf. Theorem 3.4.2 in Gallier's book). Cut-elimination Theorem for LJ a la Gentzen (see e.g. Section 3.1 here ). Hints on Linear Logic . My slides .
Lecture on Friday 03.12.2010 :
Syntax and semantics of (classical) first-order logic. Equivalences. Prenex normal form. Skolem form. My slides .
Herbrand Theorem (see here for my slides).
Sequent calculi for first order classical an intuitionistic logic. Soundness and Completeness for LK'. Some slides . One example of test.