Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
205212
Бројач данашњих посета
7
Ваша интернет адреса
54.82.102.217
Време последње измене
22. 1. 2016. | 16:10:55
Тренутно време
7. 2. 2016. | 01:58:22
Месечни календар
Фебруар 2016
ПоУтСрЧеПеСуНе
1234567
891011121314
15161718192021
22232425262728
29
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.
  • Филип Марић. Белешке са предавања (и шири списак литературе)


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


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


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


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

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

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

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


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

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

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


Теме за семинарске радове можете погледати на овој страни. Сваку тему раде два студента у пару. Пријаве слати искључиво на мејл предметног асистента. Теме ће бити додељиване оним редом којим се студенти буду пријављивали. Студенти могу предложити и неку тему која није на списку, ако иста има смисла, биће узета у разматрање. Семинарски се брани код професора. За детаље о изради семинарског рада, обратити се професору.