Uniwersytet Warszawski - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Logika dla informatyków

Informacje ogólne

Kod przedmiotu: 1000-217bLOG Kod Erasmus / ISCED: 11.304 / (0612) Database and network design and administration
Nazwa przedmiotu: Logika dla informatyków
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty obowiązkowe dla I roku studiów 2 stopnia na kierunku informatyka
Punkty ECTS i inne: 6.00
Język prowadzenia: angielski
Rodzaj przedmiotu:

obowiązkowe

Skrócony opis:

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.

Pełny opis:

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

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.

Efekty uczenia się:

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

Zajęcia w cyklu "Semestr letni 2019/20" (zakończony)

Okres: 2020-02-17 - 2020-08-02
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Laboratorium, 15 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Lorenzo Clemente
Prowadzący grup: Jacek Chrząszcz, Lorenzo Clemente, Piotr Hofman, Jędrzej Kołodziejski, Daria Walukiewicz-Chrząszcz
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin

Zajęcia w cyklu "Semestr letni 2020/21" (jeszcze nie rozpoczęty)

Okres: 2021-02-22 - 2021-06-13
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Laboratorium, 15 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Lorenzo Clemente
Prowadzący grup: Jacek Chrząszcz, Lorenzo Clemente, Vincent Michielini, Paweł Parys, Daria Walukiewicz-Chrząszcz
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.