Logika dla informatyków 1000-217bLOG
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).
Koordynatorzy przedmiotu
W cyklu 2023L: | W cyklu 2024L: |
Rodzaj przedmiotu
Efekty kształcenia
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].
Literatura
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.