Ivan Drecun

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

Automatsko rezonovanje


Profesor: Milan Banković
Asistent: Ivan Drecun

Važne informacije

Časovi vežbi u prvoj nedelji semestra (utorak 20.2.) neće biti održani.

Obaveze na predmetu

Predispitne obaveze se sastoje iz domaćih zadataka, teorijskih testova i projekta. Domaći zadaci se zadaju za svaku temu obrađenu na vežbama. 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 10 poena)
Usmeni deo 30 poena (prag 10 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 Rezonovanje u odabranim teorijama
12 Primene SMT rešavača