Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
248654
Бројач данашњих посета
4
Ваша интернет адреса
54.225.3.207
Време последње измене
23. 9. 2017. | 17:48:15
Тренутно време
26. 9. 2017. | 00:09:24
Месечни календар
Септембар 2017
ПоУтСрЧеПеСуНе
123
45678910
11121314151617
18192021222324
252627282930
XHTML 1.0 Strict validation CSS 2.1 validation
Matf
Milan Bankovic
Универзитет у Београду
Математички факултет
Катедра за рачунарство
Милан Банковић
Асистент
milan@matf.bg.ac.rs



  • John Harrison. Handbook of Practical Logic and Automated Reasoning.
  • Предраг Јаничић. Математичка логика у рачунарству.
  • Franz Baader, Tobias Nipkow. Term rewriting and all that.
  • Biere, A., Heule, M., Van Maaren, H., Walsh, T.. Handbook of Satisfiability.
  • Филип Марић. Белешке са предавања (и шири списак литературе)


Парсер за исказну логику и логику првог реда можете преузети овде.


  • Трочас 1 (20. 2. 2017.): Упознавање са курсом. Синтакса и семантика исказне логике. Имплементација у C++-у. 1.zip
  • Трочас 2 (27. 2. 2017.): Нормалне форме. 2.zip
  • Трочас 3 (6. 3. 2017.): Цајтинова трансформација. SAT решавачи. 3.zip
  • Трочас 4 (13. 3. 2017.): Примене SAT решавача. 4.zip
  • Трочас 5 (20. 3. 2017.): Примене SAT решавача (наставак од претходне недеље).
  • Трочас 6 (27. 3. 2017.): Природна дедукција у исказној логици. Систем Isabelle. 6.zip
  • Трочас 7 (3. 4. 2017.): Природна дедукција у исказној логици (наставак са претходног часа).
  • Трочас 8 (19. 4. 2017.): Логика првог реда. Синтакса и семантика. Имплементација у C++-у. 8.zip
  • Трочас 9 (26. 4. 2017.): Нормалне форме у логици првог реда. Сколемизација. 9.zip
  • Трочас 10 (3. 5. 2017.): Унификација. Метод резолуције. 10.zip
  • Трочас 11 (8. 5. 2017.): Доказивање ваљаности формула првог реда методом резолуције. Једнакосна логика. Парамодулација у резолуцији. 11.zip
  • Трочас 12 (15. 5. 2017.): Резолуцијски решавач Vampire. Једнакосно резоновање. Биркхофова правила. Нелсон-Опенова процедура. 12.zip
  • Трочас 13 (22. 5. 2017.): Фурије-Моцкинова процедура. Увод у SMT решаваче. 13.zip
  • Трочас 14 (27. 5. 2017.): Примене SMT решавача. 14.zip
  • Приступно предавање (6. 6. 2017.): SMT решавачи. 15.zip


Решења задатака са колоквијума могу се видети овде.

Резултати колоквијума се могу видети овде.


Резултати испита у јунском року могу се видети овде.


Резултати испита у јулском року могу се видети овде.


Резултати испита у септембарском року могу се видети овде.


Резултати испита у октобарском року могу се видети овде.


Задаци за припрему колоквијума могу се погледати овде.

Задаци са колоквијума 2014. године могу се видети овде.

Задаци са колоквијума 2015. године могу се видети овде.

Задаци са колоквијума 2016. године могу се видети овде.

Задаци са претходних испитних рокова могу се погледати овде.


Теме за семинарске радове можете погледати овде. Сваку тему ради двоје студената у пару. Теме се бирају по систему "ко пре девојци", тако што мени пошаљете мејл у коме наведете назив жељене теме, као и ваша имена. У мејлу можете навести и резервну тему (или више тема, почев од најпожељније) која ће вам бити додељена уколико је тема која је ваш први избор већ заузета. Уколико неко има жељу да ради неку тему која није на списку, може је предложити професору или мени, па ћемо је узети у разматрање.