Logika matematyczna i jej zastosowania 1000-M1LogMatZas

Przedmiot ma charakter wprowadzający i przekrojowy, gdyż celem jest przedstawienie fundamentalnych informacji o rożnych rodzajach logik bez dowodzenia trudnych twierdzeń. Ważną rolę będą odgrywały zastosowania w informatyce i matematyce. Chociaż logika matematyczna jest z natury przedmiotem formalnym (więc sprawia wrażenie wymagającego), przedstawiane na wykładzie i ćwiczeniach treści będą miały umiarkowany poziom trudności, odpowiedni zarówno dla matematyków jak i informatyków. Dodatkowym atutem zajęć jest obecność dużej liczby przykładów.

Plan przedmiotu:

(1) Elementy teorii języków formalnych – rozstrzygalność; języki rekurencyjne; formalne systemy dowodzenia.

(2) Logika pierwszego rzędu – uzupełnienie informacji o klasycznym rachunku zdań; syntaktyka i semantyka logiki pierwszego rzędu; systemy dowodzenia i rachunek sekwentów; podstawowe twierdzenia teorii modeli, w tym twierdzenia Gödla o niezupełności; wzmianka o logikach wyższych rzędów; zastosowania, m. in. Twierdzenie Codda.

(3) Logika intuicjonistyczna – intuicjonistyczny rachunek zdań; semantyka Kripkego; kraty, algebry Boole'a i algebry Heytinga; lambda-termy bez typów i z typami; izomorfizm Curry'ego-Howarda.

(4) Logika modalna – modalny rachunek zdań; modele Kripkego dla logiki modalnej; przykłady (logika temporalna i dynamiczna); podstawowe twierdzenia; bisymulacje.

(5) O roli teorii kategorii w informatyce i logice matematycznej.

Uwaga. Punkty (4) i (5) będą zrealizowane w zależności od czasu oraz zainteresowań i możliwości większości studentów.

Całkowity nakład pracy studenta

30 godz. – wykład 5 godz. - egzamin 30 godz. - ćwiczenia 50 godz. - praca własna - bieżące przygotowanie do zajęć, studiowanie literatury, 35 godz. praca własna - przygotowanie do egzaminu RAZEM: 150 godz. 6 pkt. ECTS

Efekty uczenia się - wiedza

Po ukończeniu kursu student(ka) osiąga następujące efekty (kody odnoszą się do efektów dla studiów 1 stopnia na kierunku informatyka i matematyka): W1: ma uporządkowaną wiedzę ogólną w zakresie podstawowych działów logiki matematycznej, w tym przede wszystkim logiki pierwszego rzędu, logiki modalnej i logiki intuicjonistycznej - K_W01 (inf), K_W03 (mat); W2: rozumie rolę i znaczenie formalizmu matematycznego w podstawach informatyki - K_W01 (inf), K_W03 (mat). W3: rozumie budowę zaawansowanych teorii matematycznych, potrafi użyć formalizmu matematycznego do budowy i analizy prostych modeli matematycznych w innych dziedzinach - K_W01 (inf), K_W03 (mat).

Efekty uczenia się - umiejętności

Po ukończeniu kursu student(ka) osiąga następujące efekty (kody odnoszą się do efektów dla studiów 1 stopnia na kierunku informatyka i matematyka): U1: umie stosować oraz przedstawiać w mowie i na piśmie podstawowe metody logiki pierwszego rzędu, logiki modalnej i logiki intuicjonistycznej - K_U01, K_U02, K_U03 (inf); K_U01, K_U02 (mat).

Efekty uczenia się - kompetencje społeczne

Po ukończeniu kursu student(ka) osiąga następujące efekty (kody odnoszą się do efektów dla studiów 1 stopnia na kierunku informatyka i matematyka): K1: W zrozumiały sposób przekazuje innym swoje myśli i właściwie posługuje się terminologią fachową. Nawiązuje kontakt w obrębie grupy celem przyswojenia trudniejszych zagadnień lub rozwiązania złożonych problemów. swojej dziedziny - K_K02 (inf, mat) K2: rozumie potrzebę ciągłego doskonalenia się - K_K03 (inf, mat)

Koordynatorzy przedmiotu

Grzegorz Pastuszak

Metody dydaktyczne

Metody podające – wykład konwersatoryjny Metody poszukujące – ćwiczeniowa

Metody dydaktyczne podające

- wykład informacyjny (konwencjonalny)

Metody dydaktyczne poszukujące

- laboratoryjna
- projektu
- klasyczna metoda problemowa
- ćwiczeniowa
- seminaryjna
- giełda pomysłów
- referatu

Metody dydaktyczne w kształceniu online

- metody wymiany i dyskusji
- metody służące prezentacji treści
- metody rozwijające refleksyjne myślenie

Rodzaj przedmiotu

przedmiot fakultatywny

Wymagania wstępne

Podstawowa wiedza w zakresie pierwszego roku studiów informatycznych lub matematycznych. Przedmiot przeznaczony zarówno dla studentów informatyki jak i matematyki.

Kryteria oceniania

Egzamin pisemny obejmujący zagadnienia teoretyczne (przede wszystkim) i praktyczne - W1, W2, W3.

Ćwiczenia (prace pisemne w postaci 1-2 kolokwiów i aktywność)- U1, K1, K2.

Przystąpienie do poprawy ćwiczeń wymaga uzyskania na zajęciach niezbędnego minimum z prac pisemnych (do ustalenia w trakcie semestru).

Literatura

Literatura:

(1) D. Marker, Model theory. An introduction. Graduate Texts in Mathematics, 217. Springer-Verlag, New York, 2002.

(2) M. Sorensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, Volume 149, 2007.

(3) P. Blackburn, M. de Rijke, Y. Venema, Modal logic. Cambridge Tracts in Theoretical Computer Science, 53. Cambridge University Press, Cambridge, 2001.

(4) Materiały przygotowane przez wykładowcę.

Więcej informacji

Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb:

Strona przedmiotu 1000-M1LogMatZas w USOSweb