Изаберите језик:
rs rsl en
Информације и наука
Информације Наука
Настава
Опште информације Програмирање 1 Програмирање 2 Микрорачунари Увод у организацију рачунара Развој софтвера 2 Напредна архитектура рачунара Аутоматско резоновање Увод у архитектуру рачунара
Бројач посета
182123
Бројач данашњих посета
83
Ваша интернет адреса
54.226.143.14
Време последње измене
22. 5. 2015. | 10:18:54
Тренутно време
24. 5. 2015. | 23:02:25
Месечни календар
Мај 2015
ПоУтСрЧеПеСуНе
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.
  • Филип Марић. Белешке са предавања (и шири списак литературе)


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


  • Трочас 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


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


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

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

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


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