Материјали са предавања
- Тема 0: Увод у аутоматско
резоновање. Основне информације о
предмету.(слајдови)
- Тема 1: Исказна логика. Синтакса и
семантика. Нормалне форме. SAT решавачи. Метод резолуције. DP
процедура. DPLL процедура. CDCL процедура. Метод таблоа. Теорема
компактности. Примене SAT решавача (слајдови,
примери)
- Тема 2: Логика првог реда. Синтакса и
семантика. Нормалне форме. Ербранова теорема и Гилморова процедура.
Сколем-Ловенхајмова теорема и теорема компактности.
Унификација. Метод резолуције у логици првог реда. Метод таблоа.
Системи за дедукцију. Природна дедукција.
(слајдови,
примери)
- Тема 3: Логика првог реда са једнакошћу.
Нормалне интерпретације. Аксиоме једнакости. Парамодулација. Биркхофов
систем. Конгруентно затворење. Нелсон-Опенова процедура. Системи за
презаписивање термова. Заустављање и конфлуентност. Уређења презаписивања
и уређења свођења. Уређења лексикографске стазе. Кнут-Бендиксова процедура
употпуњавања. (слајдови,
примери)
- Тема 4: Теорије првог реда. Резоновање у теорији.
Фурије-Моцкинова процедура. Симплекс метод. SMT решавачи.
(слајдови,
примери)
