Fakultet tehničkih nauka

Predmet: Interaktivni dokazivači (17.DOM71)

Osnovne informacije:
 
Kategorija Naučno-stručni
Uža naučna oblast
  • Primenjene računarske nauke i informatika
  • Teorijska i primenjena matematika
ESPB 10

Sticanje znanja i praktičan rad sa interaktivnim dokazivačima COQ, ISABELL/HOL. Uključivanje studenta u naučno-istraživački rad.

Poznavanje teorijskih osnova i praktičnog rada sa interaktivnim dokazivačima teorema. Uključivanje u aktuelna istraživanja u domenu interaktivnih dokazivača, po izboru studenta, a u saradnji sa naučnicima iz zemlje i inostranstva.

Teoretske osnove interaktivnih dokazivača. Uvodni pojmovi iz teorije tipova: tipovi, termi. Razni tipski sistemi. Tipski sistem sa osnovnim (prostim) tipom. Osnovne definicje i osobine. Konfluentnost i teoreme o normalizacijama dokaza. Polimorfni tipski sistem. Teorema o jakoj normalizaciji, njen dokaz i značaj kao primer Gedelove rečenice. Tipski sistemi sa zavisnim tipovima. Teorija konstrukcija (Coquand). Uvod u osnovne pojmove interaktivnog dokazivanja teorema. Dokazivači teorema: COQ i ISABELLE.

Na predavanjima se izlaže teoretski deo gradiva propraćen karakterističnim primerima radi lakšeg razumevanja gradiva. Student samostalno proučava dodatnu literaturu i diskutuje je sa nastavnikom na konsultacijama.

Autori Naziv Godina Izdavač Jezik
Zoran Ognjanović, Silvia Gilezan Teorijsko računarstvo 2018 Srpski jezik
Benjamin Pierce Software Foundations 2018 https://softwarefoundations.cis.upenn.edu/current/index.html Engleski
COQ Team The COQ Proof Assitant 2018 https://coq.inria.fr/ Engleski
Nipkow, T., Paulson, L., Wenzel, M. Isabelle/HOL : A Proof Assistant for Higher-Order Logic 2002 Springer, Berlin Engleski
Predmetna aktivnost Predispitna Obavezna Broj poena
Predmetna aktivnost
Usmeni deo ispita
Predispitna
Ne
Obavezna
Da
Broj poena
50.00
Predmetna aktivnost
Seminarski rad
Predispitna
Da
Obavezna
Da
Broj poena
50.00
Predavanja
Studijski istraživački rad