Tematy wykładów

• rozszerzone definicje indukcyjne
• schemat dowodów indukcyjnych dla tak skonstruowanych klas obiektów
• definicje indukcyjne dla klas obiektów zdefiniowanych indukcyjnie
• rachunek zdań, definicja
• wartościowania formuł zdaniowych, tautologie
• znajdywanie tautologii:
  • złożoność obliczeń wynikających z definicji
  • problem spełnialności SAT i jego trudność
• hilbertowski system dowodzenia
  • twierdzenie o adekwatności
  • twierdzenie o dedukcji
  • przykłady dowodów
  • Lemat Kalmara
  • Twierdzenie o pełności, dowód
• system dedukcji naturalnej
• informacja o logice intuicjonistycznej
• budowa formuł pierwszego rzędu
  • zmienne wolne
  • zasięg kwantyfikatorów, wolne wystąpienia zmiennych,
  • model, wartościowania, interpretacja termów, spełnianie formuły
  • przykład: arytmetyka reszt modulo 17
  • tautologie dla formuł pierwszego rzędu
  • znaczenie formuł z blokami kwantyfikatorów
  • dopuszczalność podstawień w formułach pierwszego rzędu
  • hilbertowski system dowodzenia dla formuł 1 rzędu,
  • twierdzenia o dedukcji, konwersji, generalizacji,
  • konsekwencje semantyczne, twierdzenie o adekwatności,
  • aksjonmaty arytmetyki Peano
  • twierdzenie o istnieniu modelu
  • twierdzenie o zwartości, przykład: istnienie niestandardowych modeli arytmetyki, własność niewyrażalna w języku pierwszego rzędu
  • twierdzenie o pełności
• niedowodliwość, nierozstrzygalność
  • tw. Goedla
  • maszyna RAM, problem stopu, problemy nierozstrzygalne (równoważność programów, informacja o równaniach diofantycznych)
• programowanie w logice
  • filozofia programowania imperatywnego, funkcyjnego, logicznego
  • programowanie w Prologu: mechanizm SLD-rezolucji i SLD-odrzucenia, podstawienia z SLD-rezolucji, twierdzenie o zupełności SLD-rezolucji

  ---