Logika dla informatyków

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).

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].