Uvod u interaktivno dokazivanje teorema

prof. dr Filip Marić

dr Sana Stojanović Đurđević; Andrija Urošević

(i) Formulizacija: 10p.

(ii) Dokazi: 30p.

(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.

17.04.2024.

14.04.2024.

08.04.2024.

01.04.2024.

25.03.2024.

18.02.2024.

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.

Zapisivanje logičkih formula (nastavak). Silogizmi. Logički lavirinti.

Postavke: [Vezbe02.pdf] [Vezbe02.thy] Rešenja: [Vezbe02.pdf] [Vezbe02.thy]

26.02.2023.

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.

Programski jezik Isar i struktuirani dokazi nekih teorema algebre skupova.

Postavke: [Vezbe04.pdf] [Vezbe04.thy] Rešenja: [Vezbe04.pdf] [Vezbe04.thy]

11.03.2023.

Programski jezik Isar i struktuirani dokazi nekih osobina funkcija.

Postavke: [Vezbe05.pdf] [Vezbe05.thy] Rešenja: [Vezbe05.pdf] [Vezbe05.thy]

18.03.2023.

Programski jezik Isar i struktuirani dokazi nekih teorema u logici.

Postavke: [Vezbe06.pdf] [Vezbe06.thy] Rešenja: [Vezbe06.pdf] [Vezbe06.thy]

25.03.2023.

Programski jezik Isar i struktuirani dokazi matematičkom indukcijom.

Postavke: [Vezbe07.pdf] [Vezbe07.thy] Rešenja: [Vezbe07.pdf] [Vezbe07.thy]

01.04.2024.

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.

Algebarski tip podataka: list. Funkcije nad listama. Osnovne leme.

Postavke: [Vezbe09.pdf] [Vezbe09.thy]

22.04.2023.

Andrija Urošević