Andrija Urošević
Lična strana Kursevi Kontakt

Uvod u interaktivno dokazivanje teorema

§ Osnovne informacije

Predavanja:
prof. dr Filip Marić
Vežbe:
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.
(ii) Programerski deo: 30p (prag 15p). Polaže se u ispitnom roku.

§ Obaveštenja

Zulip chat. Pozivnicu ste dobili na mejl.

23.03.2026.

Preuzmite i instalirajte Isabelle: Isabelle instalacija.

23.03.2026.

Srećano interaktivno dokazivanje uz Isabelle!

23.03.2026.

§ Č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]

23.03.2026.

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]

30.03.2026.

03. Prirodna dedukcija u Isabelle-u

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

06.04.2026.

04. Jezik Isar i struktuirani dokazi

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

20.04.2026.

05. Jezik Isar i struktuirani dokazi

Programski jezik Isar i struktuirani dokazi nekih osobina funkcija.
Postavke: [Vezbe05.pdf] [Vezbe05.thy]

27.04.2026.

§ Literatura

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