|
Schedule
Lectures: 13:45-15:30, room 174
Practica: 13:45-15:30 room 174 |
Goal
This course gives an introduction to the field of mathematical logic by presenting the syntax and semantics of propositional logic and of the richer language of predicate logic. The goal is to describe and investigate the above logics by finitary methods, and to train students in formalizing specifications and in verifying properties of systems.
Description
Originally logic was used by the Greek Sophists to demonstrate the correctness of their argument in formal debates. The ambiguity of human languages asked for formulation of logic in a symbolic formal language.
Only towards the end of the 19th century logic has been formulated in the language of mathematics, and in particular of algebra, making it a useful tool to solve mathematical problems. In the same period the language used to prove theorems from mathematics begun suffering the same problems of natural language, showing many paradoxes. Logic was proposed as the foundational language of mathematics, but several limitation where soon discovered.
More recently logic has become the language of computer science, just as calculus is the language of many engineering discipline. In this course we will study propositional and predicate logic, their proof theory, their limitation, as well as some of their applications in computer science.
Literature
Schedule Lectures
| Nun | Date | Topic | Reading | Extra |
| 1a | 10 Feb |
Overview + history of logic | [V03] | slides |
| 1b |
The language of propositional logic (PL) |
[HR04]:1.1, 1.3 |
||
| 2a |
17 Feb |
Semantics of propositional logic |
[HR04]:1.4.1 |
|
| 2b |
Mathematical induction |
[HR04]:1.4.2 |
||
| 22 Feb |
HOMEWORK 1 - Exercises 1.4: 2b, 2d, 7a |
Solutions |
||
| 3 |
24 Feb |
Natural deduction (until rules for implication) |
[HR04]:1.2.1 |
|
| 4 |
2 Mrt |
Natural deduction |
[HR04]:1.2 |
|
| 7 Mrt |
HOMEWORK 2 - Exercises 1.2: 1p, 2f, 5c |
Solutions |
||
| 5 |
9 Mrt |
Soundness and completeness of PL |
[HR04]:1.4.3-4 |
|
| 6 |
16 Mrt |
Validity and Conjunctive normal form |
[HR04]:1.5.1-2 |
|
| 7 |
23 Mrt |
Horn Formulas and Sat solvers |
[HR04]:1.5.3, 1.6 |
|
| 23 Mrt |
HOMEWORK 3 - Exercises 1.5: 7c,12,15b |
Solutions |
||
| 8 |
13 Apr |
Predicate logic (FOL) |
[HR04]:2.1, 2.2 |
|
| 13 Apr |
HOMEWORK 4 - Exercises 2.1:2 + 2.2: 1a, 5d | Deadline 25 Apr |
Solutions |
|
| 9 |
20 Apr |
Natural deduction for FOL |
[HR04]:2.3 |
|
| 10 |
4 May |
Semantics of FOL |
[HR04]:2.4 |
|
| !!! |
4 May |
HOMEWORK 5 - Exercises 2.3:6b, 7b, 9p |
Deadline 16 May |
!!! |
| 11 |
11 May |
Undecidability of FOL |
[HR04]:2.5 |
|
| 12 |
25 May |
Expressivity of FOL |
Bibliography
[HR04] Michael R. A. Huth and Mark D. Ryan Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
[V03] Moshe Vardi A Brief History of Logic, 2003.
Exam and Homework information
- Examination is worth 70% of the grade. The remaining 30% is from the homeworks.
- Return homework solutions either in my mail box, or by e-mail to Joost Winter
- Deadline is on Wednesday one week after the homework has been given. Bring your solution before the start of the lesson (13:45) at latest.
- After the deadline, but before Friday 16:00 o' clock, the homework grade is diminished by 25%.
- After Friday 16:00 solutions to the homework are no longer accepted.
- Solutions and grades can be found here.
Past Examinations
- 13 May 2011 (trial)
- 7 June 2011 (Solutions here, here and here) and 12 August 2011