Logika i teoria obliczeń
Informacje ogólne
Kod przedmiotu: | 1000-2D08LTO |
Kod Erasmus / ISCED: |
11.304
|
Nazwa przedmiotu: | Logika i teoria obliczeń |
Jednostka: | Wydział Matematyki, Informatyki i Mechaniki |
Grupy: |
Seminaria magisterskie na informatyce |
Punkty ECTS i inne: |
(brak)
|
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 uczenia się: |
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 zaliczenia seminarium jest staranne przygotowanie i wygłoszenie przynajmniej jednego referatu w semestrze oraz -- w zależności od roku -- zatwierdzenie tematu pracy magisterskiej lib złożenie pracy. |
Właścicielem praw autorskich jest Uniwersytet Warszawski.