ВУЗ:
Составители:
Оглавление
1 Что такое декларативное программирование? ______________________________4
1.1 Машина фон Неймана и процедурное программирование ________________4
1.2 От процедурного к декларативному программированию _________________5
1.3 Почему следует изучать декларативное
программирование? ________________________________________________________5
2 Формальные аксиоматические теории _____________________________________8
2.1 Определение формальной теории ______________________________________8
2.2 Выводимость ________________________________________________________8
2.3 Язык первого порядка _______________________________________________11
2.3.1 Предметы и универсум ___________________________________________11
2.3.2 Предикаты и элементарные формулы _______________________________12
2.3.3 Логические связки _______________________________________________13
2.3.4 Свободные и связанные переменные ________________________________17
2.4 Теории с языком первого порядка ____________________________________18
2.4.1 Интерпретация __________________________________________________18
2.4.2 Общезначимость и непротиворечивость _____________________________19
2.4.3 Полнота, независимость и разрешимость ____________________________19
2.5 Примеры формальных теорий________________________________________20
3 Исчисление высказываний ________________________________________________23
3.1 Определение исчисления высказываний ______________________________23
3.2 Разрешимость и непротиворечивость исчисления высказываний ____23
4 Теории первого порядка __________________________________________________24
4.1 Синтаксические свойства истинности теорий с языком первого порядка _24
4.2 Определение теории первого порядка _________________________________24
4.3 Некоторые свойства теорий первого порядка __________________________25
4.4 Непротиворечивость, полнота и неразрешимость исчисления предикатов 26
5 Классические методы доказательства_____________________________________27
5.1 Использование теоремы о дедукции___________________________________28
5.2 Доказательство импликаций с помощью контропозиции ________________28
5.3 Доказательство от противного _______________________________________29
5.4 Доказательство контрпримером ______________________________________30
5.5 Математическая индукция___________________________________________30
6 Автоматическое доказательство теорем__________________________________33
6.1 Постановка задачи __________________________________________________33
6.2 Предваренная нормальная форма ____________________________________33
6.3 Сколемизация ______________________________________________________35
6.4 Конъюнктивная нормальная форма __________________________________36
6.5 Сведение к дизъюнктам _____________________________________________36
2
