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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Diks (dyskusja | edycje)
538 edycji
Poprawki edytorskie
Linia 6: Linia 6:




=== Sylabus ===
== Sylabus ==


=== Autorzy ===
=== Autorzy ===
Linia 15: Linia 15:


=== Wymagania wstępne ===
=== Wymagania wstępne ===
===== Konieczne =====


* Logika i teoria mnogości
* Logika i teoria mnogości
* Automaty i obliczenia
* Automaty i obliczenia
* Matematyka dyskretna
* Matematyka dyskretna
===== Pożądane, ale niekonieczne =====
* Bazy danych
* Bazy danych
* Programowanie funkcyjne
* Programowanie funkcyjne
Linia 36: Linia 31:
**  Sila wyrazu logiki zdaniowej.
**  Sila wyrazu logiki zdaniowej.
** Informacja o SAT-solverach
** Informacja o SAT-solverach
* Logika pierwszego rzedu - cz.1: definicje
* Logika pierwszego rzedu - cz.1: definicje
** Formuly, zmienne wolne i zwiazane.  
** Formuly, zmienne wolne i zwiazane.  
** Spelnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.  
** Spelnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.  
** Podstawienie i jego sens semantyczny.  
** Podstawienie i jego sens semantyczny.  
* Logika pierwszego rzedu - cz. 2: sposob uzycia
* Logika pierwszego rzedu - cz. 2: sposob uzycia
**  Dyskusja waznych tautologii logiki pierwszego rzedu.
**  Dyskusja waznych tautologii logiki pierwszego rzedu.
** Preneksowa postac normalna i jej zastosowania  
** Preneksowa postac normalna i jej zastosowania  
** Logika formalna a zdania jezyka naturalnego.
** Logika formalna a zdania jezyka naturalnego.
* Logika pierwszego rzedu - cz. 3: ograniczenia
* Logika pierwszego rzedu - cz. 3: ograniczenia
** Nierozstrzygalnosc lgiki pierwszego rzedu.
** Nierozstrzygalnosc lgiki pierwszego rzedu.
** Elementarna rownowaznosc struktur.
** Elementarna rownowaznosc struktur.
** Gry Ehrenfeuchta-Fraissego.
** Gry Ehrenfeuchta-Fraissego.
* Paradygmaty dowodzenia:  
* Paradygmaty dowodzenia:  
** styl Hilberta
** styl Hilberta
Linia 57: Linia 48:
** rachunek sekwentow.  
** rachunek sekwentow.  
** Informacja o proverach
** Informacja o proverach
* Twierdzenie o Pelnosci dla  rachunku zdan.
* Twierdzenie o Pelnosci dla  rachunku zdan.
* Twierdzenie o Pelnosci dla  rachunku predykatow.
* Twierdzenie o Pelnosci dla  rachunku predykatow.
* Teoria modeli
* Teoria modeli
** Twierdzenie o zwartosci i zastosowania
** Twierdzenie o zwartosci i zastosowania
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.  
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.  
**
* Arytmetyka i tw. o niezpulenosci Goedla.
* Arytmetyka i tw. o niezpulenosci Goedla.
*  Logiki programow
*  Logiki programow
** 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 spojnikow
** Konstruktywna interpretacja spojnikow
** Semantyka w zbiorach otwartych (bez dowodu).  
** Semantyka w zbiorach otwartych (bez dowodu).  
** Formuly-typy, normalizacja dowodów jako proces obliczenia.
** Formuly-typy, normalizacja dowodów jako proces obliczenia.
* Logika 2 rzedu
* Logika 2 rzedu
** Definicja, podstawowe własności.
** Definicja, podstawowe własności.
Linia 86: Linia 67:
** Równoważnośc monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** Równoważnośc 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
** Tw. Codda  
** Tw. Codda  
** Logiki wielowartościowe
** Logiki wielowartościowe
** Weryfikacja wspierana komputerowo
** Weryfikacja wspierana komputerowo

Wersja z 10:44, 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 zdan.
    • Skladnia formul i semantyka zerojedynkowa.
    • Wzajemna wyrazalnosc spojnikow, funkcjonalna zupelnosc.
    • Postac normalna formuly tautologii.
    • Sila wyrazu logiki zdaniowej.
    • Informacja o SAT-solverach
  • Logika pierwszego rzedu - cz.1: definicje
    • Formuly, zmienne wolne i zwiazane.
    • Spelnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.
    • Podstawienie i jego sens semantyczny.
  • Logika pierwszego rzedu - cz. 2: sposob uzycia
    • Dyskusja waznych tautologii logiki pierwszego rzedu.
    • Preneksowa postac normalna i jej zastosowania
    • Logika formalna a zdania jezyka naturalnego.
  • Logika pierwszego rzedu - cz. 3: ograniczenia
    • Nierozstrzygalnosc lgiki pierwszego rzedu.
    • Elementarna rownowaznosc struktur.
    • Gry Ehrenfeuchta-Fraissego.
  • Paradygmaty dowodzenia:
    • styl Hilberta
    • naturalna dedukcja,
    • rachunek sekwentow.
    • Informacja o proverach
  • Twierdzenie o Pelnosci dla rachunku zdan.
  • Twierdzenie o Pelnosci dla rachunku predykatow.
  • Teoria modeli
    • Twierdzenie o zwartosci i zastosowania
    • Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
  • Arytmetyka i tw. o niezpulenosci Goedla.
  • Logiki programow
    • Składnia PDL
    • Twierdzenie o małym modelu dla PDL
    • Twierdzenie o pełności dla PDL
  • Logika intuicjonistyczna
    • Konstruktywna interpretacja spojnikow
    • Semantyka w zbiorach otwartych (bez dowodu).
    • Formuly-typy, normalizacja dowodów jako proces obliczenia.
  • Logika 2 rzedu
    • Definicja, podstawowe własności.
    • Informacja o semantyce Henkina i relacji do polimorfizmu
    • Równoważnośc 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
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Logika_dla_informatyków&oldid=3038”