Fakultet tehničkih nauka

Predmet: Uvod u interaktivne dokazivače (17.0M513)

Matične organizacione jedinice predmeta: Departman za opšte discipline u tehnici
Osnovne informacije:
 
Kategorija Stručno-aplikativni
Uža naučna oblast Teorijska i primenjena matematika
ESPB 5

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

Poznavanje osnovnih pojmova i rezultata funkcionalnih programskih jezika i dokazivača teorema. Uključivanje u istraživanje u užoj oblasti iz odredjenih oblasti iz logike, 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. Teorem o jakoj normalizaciji, njen dokaz i značaj kao primer Gedelove rečenice. Tipski sistemi sa zavsnim 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
The COQ Proof Assitant : 2018 (online http://coq.inria.fr/) Engleski
L. C. Paulson, Isabelle: A Generic Theorem Prover 1994 Springer-Verlag, Berlin Engleski
B. Pierece: Software Foundation Software Foundation 2004 (online http://www.cis.upenn.edu/~bcpierce/sf/) Engleski
Predmetna aktivnost Predispitna Obavezna Broj poena
Predmetna aktivnost
Prisustvo na vežbama
Predispitna
Da
Obavezna
Da
Broj poena
2.00
Predmetna aktivnost
Teorijski deo ispita
Predispitna
Ne
Obavezna
Da
Broj poena
50.00
Predmetna aktivnost
Seminarski rad
Predispitna
Da
Obavezna
Da
Broj poena
45.00
Predmetna aktivnost
Prisustvo na predavanjima
Predispitna
Da
Obavezna
Da
Broj poena
3.00
Predavanja
Predavanja
Auditorne vežbe
Računarske vežbe
Računarske vežbe