Andrija Urošević
Lična strana Kursevi Kontakt

Uvod u interaktivno dokazivanje teorema

§ Osnovne informacije

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

§ Obaveštenja

Ispitni rok jun1 će se održati u nedelju 21.09. od 13č. Izlazak na ispit potvrdite mejlom.

16.09.2025.

Rezultati ispita u svim ispitnim rokovima podeljeni po karticama.

11.08.2025.

Incijalna prijava za projekat. Obavezno popuniti do 15.08.2024.

15.08.2024.

Zulip chat

01.04.2024.

Preuzmite i instalirajte Isabelle: Isabelle instalacija.

18.02.2024.

Srećano interaktivno dokazivanje uz Isabelle!

18.02.2024.

§ Č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] Rešenja: [Vezbe02.pdf] [Vezbe02.thy]

26.02.2023.

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]

04.03.2023.

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]

11.03.2023.

05. Jezik Isar i struktuirani dokazi

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

18.03.2023.

06. Jezik Isar i struktuirani dokazi

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

25.03.2023.

07. Jezik Isar i matematička indukcija

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

01.04.2024.

08. Zasnivanje prirodnih brojeva

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

18.04.2023.

09. Liste

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

22.04.2023.

10. Stabla

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

13.05.2024.

11. Stek mašina

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

20.05.2023.

12. Razni zadaci

Desni linearni lanac. Fold-ovanje nad drvetom. Odsecanje liste.
Postavke: [Vezbe12.pdf] [Vezbe12.thy] Rešenja: [Vezbe12.pdf] [Vezbe12.thy]

27.05.2023.

§ Literatura

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