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).
Rodzaj przedmiotu
Koordynatorzy przedmiotu
W cyklu 2023L: | W cyklu 2024L: |
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.
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: