Uniwersytet Mikołaja Kopernika w Toruniu - Centralny punkt logowania
Strona główna

Logiczne aspekty informatyki

Informacje ogólne

Kod przedmiotu: 1000-I2LAI
Kod Erasmus / ISCED: (brak danych) / (0613) Tworzenie i analiza oprogramowania i aplikacji Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
Nazwa przedmiotu: Logiczne aspekty informatyki
Jednostka: Wydział Matematyki i Informatyki
Grupy: Inf., I st., stacjonarne, 2 rok, przedmioty do wyboru
Inf., I st., stacjonarne, 3 rok, przedmioty do wyboru
Inf., II st, stacjonarne, przedmioty do wyboru
Punkty ECTS i inne: 6.00 Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.

zobacz reguły punktacji
Język prowadzenia: polski
Wymagania wstępne:

Podstawowa wiedza w zakresie pierwszego roku studiów informatycznych lub matematycznych.

Rodzaj przedmiotu:

przedmiot fakultatywny

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 - studia licencjackie i inżynierskie):


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;


W2: rozumie rolę i znaczenie formalizmu matematycznego w podstawach informatyki - K_W01


W3: rozumie budowę zaawansowanych teorii matematycznych, potrafi użyć formalizmu matematycznego do budowy i analizy prostych modeli matematycznych w innych dziedzinach - K_W01

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 - studia licencjackie i inżynierskie):


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

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 - studia licencjackie i inżynierskie):


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


K2: rozumie potrzebę ciągłego doskonalenia się - K_K03

Metody dydaktyczne:

Metody podające – wykład konwersatoryjny


Metody poszukujące – ćwiczeniowa

Metody dydaktyczne podające:

- wykład informacyjny (konwencjonalny)

Metody dydaktyczne poszukujące:

- ćwiczeniowa
- laboratoryjna
- referatu

Skrócony opis:

Celem przedmiotu jest wprowadzenie w podstawowe zagadnienia szeroko rozumianej logiki matematycznej, ze szczególnym uwzględnieniem zastosowań w informatyce. Logika matematyczna jest jedną z podstawowych dziedzin matematyki (obok teorii kategorii i matematyki dyskretnej), które z powodzeniem wykorzystywane są w informatyce. W języku logiki formułuje się wiele podstawowych zagadnień i teorii informatycznych, do których należą: rozstrzygalność i nierozstrzygalność języków formalnych, programowanie funkcyjne, sztuczna inteligencja, semantyka i weryfikacja programów, teoria złożoności, teoria obliczalności. Największą rolę w informatyce odgrywają trzy dziedziny logiki – logika pierwszego rzędu (tzn. rachunek kwantyfikatorów), logika intuicjonistyczna oraz logika modalna. Ten fakt posiada swoje odzwierciedlenie w programie przedmiotu, który w naszym założeniu powinien być możliwie szeroki i przekrojowy.

Pełny opis:

(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.

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ę.

Metody i 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).

Zajęcia w cyklu "Semestr letni 2021/22" (zakończony)

Okres: 2022-02-21 - 2022-09-30
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Ćwiczenia, 30 godzin, 30 miejsc więcej informacji
Wykład, 30 godzin, 30 miejsc więcej informacji
Koordynatorzy: Grzegorz Pastuszak
Prowadzący grup: Grzegorz Pastuszak
Lista studentów: (nie masz dostępu)
Zaliczenie: Przedmiot - Egzamin
Ćwiczenia - Zaliczenie na ocenę
Wykład - Egzamin

Zajęcia w cyklu "Semestr letni 2022/23" (zakończony)

Okres: 2023-02-20 - 2023-09-30
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Ćwiczenia, 30 godzin, 30 miejsc więcej informacji
Wykład, 30 godzin, 30 miejsc więcej informacji
Koordynatorzy: Grzegorz Pastuszak
Prowadzący grup: Grzegorz Pastuszak
Lista studentów: (nie masz dostępu)
Zaliczenie: Przedmiot - Egzamin
Ćwiczenia - Zaliczenie na ocenę
Wykład - Egzamin

Zajęcia w cyklu "Semestr letni 2023/24" (w trakcie)

Okres: 2024-02-20 - 2024-09-30
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Ćwiczenia, 30 godzin, 30 miejsc więcej informacji
Wykład, 30 godzin, 30 miejsc więcej informacji
Koordynatorzy: Grzegorz Pastuszak
Prowadzący grup: Grzegorz Pastuszak
Lista studentów: (nie masz dostępu)
Zaliczenie: Przedmiot - Egzamin
Ćwiczenia - Zaliczenie na ocenę
Wykład - Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Mikołaja Kopernika w Toruniu.
ul. Jurija Gagarina 11, 87-100 Toruń tel: +48 56 611-40-10 https://usosweb.umk.pl/ kontakt deklaracja dostępności USOSweb 7.0.2.0-1 (2024-03-12)