Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
216895
Бројач данашњих посета
14
Ваша интернет адреса
54.146.4.250
Време последње измене
5. 7. 2016. | 12:54:33
Тренутно време
27. 7. 2016. | 08:25:04
Месечни календар
Јул 2016
ПоУтСрЧеПеСуНе
123
45678910
11121314151617
18192021222324
25262728293031
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) року могу се видети овде.


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