Andrija Urošević
Lična strana Kursevi Kontakt

Uvod u interaktivno dokazivanje teorema

§ Osnovne informacije

Predavanja:
dr Filip Marić
Vežbe:
dr Sana Stojanović Đurđević; Andrija Urošević
Obaveze studenata:
Projekat: 40p
(i) Formulizacija: 10p.
(ii) Dokazi: 30p.
Praktični ispit: 60p
(i) Matematički deo: 30p (prag 15p). Polaže se u kolokvijumskoj nedelji ili u ispitnom roku. Gradivo obuhvata sve do 200. str.
(ii) Programerski deo: 30p (prag 15p). Polaže se u ispitnom roku. Gradivo obuhvata od 201. do 320. str.

§ Obaveštenja

• Rezultati ukupno.

24.09.2023.

• Rezultati ispita [sep2] sa komentarima.

24.09.2023.

Prijava za ispit [sep2] do ponedeljka, 18.09.2023. 17:00.

17.09.2023.

Rezultati ispita [sep1] sa komentarima.

12.09.2023.

Prijava za ispit [sep1] do srede, 10.09.2023. 17:00.

06.09.2023.

Rezultati ispita [jun2] sa komentarima.

29.06.2023.

Prijava za ispit [jun2] do četvrtka, 22.06.2023. 17:00.

19.06.2023.

Rezultati ispita [jun1] sa komentarima.

16.06.2023.

Unesite svoj Github nalog preko koga ćete raditi projekat: upitnik.

14.06.2023.

Raspored sedenja [jun1].

14.06.2023.

Prijava za ispit [jun1] do srede, 14.06.2023. 17:00.

09.06.2023.

Rezultati kolokvijuma (sa komentarima). Uvid u radove kod profesorke Sane.

28.04.2023.

Rešenja kolokvijuma: [klk2023.pdf] [klk2023.thy].

26.04.2023.

Kolokvijum će se održati 25.04.2023. u 13:30. Raspored sedenja.

13.04.2023.

Obavezno se prijavite za projekat do 20.04.2023: upitnik.

12.04.2023.

Ukoliko planirate da izađete na kolokvijum popunite upitnik.

29.03.2023.

Preuzmite i instalirajte Isabelle: Isabelle instalacija.

14.02.2023.

Srećan početak semestra i interaktivno dokazivanje uz Isabelle!

13.02.2023.

§ Časovi

01. Uvod u interaktivni dokazivač Isabelle

O interaktivnom dokazivanju. Primer jednostavne Isabelle teorije. Zapisivanje logičkih formula.
Postavke: [Vezbe01.pdf] [Vezbe01.thy] Rešenja: [Vezbe01.pdf] [Vezbe01.thy]

21.02.2023.

02. Zapisivanje raznih tvrđenja u Isabelle-u

Zapisivanje logičkih formula (nastavak). Silogizmi. Logički lavirinti.
Postavke: [Vezbe02.pdf] [Vezbe02.thy] Rešenja: [Vezbe02.pdf] [Vezbe02.thy]

28.02.2023.

03. Prirodna dedukcija u Isabelle-u

Intuicionistička pravila uvođenja i eliminacije prirodne dedukcije u iskaznoj logici.
Postavke: [Vezbe03.pdf] [Vezbe03.thy] Rešenja: [Vezbe03.pdf] [Vezbe03.thy]

07.03.2023.

04. Prirodna dedukcija u Isabelle-u

Intuicionistička pravila uvođenja i eliminacije prirodne dedukcije u logici provog reda. Klasična pravila.
Postavke: [Vezbe04.pdf] [Vezbe04.thy] Rešenja: [Vezbe04.pdf] [Vezbe04.thy]

14.03.2023.

05. Jezik Isar i struktuirani dokazi

Programski jezik Isar i struktuirani dokazi nekih teorema algebre skupova.
Postavke: [Vezbe05.pdf] [Vezbe05.thy] Rešenja: [Vezbe05.pdf] [Vezbe05.thy]

21.03.2023.

06. Jezik Isar i struktuirani dokazi

Programski jezik Isar i struktuirani dokazi nekih osobina funkcija.
Postavke: [Vezbe06.pdf] [Vezbe06.thy] Rešenja: [Vezbe06.pdf] [Vezbe06.thy]

28.03.2023.

07. Jezik Isar i struktuirani dokazi

Programski jezik Isar i struktuirani dokazi nekih teorema u logici.
Postavke: [Vezbe07.pdf] [Vezbe07.thy] Rešenja: [Vezbe07.pdf] [Vezbe07.thy]

04.04.2023.

08. Jezik Isar i matematička indukcija

Programski jezik Isar i struktuirani dokazi matematičkom indukcijom.
Postavke: [Vezbe08.pdf] [Vezbe08.thy] Rešenja: [Vezbe08.pdf] [Vezbe08.thy]

11.04.2023.

09. Zasnivanje prirodnih brojeva

Algebarski tip podataka: prirodni. Funkcije sabiranja, množenja i stepenovanja. Osnovne leme.
Postavke: [Vezbe09.pdf] [Vezbe09.thy] Rešenja: [Vezbe09.pdf] [Vezbe09.thy]

18.04.2023.

10. Liste

Algebarski tip podataka: list. Funkcije nad listama. Osnovne leme.
Postavke: [Vezbe10.pdf] [Vezbe10.thy] Rešenja: [Vezbe10.pdf] [Vezbe10.thy]

03.05.2023.

11. Stabla

Algebarski tip podataka: drvo. Funkcije nad stablima. Osnovne leme.
Postavke: [Vezbe11.pdf] [Vezbe11.thy] Rešenja: [Vezbe11.pdf] [Vezbe11.thy]

09.05.2023.

12. Stek mašina

Prefiksno zadati izraz. Generisanje koda za stek mašinu. Izvršavanje programa nad stek mašinom.
Postavke: [Vezbe12.pdf] [Vezbe12.thy] Rešenja: [Vezbe12.pdf] [Vezbe12.thy]

16.05.2023.

§ Literatura

Sana Stojanović Đurđević, Filip Marić: Uvod u interaktivno dokazivanje teorema