Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
215270
Бројач данашњих посета
83
Ваша интернет адреса
54.81.148.144
Време последње измене
24. 6. 2016. | 20:39:53
Тренутно време
30. 6. 2016. | 22:59:34
Месечни календар
Јун 2016
ПоУтСрЧеПеСуНе
12345
6789101112
13141516171819
20212223242526
27282930
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 (22. 2. 2016.): Упознавање са курсом. Синтакса и семантика исказне логике. Имплементација у C++-у. 1.zip
  • Трочас 2 (29. 2. 2016.): Теорема о замени и нормалне форме. Имплементација у C++-у. Еквизадовољивост и Цајтинова трансформација. 2.zip
  • Трочас 3 (9. 3. 2016.): SAT проблем и SAT решавачи. Поређење различитих алгоритама (метод истинитоносних таблица, претрага са враћањем (backtracking), DPLL алгоритам). Имплементација у C++-у. CDCL SAT решавачи (информативно). 3.zip
  • Трочас 4 (16. 3. 2016.): Примене SAT решавача. 4.zip
  • Трочас 5 (23. 3. 2016.): Природна дедукција у исказној логици. Интерактивни доказивач теорема Isabelle. 5.zip
  • Трочас 6 (30. 3. 2016.): Синтакса логике првог реда. 6.zip
  • Трочас 7 (13. 4. 2016.): Семантика логике првог реда. Нормалне форме. Сколемизација. 7.zip
  • Трочас 8 (20. 4. 2016.): Свођење формуле на еквизадовољиви клаузални облик. Унификација. 8.zip
  • Трочас 9 (27. 4. 2016.): Метод резолуције. Једнакосна логика и нормални модели. Парамодулација. 9.zip
  • Трочас 10 (4. 5. 2016.): Резолуцијски решавачи. Vampire доказивач теорема. Једнакосно резоновање. Биркхофова правила. Конгруентна затворења. Алгоритам Nelson-Oppen. 10.zip
  • Трочас 11 (11. 5. 2016.): Акерманова редукција. Презаписивање. 11.zip
  • Трочас 12 (18. 5. 2016.): Фурије-Моцкинова процедура. SMT решавачи. 12.zip
  • Трочас 13 (25. 5. 2016.): Примене SMT решавача. 13.zip


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

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

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

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


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


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


Испит из аутоматског резоновања у јулском (јун2) испитном року се помера за два сата касније, због пријемног испита који се одвија истог дана пре подне. Дакле, нови термин испита је среда, 29.6. од 17 до 20 часова у рачунарским учионицама на Студентском тргу.


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