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 i zastosowania w informatyce. Inne logiki ważne w informatyce.

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

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.

Efekty uczenia się:

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

Zajęcia w cyklu "Semestr letni 2018/19" (zakończony)

Okres: 2019-02-16 - 2019-06-08
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Jerzy Tyszkiewicz
Prowadzący grup: Tomasz Gogacz, Jerzy Tyszkiewicz
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin

Zajęcia w cyklu "Semestr letni 2019/20" (w trakcie)

Okres: 2020-02-17 - 2020-06-10
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Jerzy Tyszkiewicz
Prowadzący grup: Jerzy Tyszkiewicz
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.