Fakultet tehničkih nauka

Predmet: Interaktivni dokazivači (17.DOM71)

Matične organizacione jedinice predmeta:
Osnovne informacije:
 
Kategorija Naučno-stručni
Uža naučna oblast Teorijska i primenjena matematika
Multidisciplinarna Da
ESPB 10
Cilj:

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

Ishod:

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.

Sadržaj:

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.

Metodologija izvođenja nastave:

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.

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