Logika dla informatyków

obowiązkowe

Wprowadzenie do logiki zdaniowej i logiki pierwszego rzędu: elementy teorii modeli, elementy teorii dowodu, rola w

informatyce. Inne logiki ważne w informatyce.

Przedmiot ma dwa warianty. W pierwszym z nich zajęcia mają charakter bardziej praktyczny i prowadzone są wraz z

laboratorium, w drugim – zajęcia mają pogłębiony charakter teoretyczny.

1. Logika zdaniowa: związki z obwodami logicznymi; systemy dowodowe; zdaniowa logika intuicjonistyczna

2. Zastosowania logiki zdaniowej: SAT-solvery.

3. Logika pierwszego rzędu: sposób użycia; związki z bazami danych (tw. Codda); ograniczenia siły wyrazu (gry

Ehrenfeuchta-Fraisse); systemy dowodzenia; twierdzenie o pełności;

4. Klasyczna teoria modeli: twierdzenie o zwartości, twierdzenie Skolema-Löwenheima.

5. Rozstrzygalność teorii logicznych: nierozstrzygalność logiki pierwszego rzędu; rozstrzygalne fragmenty.

6. Arytmetyka i twierdzenie Gödla o niezupełności.

7. Datalog, czyli rozszerzenie logiki pierwszego rzędu o rekurencję.

8. Logika w weryfikacji: SPIN, Coq, provery.

9. Logika 2 rzędu: SO, MSO i związki z automatami, rozstrzygalność, zastosowania (np. MONA).

1. Punkty 1, 3, 4, 5, 6: Skrypt http://www.mimuw.edu.pl/~urzy/calosc.pdf

2. Punkty 2, 7, 8, 9: Slajdy do wykładu.

Wiedza: absolwent zna i rozumie

* w pogłębionym stopniu - wiedzę z działów matematyki niezbędnych do studiowania informatyki (logika i jej związki

z informatyką, teoria złożoności) [K_W01],

* w pogłębionym stopniu - rolę i znaczenie konstrukcji rozumowań matematycznych [K_W02].

Umiejętności: absolwent potrafi

* konstruować rozumowania matematyczne [K_U01],

* wyrażać problemy obliczeniowe w języku matematyki [K_U02],

* analizować pojęcia sformalizowane w wybranych systemach logicznych o znaczeniu informatycznym, tworzyć w

nich formalizacje zadanych pojęć bądź też dowodzić niemożności takiej formalizacji [K_U07].