Logika dla informatyków: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Poprawki edytorskie |
m Poprawki edytorskie |
||
| Linia 25: | Linia 25: | ||
=== Zawartość === | === Zawartość === | ||
* Rachunek | * Rachunek zdań. | ||
** | ** Składnia formul i semantyka zerojedynkowa. | ||
** Wzajemna | ** Wzajemna wyrażalność spójników, funkcjonalna zupełność. | ||
** | ** Postać normalna formuły tautologii. | ||
** | ** Siła wyrazu logiki zdaniowej. | ||
** Informacja o SAT-solverach | ** Informacja o SAT-solverach | ||
* Logika pierwszego | * Logika pierwszego rzędu - cz.1: definicje | ||
** | ** Formuły, zmienne wolne i związane. | ||
** | ** Spełnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego. | ||
** Podstawienie i jego sens semantyczny. | ** Podstawienie i jego sens semantyczny. | ||
* Logika pierwszego | * Logika pierwszego rzędu - cz. 2: sposób użycia | ||
** Dyskusja | ** Dyskusja ważnych tautologii logiki pierwszego rzędu. | ||
** Preneksowa | ** Preneksowa postać normalna i jej zastosowania | ||
** Logika formalna a zdania | ** Logika formalna a zdania języka naturalnego. | ||
* Logika pierwszego | * Logika pierwszego rzędu - cz. 3: ograniczenia | ||
** | ** Nierozstrzygalność logiki pierwszego rzędu. | ||
** Elementarna | ** Elementarna równoważność struktur. | ||
** Gry Ehrenfeuchta-Fraissego. | ** Gry Ehrenfeuchta-Fraissego. | ||
* Paradygmaty dowodzenia: | * Paradygmaty dowodzenia: | ||
** styl Hilberta | ** styl Hilberta | ||
** naturalna dedukcja, | ** naturalna dedukcja, | ||
** rachunek | ** rachunek sekwentów. | ||
** Informacja o | ** Informacja o informatycznych systemach dowodzenia | ||
* Twierdzenie o | * Twierdzenie o pełności dla rachunku zdań. | ||
* Twierdzenie o | * Twierdzenie o pełności dla rachunku predykatów. | ||
* Teoria modeli | * Teoria modeli | ||
** Twierdzenie o | ** Twierdzenie o zwartości i zastosowania | ||
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki. | ** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki. | ||
* Arytmetyka i tw. o | * Arytmetyka i tw. o niezupełności Goedla. | ||
* Logiki | * Logiki programów | ||
** Składnia PDL | ** Składnia PDL | ||
** Twierdzenie o małym modelu dla PDL | ** Twierdzenie o małym modelu dla PDL | ||
** Twierdzenie o pełności dla PDL | ** Twierdzenie o pełności dla PDL | ||
* Logika intuicjonistyczna | * Logika intuicjonistyczna | ||
** Konstruktywna interpretacja | ** Konstruktywna interpretacja spójników | ||
** Semantyka w zbiorach otwartych (bez dowodu). | ** Semantyka w zbiorach otwartych (bez dowodu). | ||
** | ** Formuły-typy, normalizacja dowodów jako proces obliczenia. | ||
* Logika 2 | * Logika 2 rzędu | ||
** Definicja, podstawowe własności. | ** Definicja, podstawowe własności. | ||
** Informacja o semantyce Henkina i relacji do polimorfizmu | ** Informacja o semantyce Henkina i relacji do polimorfizmu | ||
** | ** Równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach | ||
** Informacja o tw. Fagina | ** Informacja o tw. Fagina | ||
* Wybrane zastosowania logiki w informatyce | * Wybrane zastosowania logiki w informatyce | ||
Wersja z 10:50, 7 lip 2006
Forma zajęć
Wykład (30 godzin) + ćwiczenia (30 godzin)
Opis
Sylabus
Autorzy
- Jerzy Tiuryn
- Jerzy Tyszkiewicz
- Paweł Urzyczyn
Wymagania wstępne
- Logika i teoria mnogości
- Automaty i obliczenia
- Matematyka dyskretna
- Bazy danych
- Programowanie funkcyjne
- Złożoność obliczeniowa
Zawartość
- Rachunek zdań.
- Składnia formul i semantyka zerojedynkowa.
- Wzajemna wyrażalność spójników, funkcjonalna zupełność.
- Postać normalna formuły tautologii.
- Siła wyrazu logiki zdaniowej.
- Informacja o SAT-solverach
- Logika pierwszego rzędu - cz.1: definicje
- Formuły, zmienne wolne i związane.
- Spełnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.
- Podstawienie i jego sens semantyczny.
- Logika pierwszego rzędu - cz. 2: sposób użycia
- Dyskusja ważnych tautologii logiki pierwszego rzędu.
- Preneksowa postać normalna i jej zastosowania
- Logika formalna a zdania języka naturalnego.
- Logika pierwszego rzędu - cz. 3: ograniczenia
- Nierozstrzygalność logiki pierwszego rzędu.
- Elementarna równoważność struktur.
- Gry Ehrenfeuchta-Fraissego.
- Paradygmaty dowodzenia:
- styl Hilberta
- naturalna dedukcja,
- rachunek sekwentów.
- Informacja o informatycznych systemach dowodzenia
- Twierdzenie o pełności dla rachunku zdań.
- Twierdzenie o pełności dla rachunku predykatów.
- Teoria modeli
- Twierdzenie o zwartości i zastosowania
- Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
- Arytmetyka i tw. o niezupełności Goedla.
- Logiki programów
- Składnia PDL
- Twierdzenie o małym modelu dla PDL
- Twierdzenie o pełności dla PDL
- Logika intuicjonistyczna
- Konstruktywna interpretacja spójników
- Semantyka w zbiorach otwartych (bez dowodu).
- Formuły-typy, normalizacja dowodów jako proces obliczenia.
- Logika 2 rzędu
- Definicja, podstawowe własności.
- Informacja o semantyce Henkina i relacji do polimorfizmu
- Równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
- Informacja o tw. Fagina
- Wybrane zastosowania logiki w informatyce
- Tw. Codda
- Logiki wielowartościowe
- Weryfikacja wspierana komputerowo
