Logika i teoria obliczeń (sem. mono. wspólnie z 1000-2D08LTO) 1000-1S16LTO
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.
Rodzaj przedmiotu
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.
Kryteria oceniania
Warunkiem zaliczenia seminarium jest staranne przygotowanie i wygłoszenie przynajmniej jednego referatu w semestrze.
Literatura
Współczesna literatura z tej dziedziny, w tym czasopisma naukowe i dane z Internetu. Szczegóły przedstawią prowadzący na pierwszych zajęciach.
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: