Uvod u interaktivno dokazivanje teorema

Profesor: dr. Filip Marić

Nastava u 2022. godini:

Materijali za kurs:

  • Sana Stojanovic Djurdjevic, Filip Maric: Uvod u interaktivno dokazivanje teorema - uidt.pdf (12.04.2021.)

Obaveštenje:

  • Webex snimci ce mozda uskoro postati nedostupni, otuda su svi video materijali prebaceni na enastava
  • Online konsultacije - vasa pitanja mozete uneti u naredni dokument: konsultacije
  • Obavestenja od 2021/2022 godine:
    • [14.07.2022.] Rezultati septembar1 (rezultati svih rokova) (poseban tab za rok, poseban za sumarne rezultate)
    • [06.07.2022.] Ukoliko izlazite na ispit u roku jun2, molim da popunite naredni: formular
    • Rezultati iz roka jun1 ce biti provereni nakon pristupa fakultetskim racunarima. Molim da mi se javite mail-om ako imate manji broj poena od ocekivanog (odnosno, ako se kod na ispitu NIJE CRVENEO).
    • [28.06.2022.] Rezultati jun1 (poseban tab)
    • [24.05.2022.]U narednu tabelu mozete uneti svoje github naloge i teme za seminarski: UIDT 2022 - seminarski
    • [24.05.2022.] Opis seminarskog rada i vase verzije seminarskog rada cemo cuvati na sledecem linku: github (2022)
    • [23.05.2022.] Resenja sa kolokvijuma se nalaze ovde Kolokvijum2022_resenja.thy
    • [09.05.2022.] Rezultati kolokvijuma za moju grupu (prema spisku sa hipatije)
    • [03.05.2022.] Raspored sedenja na kolokvijumu (ako neko nije u tabeli nek se javi, isto i ako neko odustaje)
    • KOLOKVIJUM CE BITI ODRZAN U SUBOTU 07.05.2022. u 10h
    • [28.04.2022.] --- Popunite narednu anketu vezanu za izbor seminarskih radova: anketa
    • Ako neko odustaje od kolokvijuma neka se javi mail-om zbog evidencije i pravljenja rasporeda sedenja
    • [28.04.2022.] --- Okacen je snimak danasnjeg casa vezbi.
    • [24.03.2022.] Ako planirate da izadjete na kolokvijum, upisite se u naredni formular: prijava za kolokvijum
  • Obavestenja od 2020/2021 godine:
    • Odabrane teme mozete uneti u naredni dokument: odabrani seminarski (generacija 2021)
    • [29.09.2021.] ---> Rezultati roka septembar 2: rezultati (ods format)
    • [23.05.2021.] Molim studente koji su uneli u tabelu seminarske sa linka imomath: balkanske olimpijade, da odaberu seminarski sa linka koji je postavljen u delu "Izrada prvog i drugog seminarskog rada": internacionalne olimpijade
    • [21.05.2021.] Poslati su pozivi za github repozitorijum studentima koji su uneli svoj github nalog u dokument (nize na sajtu), imate 7 dana da ih prihvatite. Pisite mi ako Vam poziv nije stigao. Seminarske unosite u folder uidt_2021_seminarski.
    • [19.05.2021.] Okacen je link (nize na stranici) sa kog birate seminarske zadatke kao i link na dokument u koji mozete uneti svoj github nalog kao i seminarski rad koji birate (molim vas da proverite da nije vec neko odabrao isti zadatak).
    • [08.05.2021.] --- Rezultati kolokvijuma (sa objasnjenjima): rezultati (ods format)
  • Obavestenja od 2019/2020 godine:
    • Izabrani seminarski zadatak upisite u naredni dokument: odabrani seminarski (generacija 2020).
    • [06.05.2020.] --- Od sada svoje seminarske mozete da uploadujete direktno na github. Pristup repozitorijumu su dobili studenti koji su upisali github nalog u dokument.
    • [04.05.2020.] --- napravljen je github repozitorijum u kome cete kaciti svoje seminarske radove, upisite svoj github nalog u dokument za odabrane seminarske da bih vas dodala (ako nemate nalog, prvo ga kreirajte: https://github.com)
    • Pripremni zadaci sa olimpijada mogu se naci na sledecim linkovima: internacionalne olimpijade i balkanske olimpijade.
    • [09.03.2020.] --- Primere koda sa greskama mozete uneti u sledeci dokument.

Raspodela poena:

  • Seminarski radovi:
    • Prvi seminarski rad: 10 poena
    • Drugi seminarski rad sa odbranom: 30 poena
    • Seminarski radovi se predaju i brane online
  • Pismeni ispit:
    • Prvi deo ispita (koji se sastoji od matematickog dela): 30 poena
    • Drugi deo ispita (koji se sastoji od programerskog dela): 30 poena
  • Prag: na svakoj pojedinacnoj obavezi prag je 50%
  • Ispit se polaze na racunarima na fakultetu na jedan od sledecih nacina:
    • I deo ispita (u trajanju od 2 sata, otprilike 5 zadataka)
    • II deo ispita (u trajanju od 2 sata, otprilike 5 zadataka)
    • Oba dela ispita (u trajanju od 3 sata, otprilike 8 zadataka)
    • Ako neko ko bude polagao oba dela ispita ne bude bio zadovoljan bilo kojim delom ispita, ima mogucnost da ponovi samo onaj deo ispita koji zeli (ne mora ponovo da se polaze ceo ispit).

Resenja nekih ispitnih rokova i kolokvijuma:

Izrada prvog i drugog seminarskog rada:

  • Prvi seminarski rad se sastoji od formalnog zapisivanja iskaza teoreme i svih definicija koje se koriste u iskazu teoreme. Potrebno je precizno definisati sve pojmove koje se javljaju u tvrdjenju. Nije potrebno navoditi dokaz teoreme.
  • Drugi seminarski rad se sastoji od zapisivanja kompletnog resenja jednog problema u Isabelle-u. Drugi seminarski moze biti nastavak prvog seminarskog rada, ali to nije obavezno.
  • Pogledajte profesorovo predavanje koje je okaceno u ponedeljak 27.04.2020. (proslogodisnje predavanje)
  • Teme za prvi seminarski mozete izabrati iz materijala koji su korisceni kao pripremni zadaci za olimpijade. U materijalima sa profesorovog sajta mozete pogledati nekoliko vec uradjenih zadataka sa olimpijada, da biste stekli uvid u to kako treba da izgleda.
  • Sve verzije seminarskih radova cemo cuvati online, preko git repozitorijuma. Potrebno je da kreirate svoj nalog i da upisete vas username (u dokument za izabrane seminarske) da bih vas dodala u repozitorijum. Dakle, ne morate da cekate da imate finalnu verziju resenja seminarskog vec mozete kaciti svoj seminarski od pocetka da bismo profesor i ja mogli da pratimo kako napredujete.
  • Seminarski zadaci se biraju iz dokumenata kreiranih za pripremne zadatke sa olimpijada: internacionalne olimpijade.

Odabrani snimci sa vežbi (generacija 2020/2021 i generacija 2021/2022):

  • SVI SNIMCI SE MOGU NACI NA ADRESI: enastava
  • Zbog politike Webex-a moguce je da ce naredni linkovi biti nedostupni ubrzo
    • [2021] Snimak sa XII casa vezbi: Izracunavanje izraza prefiksno zadatog izraza i kreiranje stek masine: 4nFetbmn
  • [2021] Snimak sa XI casa vezbi: Ugradjen tip listi i kreiranje novog tipa lista: 3EkPxDSr
  • XI cas vezbi (05.05.2022.): vezbanje gradiva vezano za definisanje korisnickih funkcija i dokazivanje njihovih svojstava
  • Snimak X casa vezbi (28.04.2022.): Uvodjenje novih tipova podataka, definicije, skracenice i dokazivanje svojstava korisnickih funkcija (od 26 minuta, do tada objasnjenje kolokvijuma i seminarskog) PcxemNM2
    • [2021] Snimak X casa vezbi: Gradjenje skupa prirodnih brojeva i operacija nad njim (od 17 min, do tada objasnjenje seminarskog): 9xWEixnp
  • [2021] Snimak IX casa vezbi: Matematicka indukcija - rad sa matricama i indukcija pocevsi od pozitivnog broja (od 18 min, do tada objasnjenje kolokvijuma): 7iXvsd29
  • [2021] Snimak VIII casa vezbi: Prirodni brojevi i matematicka indukcija: zPVvVgw9
  • [2021] Snimak VII casa vezbi: Programski jezik Isar - funkcije, kvantifikatori, klasicna logika, dokazi po slucajevima: HinPTW33
  • [2021]Snimak VI casa vezbi: Prirodna dedukcija - klasicna logika, Isar - rad sa funkcijama wTRZnig3
  • [2021] Snimak V casa vezbi: Programski jezik Isar, rad sa skupovimaMhYmPAG3
  • Snimak IV casa vezbi (17.03.2022): Logika prvog reda, kvantifikatori i pravilo iskljucenja treceg (webex link: Yebnm2Mp)
  • [2021] Snimak III casa vezbi: Prirodna dedukcija (webex link: XhPpHfF8)
  • Snimak II casa vezbi (03.03.2022): zapisivanje formula logike prvog reda, silogizmi, logicki lavirinti (webex link: kPqJAVx3)
  • Snimak I casa vezbi (24.02.2022): Osnove o interaktivnom dokazivanju teorema i o dokazivacu Isabelle, primer jednostavne matematicke teorije, zapisivanje formula logike prvog reda (webex link: Pmgf3vtf)

Teme obrađene na vežbama (generacija 2019/2020):

Teme obrađene na vežbama (generacija 2018/2019):