Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
242565
Бројач данашњих посета
43
Ваша интернет адреса
54.196.107.247
Време последње измене
24. 5. 2017. | 19:10:57
Тренутно време
27. 5. 2017. | 23:00:08
Месечни календар
Мај 2017
ПоУтСрЧеПеСуНе
1234567
891011121314
15161718192021
22232425262728
293031
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


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

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


Испит у јунском року биће одржан у само једном термину за студенте свих група -- 16.6.2017. од 14 часова на Тргу. Испит неће бити одржан у другом термину који је наведен у распореду (20.6.).


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

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

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

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

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


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