Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара / Паралелни алгоритми Аутоматско резоновање Увод у архитектуру рачунара
Важне локације
Универзитет у Београду Математички факултет Катедра за рачунарство и информатику Група за аутоматско резоновање (АРГО)
Бројач посета
211035
Бројач данашњих посета
20
Ваша интернет адреса
54.82.20.59
Време последње измене
27. 4. 2016. | 20:23:14
Тренутно време
1. 5. 2016. | 15:36:41
Месечни календар
Мај 2016
ПоУтСрЧеПеСуНе
1
2345678
9101112131415
16171819202122
23242526272829
3031
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


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

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

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

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


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


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