Logika dla informatyków: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Tprybick (dyskusja | edycje)
 
(Nie pokazano 20 wersji utworzonych przez 7 użytkowników)
Linia 4: Linia 4:


=== Opis ===
=== Opis ===
Zastosowanie metod i narzędzi logiki matematycznej w informatyce.
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 10: Linia 10:
=== Autorzy ===
=== Autorzy ===


* Jerzy Tiuryn
* Jerzy Tiuryn — Uniwersytet Warszawski
* Jerzy Tyszkiewicz  
* Jerzy Tyszkiewicz — Uniwersytet Warszawski
* Paweł Urzyczyn
* Paweł Urzyczyn — Uniwersytet Warszawski


=== Wymagania wstępne ===
=== Wymagania wstępne ===
Linia 25: Linia 25:
=== Zawartość ===
=== Zawartość ===


* Rachunek zdań.
* Rachunek zdań:
** Składnia formuł i semantyka zerojedynkowa.
** składnia formuł i semantyka zerojedynkowa
** Wzajemna wyrażalność spójników, funkcjonalna zupełność.
** tautologie rachunku zdań
** Postać normalna formuły tautologii.
** postać normalna formuł
**  Siła wyrazu logiki zdaniowej.
* 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
** dyskusja ważnych tautologii logiki pierwszego rzędu
** Dyskusja ważnych tautologii logiki pierwszego rzędu.
** preneksowa postać normalna i jej zastosowania  
** Preneksowa postać normalna i jej zastosowania  
** logika formalna a zdania języka naturalnego
** Logika formalna a zdania języka naturalnego.
* Logika pierwszego rzędu - cz. 3: ograniczenia:
* Logika pierwszego rzędu - cz. 3: ograniczenia
** nierozstrzygalność logiki pierwszego rzędu
** Nierozstrzygalność logiki pierwszego rzędu.
** elementarna równoważność struktur
** Elementarna równoważność struktur.
** gry Ehrenfeuchta-Fraïssé
** Gry Ehrenfeuchta-Fraissego.
* Paradygmaty dowodzenia:  
* Paradygmaty dowodzenia:  
** styl Hilberta
** styl Hilberta
** naturalna dedukcja,
** naturalna dedukcja
** rachunek sekwentów.
** rachunek sekwentów  
* Twierdzenie o pełności dla rachunku zdań.
* Twierdzenie o pełności dla rachunku zdań
* Twierdzenie o pełności dla rachunku predykatów.
* Twierdzenie o pełności dla rachunku predykatów
* Teoria modeli
* Teoria modeli:
** Twierdzenie o zwartości i zastosowania
** twierdzenie o zwartości i zastosowania
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
** twierdzenie Skolema-Löwenheima, niestandardowy model arytmetyki
* Arytmetyka i tw. o niezupełności Goedla.
* Arytmetyka i twierdzenie o niezupełności Gödla
* Logiki programów
* 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 spójników
** konstruktywna interpretacja spójników
** Semantyka w zbiorach otwartych (bez dowodu).
** 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:
** Definicja, podstawowe własności.
** definicja, podstawowe własności.
** Równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** Informacja o tw. Fagina i Stockmeyera
** informacja o twierdzeniu Fagina i Stockmeyera
** Informacja o tw. Rabina
** informacja o twierdzeniu Rabina
* Logika w informatyce
* Logika w informatyce:
** Logiki wielowartościowe
** logiki wielowartościowe
** Tw. Codda  
** twierdzenie Codda  
** Rozstrzygalnośc teorii logicznych
** rozstrzygalność teorii logicznych


== Moduły ==
== Moduły ==


[[Media:Logika.pdf | Wykład z logiki w formacie PDF]]


[[Logika dla informatyków/notacje| założenia]]
[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]]) TR
# [[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]]) TR
# [[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/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/Ograniczenia logiki pierwszego rzędu|Ograniczenia logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 4|Ć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/Paradygmaty dowodzenia|Paradygmaty dowodzenia]] ([[Logika dla informatyków/Ćwiczenia 5|Ćwiczenia]])
# [[Logika dla informatyków/Paradygmaty dowodzenia|Paradygmaty dowodzenia]] ([[Logika dla informatyków/Ćwiczenia 5|Ćwiczenia]])  
# [[Logika dla informatyków/Pełność rachunku zdań|Pełność rachunku zdań]] ([[Logika dla informatyków/Ćwiczenia 6|Ćwiczenia]])
# [[Logika dla informatyków/Pełność rachunku zdań|Pełność rachunku zdań]] ([[Logika dla informatyków/Ćwiczenia 6|Ć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 predykatów|Pełność rachunku predykatów]] ([[Logika dla informatyków/Ćwiczenia 7|Ćwiczenia]])
# [[Logika dla informatyków/Teoria modeli|Teoria modeli]] ([[Logika dla informatyków/Ćwiczenia 8|Ćwiczenia]]) TR
# [[Logika dla informatyków/Teoria modeli|Teoria modeli]] ([[Logika dla informatyków/Ćwiczenia 8|Ćwiczenia]])  
# [[Logika dla informatyków/Arytmentyka pierwszego rzędu|Arytmetyka pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 9|Ćwiczenia]]) TR
# [[Logika dla informatyków/Arytmetyka pierwszego rzędu|Arytmetyka pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 9|Ćwiczenia]])  
# [[Logika dla informatyków/Zdaniowa logika dynamiczna|Zdaniowa logika dynamiczna]] ([[Logika dla informatyków/Ćwiczenia 10|Ćwiczenia]])
# [[Logika dla informatyków/Zdaniowa logika dynamiczna|Zdaniowa logika dynamiczna]] ([[Logika dla informatyków/Ćwiczenia 10|Ćwiczenia]])  
# [[Logika dla informatyków/Logika intuicjonistyczna|Logika intuicjonistyczna]] ([[Logika dla informatyków/Ćwiczenia 11|Ćwiczenia]])
# [[Logika dla informatyków/Logika intuicjonistyczna|Logika intuicjonistyczna]] ([[Logika dla informatyków/Ćwiczenia 11|Ć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 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]])
# [[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