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:
162801
Your IP address:
54.82.217.75
Last modification date:
8. 7. 2014.
Current time:
20:41:36
Month calendar:
July 2014
MoTuWeThFrSaSu
123456
78910111213
14151617181920
21222324252627
28293031
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