Automaty a logika
Informacje ogólne
Kod przedmiotu: | 1000-2M17AL |
Kod Erasmus / ISCED: |
11.3
|
Nazwa przedmiotu: | Automaty a logika |
Jednostka: | Wydział Matematyki, Informatyki i Mechaniki |
Grupy: |
Przedmioty obieralne dla informatyki Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka |
Punkty ECTS i inne: |
(brak)
|
Język prowadzenia: | angielski |
Rodzaj przedmiotu: | monograficzne |
Skrócony opis: |
Tematem wykładu są związki teorii automatów z logiką, u których podstaw leży twierdzenie Buchiego: zbiór słów jest językiem regularnym wtedy i tylko wtedy gdy da się go opisać w logice monadycznej drugiego rzędu. Omówione zostaną uogólnienia tego twierdzenia, dla automatów działających na słowach i drzewach, zarówno skończonych jak i nieskończonych. Kulminacją wykładu będzie twierdzenie Rabina o rozstrzygalności teorii monadycznej nieskończonego drzewa binarnego. Jest to kontynuacja wykładu prof. Bojańczyka prowadzonego w roku akademickim 2009/2010. |
Pełny opis: |
1.Twierdzenia Buchiego o logicznej charakteryzacji języków regularnych . Przypadki słów skończonych i nieskończonych (2-3 wykłady). 2.Własności automatów na słowach nieskończonych: determinizacja, automaty alternujące (2 wykłady). 3.Automaty na drzewach skończonych. (2-3 wykłady). 4.Automaty na drzewach nieskończonych, twierdzenie Rabina o logice monadycznej na drzewie nieskończonym. Gry z warunkiem parzystości. (3-4 wykłady). 5.Zagadnienia uzupełniające: związki z deskryptywną teorią mnogości, charakteryzacje podklas języków regularnych, problemy syntezy (3 wykłady). |
Literatura: |
1. Wolfgang Thomas, Languages, Automata and Logic, w Handbook of Formal Languages III, Springer. 2. E. Grädel, W. Thomas, and Th. Wilke, Automata, logics, and infinite games, Springer 2002, |
Efekty uczenia się: |
W szczególności student: 1. Rozumie problematykę rozstrzygalności logik na strukturach skończonych i nieskończonych. 2. Zna podstawowe zależności pomiędzy modelami automatów, a logikami. 3. Zna ograniczenia siły wyrazu logik. 4. Umie wykazać nierozstrzygalność, lub obliczeniową trudność pewnych problemów. |
Metody i kryteria oceniania: |
Ocena końcowa na podstawie punktów z egzaminu pisemnego lub ustnego i zadań domowych. Wagi poszczególnych składników: egzamin - 50%, zadania - 50%. W sesji poprawkowej obowiązują takie same zasady jak w pierwszym terminie. |
Właścicielem praw autorskich jest Uniwersytet Warszawski.