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-Loewenheima.
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 systemów sekwencyjnych i współbieżnych: SPIN, Coq, provery.
9. Logika 2 rzędu: SO, MSO i związki z automatami, rozstrzygalność, zastosowania (np. MONA).
Rodzaj przedmiotu
Efekty kształcenia
Wiedza
1. Ma uporządkowaną wiedzę w zakresie składni i semantyki logiki pierwszego rzędu (K_W01, K_W02).
2. Zna najważniejsze własności logiki pierwszego rzędu (K_W01, K_W02).
3. Ma podstawową wiedzę w zakresie składni i semantyki co najmniej jednej logiki o znaczeniu informatycznym, innej niż logika pierwszego rzędu (K_W01, K_W02).
4. Zna podstawowe własności co najmniej jednej logiki o znaczeniu informatycznym, innej niż logika pierwszego rzędu (K_W01, K_W02).
5. Ma ogólną wiedzę na temat różnych formalizmów logicznych stosowanych w informatyce (K_W01, K_W02).
6. Dobrze rozumie rolę i znaczenie konstrukcji rozumowań matematycznych (K_W01, K_W02).
Umiejętności
1. Potrafi formalizować zadane własności w logice pierwszego rzędu (K_U09).
2. Potrafi udowodnić o zadanych własnościach, że nie są formalizowalne w logice pierwszego rzędu (K_U09).
3. Potrafi formalizować zadane proste własności, dla co najmniej jednej logiki o znaczeniu informatycznym, innej niż logika pierwszego rzędu (K_U10).
4. Potrafi udowodnić o zadanych prostych własnościach, że nie są formalizowalne. dla co najmniej jednej logiki o znaczeniu informatycznym, innej niż logika pierwszego rzędu
(K_U10).
Kompetencje
1. Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia, w tym zdobywania wiedzy pozadziedzinowej (K_K01).
2. Potrafi precyzyjnie formułować pytania, służące pogłębieniu własnego zrozumienia danego tematu lub odnalezieniu brakujących elementów rozumowania (K_K02).
Kryteria oceniania
Wynik ćwiczeń: decyduje suma punktów za zadania domowe i wynik nieobowiązkowego kolokwium; same zadania wystarczają do uzyskania maksymalnej oceny.
Wynik egzaminu: suma punktów za rozwiązania zadań
Wynik końcowy: suma ważona wyniku ćwiczeń i wyniku egzaminu
Literatura
Punkty 1, 3, 4, 5, 6: Skrypt http://www.mimuw.edu.pl/~urzy/calosc.pdf
Punkty 2, 7, 8, 9: Slajdy do wykładu.
Więcej informacji
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: