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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Jty (dyskusja | edycje)
 
(Nie pokazano 9 wersji utworzonych przez 5 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 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-Fraissego
** 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 (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:
Linia 71: Linia 71:
== Moduły ==
== Moduły ==


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


[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]]) TR
<!--
# [[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/Ograniczenia logiki pierwszego rzędu|Ograniczenia logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 4|Ćwiczenia]])AS
# [[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]]) PK
# [[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]])AS
# [[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]])AS
# [[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]]) TR
# [[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/Arytmentyka pierwszego rzędu|Arytmetyka pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 9|Ćwiczenia]]) TR
# [[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]]) PK
# [[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]]) PK
# [[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]]) PK
# [[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]])AS
# [[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