Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
245706
Бројач данашњих посета
16
Ваша интернет адреса
54.161.96.239
Време последње измене
9. 7. 2017. | 15:22:30
Тренутно време
29. 7. 2017. | 13:43:37
Месечни календар
Јул 2017
ПоУтСрЧеПеСуНе
12
3456789
10111213141516
17181920212223
24252627282930
31
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. године могу се видети овде.

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


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