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]

19.02.2024.

02. Zapisivanje raznih tvrđenja u Isabelle-u

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

26.02.2023.

§ Literatura

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