Ivan Drecun @ Matematički fakultet

Automatsko rezonovanje

Profesor: Milan Banković
Asistent: Ivan Drecun

Važne informacije

Rezultate ispita u roku septembar 1 možete pronaći ovde. Uvid u radove je moguć putem mejla, najkasnije 17.10. u 23:59.

Rezultate ispita u roku jun 2 možete pronaći ovde.

Rezultate ispita u roku jun 1 možete pronaći ovde.

Rezultate ispita u roku januar 2 možete pronaći ovde.

Rezultate ispita u roku januar 1 možete pronaći ovde.

Obaveze na predmetu

Predispitne obaveze se sastoje iz domaćih zadataka, teorijskih testova i projekta. Termin za predaju svakog domaćeg zadatka objavljuje se na ovoj stranici.

Završni ispit se sastoji iz praktičnog i usmenog dela.

Za više detalja pogledati ovde.

Predispitne obaveze	Domaći zadaci	10 poena
	Teorijski testovi	10 poena
	Projekat	20 poena (prag 1 poen)
Završni ispit	Praktični deo	30 poena (prag 12 poena)
Završni ispit	Usmeni deo	30 poena (prag 12 poena)

Vežbe

Kodove sa vežbi možete pronaći ovde.

Skriptu kolege Ognjena Kocića možete pronaći ovde. U skripti je upotrebljen drugačiji pristup implementaciji struktura podataka za predstavljanje formula od onog na vežbama. Na ispitu je dozvoljena upotreba bilo kog od ta dva pristupa.

#	Tema	Snimak
1	Iskazna logika
2	Normalne forme u iskaznoj logici
3	Implementacija SAT rešavača
4	Vežbanje zadataka
5	Primene SAT rešavača
6	Logika prvog reda
7	Normalne forme u logici prvog reda
8	Unifikacija
9	Rezolucija u logici prvog reda
10	Primene rezolucijskog rešavača
11	Primene SMT rešavača

Arhiva

Tema	Napomena	Snimak
Rezonovanje u odabranim teorijama	Obrađeno 2023. godine, više se ne prelazi na časovima vežbi.

Kursevi

Arhiva

Kontakt

Ime	Ivan Drecun
Email	ivan.drecun@matf.bg.ac.rs
Konsultacije	Dogovor putem mejla
CV	Srpski \| English