Serwisy internetowe Uniwersytetu Warszawskiego | USOSownia - uniwersyteckie forum USOSoweNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Logika i teoria obliczeń

Informacje ogólne

Kod przedmiotu: 1000-2D08LTO Kod Erasmus / ISCED: 11.304 / (0612) Database and network design and administration
Nazwa przedmiotu: Logika i teoria obliczeń
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Seminaria magisterskie na informatyce
Punkty ECTS i inne: 6.00 LUB 4.00 (zmienne w czasie)
zobacz reguły punktacji
Język prowadzenia: angielski
Rodzaj przedmiotu:

seminaria magisterskie

Skrócony opis:

Od automatów skończonych do rozgrywek na dowolnych grafach, od czasu stałego do nieelementarnego, od logiki klasycznej do logik temporalnych opisujących własności złożonych systemów. Tematyka seminarium obejmuje szeroki krąg problemów współczesnej informatyki teoretycznej. Prace magisterskie często rozwiązują nietrywialne problemy matematyczne lub dają kompetentny przegląd jakiejś nowej dziedziny; możliwe są także prace implementacyjne (np. symulacje gier).

Pełny opis:

Tradycyjnie, logika zajmowała się prawami myślenia. Współcześnie, informatyka stwarza możliwości przetwarzania informacji na wielką skalę również poza umysłem człowieka. Nic więc dziwnego, że rozwój informatyki stawia przed logiką nowe wyzwania i fascynujące problemy. Spośród wielu możliwości, wybraliśmy następujące zagadnienia.

Teoria złożoności klasyfikuje problemy obliczeniowe ze względu na zasoby potrzebne do ich realizacji, takie jak czas i pamieć przy klasycznych obliczeniach sekwencyjnych, ale także liczba procesorów przy obliczeniach równoległych lub liczba bitów losowych w obliczeniach zrandomizowanych. Złożoność obliczeniowa jest przesłanką bezpieczeństwa w kryptografii asymetrycznej, pomimo że wiekszość jej hipotez pozostaje nieudowodniona, stanowiąc wyzwanie dla matematyki. Pomostem pomiędzy teorią złożoności a logiką jest tzw. teoria złożoności opisowej: pytania o zależności między różnymi klasami złożoności (jak np. P, NP, PSPACE) sprowadzają się w niej do pytań o równoważnosć różnych logik, przeważnie rozszerzeń logiki pierwszego rzędu o różnego rodzaju operatory punktu stałego.

Matematyczna weryfikacja programów. W wielu zastosowaniach od niezawodności działania oprogramowania, a także sprzętu (np. mikroprocesorów) zależą znaczne wartości ekonomiczne, a czasem nawet życie ludzi. W krytycznych zastosowaniach nie można polegać na serii testów -- poszukuje się pewniejszych metod. Jedną z nich jest budowanie matematycznego modelu wszystkich możliwych stanów systemu i sprawdzanie własności tego modelu metodami automatycznymi. Zadaniem logiki jest tu precyzyjne wyrażenie własności poprawności. Użytecznym modelem zachowania systemu jest gra o potencjalnie nieskończonym czasie trwania, w której gracz ,,system'' gra z graczem ,,środowisko''. Matematyczna weryfikacja używa szerokiej gamy metod, od logiki temporalnej i logik stałopunktowych, po elementy teorii automatów, a także teorii gier.

Klasyczna teoria automatów. Mimo, że teoria automatów rozwija się od początku istnienia informatyki, niektóre klasyczne problemy do tej pory pozostają nierozwiązane, a wciąż pojawiają się nowe. Weźmy dla przykładu wyrażenia regularne: czy istnieje język regularny, którego nie można opisać wyrażeniem regularnym bez zagnieżdżonej gwiazdki (ale z dopełnieniem)? Jest to do dziś ptytanie otwarte. Na seminarium będziemy badać podobne pytania dotyczące języków regularnych skończonych słów, a także modele bardziej ogólne, jak automaty na skończonych lub nieskończonych drzewach.

Literatura:

Współczesna literatura z tej dziedziny, w tym czasopisma naukowe i dane z Internetu. Szczegóły przedstawią prowadzący na pierwszych zajęciach.

Efekty kształcenia:

Wiedza.

Poznaje wybrane problemy badawcze z głównego nurtu aktualnych badań naukowych w dziedzinie logicznych podstaw informatyki. Podejmuje własne badania, jakie staną się podstawą pracy magisterskiej.

Umiejętności.

1. Potrafi czytać ze zrozumieniem artykuły naukowe.

2. Potrafi komunikować innym wyniki naukowe w zrozumiały i atrakcyjny sposób.

3. Potrafi słuchać w sposób krytyczny i zadawać pytania innym referującym.

Kompetencje.

Zyskuje wiedzę na temat metodologii badań naukowych w dziedzinie logiki informatyce. Zyskuje ogólne rozeznanie w sprawie miejsc publikacji i ich prestiżu naukowego.

Metody i kryteria oceniania:

Warunkiem zalczenia seminarium jest staranne przygotowanie i wygłoszenie przynajmniej jednego refeartu w semestrze oraz -- w zależności od roku -- zatwierdzenie tematu pracy magisterskiej lib złożenie pracy.

Zajęcia w cyklu "Rok akademicki 2018/19" (zakończony)

Okres: 2018-10-01 - 2019-06-08
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Seminarium magisterskie, 60 godzin więcej informacji
Koordynatorzy: Sławomir Lasota, Damian Niwiński
Prowadzący grup: Sławomir Lasota, Damian Niwiński
Lista studentów: (nie masz dostępu)
Zaliczenie: Zaliczenie

Zajęcia w cyklu "Rok akademicki 2019/20" (w trakcie)

Okres: 2019-10-01 - 2020-06-10
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Seminarium magisterskie, 60 godzin więcej informacji
Koordynatorzy: Sławomir Lasota, Damian Niwiński
Prowadzący grup: Sławomir Lasota, Paweł Parys, Szymon Toruńczyk
Lista studentów: (nie masz dostępu)
Zaliczenie: Zaliczenie
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.