Logika dla informatyków: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
(Nie pokazano 9 wersji utworzonych przez 5 użytkowników) | |||
Linia 4: | Linia 4: | ||
=== Opis === | === Opis === | ||
Wykład logiki dla informatyków na poziomie magisterskim. Oprócz przedstawienia klasycznych pojęć i wyników logiki matematycznej i teorii modeli, zawiera wykłady poświęcone działom logiki silnie powiązanym z teoretyczną informatyką. | |||
== Sylabus == | == Sylabus == | ||
Linia 31: | Linia 31: | ||
* Logika pierwszego rzędu - cz.1: definicje: | * Logika pierwszego rzędu - cz.1: definicje: | ||
** formuły, zmienne wolne i związane | ** formuły, zmienne wolne i związane | ||
** spełnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego | ** spełnianie formul w strukturach relacyjnych, pojecie tautologii, wynikania semantycznego | ||
** podstawienie i jego sens semantyczny | ** podstawienie i jego sens semantyczny | ||
* Logika pierwszego rzędu - cz. 2: sposób użycia: | * Logika pierwszego rzędu - cz. 2: sposób użycia: | ||
Linia 40: | Linia 40: | ||
** nierozstrzygalność logiki pierwszego rzędu | ** nierozstrzygalność logiki pierwszego rzędu | ||
** elementarna równoważność struktur | ** elementarna równoważność struktur | ||
** gry Ehrenfeuchta- | ** gry Ehrenfeuchta-Fraïssé | ||
* Paradygmaty dowodzenia: | * Paradygmaty dowodzenia: | ||
** styl Hilberta | ** styl Hilberta | ||
Linia 57: | Linia 57: | ||
* Logika intuicjonistyczna: | * Logika intuicjonistyczna: | ||
** konstruktywna interpretacja spójników | ** konstruktywna interpretacja spójników | ||
** semantyka w zbiorach otwartych | ** semantyka w zbiorach otwartych | ||
** formuły-typy, normalizacja dowodów jako proces obliczenia | ** formuły-typy, normalizacja dowodów jako proces obliczenia | ||
* Logika 2 rzędu: | * Logika 2 rzędu: | ||
Linia 71: | Linia 71: | ||
== Moduły == | == Moduły == | ||
[http://www.mimuw.edu.pl/~urzy/calosc.pdf Wykład z logiki w formacie PDF] | |||
# [[Logika dla informatyków/Rachunek zdań|Rachunek zdań]] ([[Logika dla informatyków/Ćwiczenia 1|Ćwiczenia]]) | <!-- | ||
# [[Logika dla informatyków/Język logiki pierwszego rzędu|Język logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 2|Ćwiczenia]]) | # [[Logika dla informatyków/Rachunek zdań|Rachunek zdań]] ([[Logika dla informatyków/Ćwiczenia 1|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia|Logika pierwszego rzędu. Sposób użycia]] ([[Logika dla informatyków/Ćwiczenia 3|Ćwiczenia]]) | # [[Logika dla informatyków/Język logiki pierwszego rzędu|Język logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 2|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Ograniczenia logiki pierwszego rzędu|Ograniczenia logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 4|Ćwiczenia]]) | # [[Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia|Logika pierwszego rzędu. Sposób użycia]] ([[Logika dla informatyków/Ćwiczenia 3|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Paradygmaty dowodzenia|Paradygmaty dowodzenia]] ([[Logika dla informatyków/Ćwiczenia 5|Ćwiczenia]]) | # [[Logika dla informatyków/Ograniczenia logiki pierwszego rzędu|Ograniczenia logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 4|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Pełność rachunku zdań|Pełność rachunku zdań]] ([[Logika dla informatyków/Ćwiczenia 6|Ćwiczenia]]) | # [[Logika dla informatyków/Paradygmaty dowodzenia|Paradygmaty dowodzenia]] ([[Logika dla informatyków/Ćwiczenia 5|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Pełność rachunku predykatów|Pełność rachunku predykatów]] ([[Logika dla informatyków/Ćwiczenia 7|Ćwiczenia]]) | # [[Logika dla informatyków/Pełność rachunku zdań|Pełność rachunku zdań]] ([[Logika dla informatyków/Ćwiczenia 6|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Teoria modeli|Teoria modeli]] ([[Logika dla informatyków/Ćwiczenia 8|Ćwiczenia]]) | # [[Logika dla informatyków/Pełność rachunku predykatów|Pełność rachunku predykatów]] ([[Logika dla informatyków/Ćwiczenia 7|Ćwiczenia]]) | ||
# [[Logika dla informatyków/ | # [[Logika dla informatyków/Teoria modeli|Teoria modeli]] ([[Logika dla informatyków/Ćwiczenia 8|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Zdaniowa logika dynamiczna|Zdaniowa logika dynamiczna]] ([[Logika dla informatyków/Ćwiczenia 10|Ćwiczenia]]) | # [[Logika dla informatyków/Arytmetyka pierwszego rzędu|Arytmetyka pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 9|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Logika intuicjonistyczna|Logika intuicjonistyczna]] ([[Logika dla informatyków/Ćwiczenia 11|Ćwiczenia]]) | # [[Logika dla informatyków/Zdaniowa logika dynamiczna|Zdaniowa logika dynamiczna]] ([[Logika dla informatyków/Ćwiczenia 10|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Logika drugiego rzędu|Logika drugiego rzędu]] ([[Logika dla informatyków/Ćwiczenia 12|Ćwiczenia]]) | # [[Logika dla informatyków/Logika intuicjonistyczna|Logika intuicjonistyczna]] ([[Logika dla informatyków/Ćwiczenia 11|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Logika w informatyce|Logika w informatyce]] ([[Logika dla informatyków/Ćwiczenia 13|Ćwiczenia]]) | # [[Logika dla informatyków/Logika drugiego rzędu|Logika drugiego rzędu]] ([[Logika dla informatyków/Ćwiczenia 12|Ćwiczenia]]) | ||
# [[Logika dla informatyków/Logika w informatyce|Logika w informatyce]] ([[Logika dla informatyków/Ćwiczenia 13|Ćwiczenia]]) | |||
--> |
Aktualna wersja na dzień 21:49, 5 lut 2007
Forma zajęć
Wykład (30 godzin) + ćwiczenia (30 godzin)
Opis
Wykład logiki dla informatyków na poziomie magisterskim. Oprócz przedstawienia klasycznych pojęć i wyników logiki matematycznej i teorii modeli, zawiera wykłady poświęcone działom logiki silnie powiązanym z teoretyczną informatyką.
Sylabus
Autorzy
- Jerzy Tiuryn — Uniwersytet Warszawski
- Jerzy Tyszkiewicz — Uniwersytet Warszawski
- Paweł Urzyczyn — Uniwersytet Warszawski
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 formuł i semantyka zerojedynkowa
- tautologie rachunku zdań
- postać normalna formuł
- 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-Fraïssé
- Paradygmaty dowodzenia:
- styl Hilberta
- naturalna dedukcja
- rachunek sekwentów
- 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-Löwenheima, niestandardowy model arytmetyki
- Arytmetyka i twierdzenie o niezupełności Gödla
- 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
- formuły-typy, normalizacja dowodów jako proces obliczenia
- Logika 2 rzędu:
- definicja, podstawowe własności.
- równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
- informacja o twierdzeniu Fagina i Stockmeyera
- informacja o twierdzeniu Rabina
- Logika w informatyce:
- logiki wielowartościowe
- twierdzenie Codda
- rozstrzygalność teorii logicznych
Moduły
Wykład z logiki w formacie PDF