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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Jty (dyskusja | edycje)
Jty (dyskusja | edycje)
Linia 30: Linia 30:
** Postać normalna formuły tautologii.
** Postać normalna formuły tautologii.
**  Siła wyrazu logiki zdaniowej.
**  Siła wyrazu logiki zdaniowej.
** Informacja o SAT-solverach
* 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.  
Linia 47: Linia 46:
** 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.
Linia 70: Linia 68:
** Logiki wielowartościowe
** Logiki wielowartościowe
** Tw. Codda  
** Tw. Codda  
** Weryfikacja wspierana komputerowo
** Rozstrzygalnośc teorii logicznych

Wersja z 21:17, 21 sie 2006

Forma zajęć

Wykład (30 godzin) + ćwiczenia (30 godzin)

Opis

Zastosowanie metod i narzędzi logiki matematycznej w informatyce.

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 zdań.
    • Składnia formuł i semantyka zerojedynkowa.
    • Wzajemna wyrażalność spójników, funkcjonalna zupełność.
    • Postać normalna formuły tautologii.
    • Siła wyrazu logiki zdaniowej.
  • 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-Fraissego.
  • 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-Lowenheima, niestandardowy model arytmetyki.
  • Arytmetyka i tw. o niezupełności Goedla.
  • 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 (bez dowodu).
    • 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 tw. Fagina i Stockmeyera
    • Informacja o tw. Rabina
  • Logika w informatyce
    • Logiki wielowartościowe
    • Tw. Codda
    • Rozstrzygalnośc teorii logicznych