Moduł oferowany także w ramach programów studiów:
Informacje ogólne:
Nazwa:
Logika matematyczna w informatyce
Tok studiów:
2014/2015
Kod:
IIN-1-207-s
Wydział:
Informatyki, Elektroniki i Telekomunikacji
Poziom studiów:
Studia I stopnia
Specjalność:
-
Kierunek:
Informatyka
Semestr:
2
Profil kształcenia:
Ogólnoakademicki (A)
Język wykładowy:
Polski
Forma i tryb studiów:
Stacjonarne
Strona www:
 
Osoba odpowiedzialna:
dr Gładki Paweł (pawel.gladki@us.edu.pl)
Osoby prowadzące:
Krótka charakterystyka modułu

Opis efektów kształcenia dla modułu zajęć
Kod EKM Student, który zaliczył moduł zajęć wie/umie/potrafi Powiązania z EKK Sposób weryfikacji efektów kształcenia (forma zaliczeń)
Wiedza
M_W001 Student zna i rozumie podstawowe pojęcia matematyczne niezbędne do operowania wiedzą z zakresu logiki matematycznej IN1A_W01 Kolokwium
M_W002 Student zna i rozumie podstawowe pojęcia logiczne niezbędne do posługiwania się narzędziami logicznymi w informatyce IN1A_W01 Kolokwium
M_W003 Student zna i rozumie teoretyczne podstawy programowania funkcyjnego IN1A_W05 Kolokwium
M_W004 Student zna nowoczesne narzędzia informatyczne wspomagające proces weryfikacji algorytmów w oparciu o metody logiki matematycznej IN1A_W04 Kolokwium
Umiejętności
M_U001 Student potrafi zastosować system wspomagania dowodzenia twierdzeń Coq do przeprowadzenia dowodów prostych twierdzeń matematycznych IN1A_U11 Wykonanie ćwiczeń laboratoryjnych
M_U002 Student potrafi przeprowadzić ekstrakcję programów z dowodów w Coq i weryfikować ich poprawność IN1A_U11 Wykonanie ćwiczeń laboratoryjnych
M_U003 Student potrafi weryfikować poprawność algorytmów w oparciu o techniki sprawdzania modeli i Java Pathfinder IN1A_U11 Wykonanie ćwiczeń laboratoryjnych
Kompetencje społeczne
M_K001 Student potrafi współdziałać i pracować w grupie nad projektem informatycznym wiążącym się z bezpieczeństwem danych i weryfikacją poprawności IN1A_K03 Aktywność na zajęciach
Matryca efektów kształcenia w odniesieniu do form zajęć
Kod EKM Student, który zaliczył moduł zajęć wie/umie/potrafi Forma zajęć
Wykład
Ćwicz. aud
Ćwicz. lab
Ćw. proj.
Konw.
Zaj. sem.
Zaj. prakt
Zaj. terenowe
Zaj. warsztatowe
Inne
E-learning
Wiedza
M_W001 Student zna i rozumie podstawowe pojęcia matematyczne niezbędne do operowania wiedzą z zakresu logiki matematycznej + - - - - - - - - - -
M_W002 Student zna i rozumie podstawowe pojęcia logiczne niezbędne do posługiwania się narzędziami logicznymi w informatyce + - - - - - - - - - -
M_W003 Student zna i rozumie teoretyczne podstawy programowania funkcyjnego + - - - - - - - - - -
M_W004 Student zna nowoczesne narzędzia informatyczne wspomagające proces weryfikacji algorytmów w oparciu o metody logiki matematycznej + - - - - - - - - - -
Umiejętności
M_U001 Student potrafi zastosować system wspomagania dowodzenia twierdzeń Coq do przeprowadzenia dowodów prostych twierdzeń matematycznych - + - - - - - - - - -
M_U002 Student potrafi przeprowadzić ekstrakcję programów z dowodów w Coq i weryfikować ich poprawność - + - - - - - - - - -
M_U003 Student potrafi weryfikować poprawność algorytmów w oparciu o techniki sprawdzania modeli i Java Pathfinder - + - - - - - - - - -
Kompetencje społeczne
M_K001 Student potrafi współdziałać i pracować w grupie nad projektem informatycznym wiążącym się z bezpieczeństwem danych i weryfikacją poprawności - + - - - - - - - - -
Treść modułu zajęć (program wykładów i pozostałych zajęć)
Wykład:
  1. Preliminaria algebraiczne (4 godziny).

    Relacje i funkcje. Równoważności i porządki. Algebry. Homomorfizmy. Algebry wolne, ilorazowe i produkty algebr. Algebry Boole’a. Kraty. Grafy i drzewa. Filtry i ultrafiltry.

  2. Klasyczny rachunek zdań (6 godzin).

    Monoidy wolne. Języki formalne. Systemy dedukcyjne. Język logiki zdań. Klasyczny rachunek zdań. Twierdzenia o dedukcji i ekstensjonalności. Semantyka klasycznego rachunku zdań. Spełnialność. Twierdzenie o zwartości. Tautologie. Twierdzenia o zgodności i pełności. Niesprzeczność. Twierdzenie Malceva.

  3. Rachunek lambda (8 godzin).

    Indukcja i rekursja strukturalna. Termy i podstawianie termów. Lambda-termy, abstrakcje i aplikacje. Drzewka de Bruijna. Podstawianie termów w rachunku lambda. Beta-redukcje, postać beta-normalna i twierdzenie Churcha-Rosera. Mocna i słaba własność Churcha-Rosera, silna normalizacja i lemat Newmana. Standaryzacja i twierdzenie o normalizacji. Obliczenia, obliczalność, liczebniki Churcha i definiowalność. Rachunek kombinatorów, typy proste i twierdzenie Curry-Howarda.

  4. Wprowadzenie do Coq (6 godzin).

    Rola systemu Coq, weryfikacja dowodów, tworzenie dowodów, weryfikacja. Podstawowe taktyki, składanie taktyk, fazy tworzenia dowodu. Programy funkcyjne zapisane w Coq, specyfikacje, dowody. Dowodzenie poprawności programów imperatywnych.

  5. Wprowadzenie do Java Pathfinder (6 godzin).

    Weryfikacja programów przez dowody vs. przez sprawdzanie modelu. Logiki czasowe LTL. Syntaktyka i semantyka. Semantyczna równoważność formuł. Przykładowe zastosowania.

Ćwiczenia audytoryjne:

1. Składanie lambda-termów.
2. Kody de-Bruijna.
3. Sytenza typów lambda-termów.
4. Taktyki dla dowodów zdań, równań i predykatów.
5. Indukcja, typy induktywne, dowody właściwości funkcji rekurencyjnych.
6. Ekstrakcja programów w Coq.
7. Model-checking w Java Pathfinder.

Nakład pracy studenta (bilans punktów ECTS)
Forma aktywności studenta Obciążenie studenta
Sumaryczne obciążenie pracą studenta 60 godz
Punkty ECTS za moduł 2 ECTS
Udział w wykładach 30 godz
Samodzielne studiowanie tematyki zajęć 10 godz
Udział w ćwiczeniach laboratoryjnych 15 godz
Przygotowanie do zajęć 5 godz
Pozostałe informacje
Sposób obliczania oceny końcowej:

1. Aby uzyskać pozytywną ocenę końcową niezbędne jest uzyskanie pozytywnej oceny z laboratorium oraz kolokwium zaliczeniowego z wykładu.
2. Obliczamy średnią ważoną z ocen z laboratorium (75%) i wykładów (25%) uzyskanych we wszystkich terminach.
3. Wyznaczmy ocenę końcową na podstawie zależności:
if sr>4.75 then OK:=5.0 else
if sr>4.25 then OK:=4.5 else
if sr>3.75 then OK:=4.0 else
if sr>3.25 then OK:=3.5 else OK:=3
4. Jeżeli pozytywną ocenę z laboratorium i zaliczenia wykładu uzyskano w pierwszym terminie oraz ocena końcowa jest mniejsza niż 5.0 to ocena końcowa jest podnoszona o 0.5

Wymagania wstępne i dodatkowe:

Umiejętność obsługi komputera, pracującego pod kontrolą dowolnego systemu operacyjnego, w podstawowym zakresie. Znajomość matematyki w zakresie wymaganym dla studentów pierwszego roku studiów informatycznych.

Zalecana literatura i pomoce naukowe:

1. M. Fitting, R.L. Mendelsohn, First Order Modal Logic, Kluwer, 1998.
2. B. Pierce, Types and Programming Languages, MIT, 2002.
3. M. Huth, M. Ryan, Logic in computer science, Cambridge, 2004.
4. J. Lambek, P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge, 1986.

Publikacje naukowe osób prowadzących zajęcia związane z tematyką modułu:

Nie podano dodatkowych publikacji

Informacje dodatkowe:

Brak