Ivan Drecun

Matematički fakultet, Univerzitet u Beogradu
Katedra za računarstvo i informatiku

Automatsko rezonovanje


Profesor: Milan Banković
Asistent: Ivan Drecun

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)
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