Info & Research
Info Research
Teaching (in Serbian only)
Opšte informacije Programiranje 1 Programiranje 2 Mikroračunari Uvod u organizaciju računara Razvoj softvera 2 Napredna arhitektura računara Automatsko rezonovanje Uvod u arhitekturu računara
Hit counter:
163420
Your IP address:
54.227.77.237
Last modification date:
8. 7. 2014.
Current time:
19:51:19
Month calendar:
August 2014
MoTuWeThFrSaSu
123
45678910
11121314151617
18192021222324
25262728293031
XHTML 1.0 Strict validation CSS 2.1 validation
Matf
Milan Bankovic
University of Belgrade
Faculty of Mathematics
Department of Computer Science
Milan Banković
Teaching Assistant
milan@matf.bg.ac.rs



  • John Harrison. Handbook of Practical Logic and Automated Reasoning.
  • Predrag Janičić. Matematička logika u računarstvu.
  • Franz Baader, Tobias Nipkow. Term rewriting and all that.
  • Filip Marić. Beleške sa predavanja (i širi spisak literature)


Parser za iskaznu logiku i logiku prvog reda možete preuzeti ovde.


  • Tročas I (3. 3. 2014.): Upoznavanje sa kursom. Sintaksa i semantika iskazne logike. (1.cpp).
  • Tročas II (10. 3. 2014.): Logičke transformacije. Normalne forme. (2.cpp).
  • Tročas III (17. 3. 2014.): Cajtinova transformacija. SAT problem. DPLL algoritam. (3.zip).
  • Tročas IV (24. 3. 2014.): Svođenje problema na SAT. Primene SAT rešavača. (4.zip).
  • Tročas V (31. 3. 2014.): Prirodna dedukcija u iskaznoj logici. Sistem isabelle. (5.zip).
  • Tročas VI (7. 4. 2014.): Sistem isabelle (nastavak). Logika prvog reda. (6.zip).
  • Tročas VII (14. 4. 2014.): Semantika logike prvog reda. (7.zip).
  • Tročas VIII (28. 4. 2014.): Normalne forme. Skolemizacija. Unifikacija. Metod rezolucije. (8.zip).
  • Tročas IX (5. 5. 2014.): Metod rezolucije. (Primeri.)
  • Tročas X (12. 5. 2014.): Vampire rezolucioni rešavač. Jednakosna logika. Kongruentna zatvorenja. Nelson-Oppen-ov algoritam. (10.zip)
  • Tročas XI (19. 5. 2014.): Prezapisivanje. Furije-Mockinova procedura. (11.zip)
  • Tročas XII (26. 5. 2014.): SMT rešavači. (12.zip)


Zadaci sa prethodnih ispitnih rokova mogu se pogledati ovde.


Teme za seminarske radove možete pogledati na ovoj strani. Svaku temu rade dva studenta u paru. Prijave slati isključivo na mejl predmetnog asistenta. Teme će biti dodeljivane onim redom kojim se studenti budu prijavljivali. Studenti mogu predložiti i neku temu koja nije na spisku, ako ista ima smisla, biće uzeta u razmatranje. Seminarski se brani kod profesora. Za detalje o izradi seminarskog rada, obratiti se profesoru.



Rezultati kolokvijuma mogu se pogledati ovde


Rezultati praktičnog dela ispita u ispitnom roku JUN1 mogu se pogledati ovde


Rezultati praktičnog dela ispita u ispitnom roku JUN2 mogu se pogledati ovde