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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
m Poprawki edytorskie i wprowadzenie opisu
 
(Nie pokazano 35 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 formul 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:
** Informacja o SAT-solverach
** formuły, zmienne wolne i związane
* Logika pierwszego rzędu - cz.1: definicje
** spełnianie formul w strukturach relacyjnych, pojecie tautologii, wynikania semantycznego
** Formuły, zmienne wolne i związane.
** podstawienie i jego sens semantyczny
** Spełnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.
* Logika pierwszego rzędu - cz. 2: sposób użycia:
** Podstawienie i jego sens semantyczny.
** dyskusja ważnych tautologii logiki pierwszego rzędu
* Logika pierwszego rzędu - cz. 2: sposób użycia
** preneksowa postać normalna i jej zastosowania  
** Dyskusja ważnych tautologii logiki pierwszego rzędu.
** logika formalna a zdania języka naturalnego
** Preneksowa postać normalna i jej zastosowania  
* Logika pierwszego rzędu - cz. 3: ograniczenia:
** Logika formalna a zdania języka naturalnego.
** nierozstrzygalność logiki pierwszego rzędu
* Logika pierwszego rzędu - cz. 3: ograniczenia
** elementarna równoważność struktur
** Nierozstrzygalność logiki pierwszego rzędu.
** gry Ehrenfeuchta-Fraïssé
** Elementarna równoważność struktur.
** Gry Ehrenfeuchta-Fraissego.
* Paradygmaty dowodzenia:  
* Paradygmaty dowodzenia:  
** styl Hilberta
** styl Hilberta
** naturalna dedukcja,
** naturalna dedukcja
** rachunek sekwentów.
** rachunek sekwentów  
** Informacja o informatycznych systemach dowodzenia
* 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-Löwenheima, niestandardowy model arytmetyki
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
* Arytmetyka i twierdzenie o niezupełności Gödla
* Arytmetyka i tw. o niezupełności Goedla.
* 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  
** Semantyka w zbiorach otwartych (bez dowodu).
** 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
** Informacja o semantyce Henkina i relacji do polimorfizmu
** informacja o twierdzeniu Fagina i Stockmeyera
** Równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** informacja o twierdzeniu Rabina
** Informacja o tw. Fagina
* Logika w informatyce:
* Wybrane zastosowania logiki w informatyce
** logiki wielowartościowe
** Tw. Codda
** twierdzenie Codda
** Logiki wielowartościowe
** rozstrzygalność teorii logicznych
** Weryfikacja wspierana komputerowo
 
== 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/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/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 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]])
# [[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/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 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


Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Logika_dla_informatyków&oldid=69291”