- •Математическая логика
- •Раздел I. Алгебра высказываний
- •1. Высказывания и операции над ними. Формулы
- •2. Следование, эквивалентность и преобразование формул
- •3. Использование законов логики в доказательстве теорем и построении схем
- •Преобразуем эту формулу, используя соответствующие эквивалентности u
- •4. Булевы функции
- •5. Нормальные формы
- •5. Полные системы операций. Алгебра Жегалкина
- •6. Выводимость
- •Раздел II. Алгебра предикатов
- •1. Предикат. Операции над предикатами.
- •2. Модель. Формула алгебры предикатов сигнатуры .
- •3. Формулы алгебры предикатов
- •Основные общезначимости алгебры предикатов
- •Раздел 3. Логические исчисления
- •1. Определение формального исчисления
- •2. Исчисление высказываний ив.
- •3. Отношение эквивалентности в ив
- •4. Исчисление секвенций ис.
- •Исчисления предикатов ип (ипс).
- •Прикладные исчисления предикатов.
- •Автоматическое доказательство теорем
- •Теория алгоритмов
- •Машины Тьюринга
- •2. Рекурсивные функции
- •3. Временная сложность алгоритма. Классы p и np.
- •4. Полиномиальная сводимость. Np-полные языки и задачи.
Автоматическое доказательство теорем
Автоматическое доказательство теорем является основой логического программирования, одним из способов построения систем искусственного интеллекта.
Алгоритм, который проверяет соотношение |- S для формулы S, множества формул и теории называется алгоритмом автоматического доказательства теорем.
Для достаточно простых формальных теорий, например, прикладных исчислений первого порядка такой алгоритм существует. Автоматическое доказательство проводится методом резолюций, в основе которого лежит способ доказательства от противного. Часто логическим программированием называют автоматическое доказательство методом резолюций, однако этот метод лишь наиболее разработанный его частный случай.
Теорема 7.1. Если , S |- F, где F – любое противоречие, то |- S.
Доказательство. Если , S |- F, то (S) |- F, так как (S) |- и (S) |- S. Следовательно, |- (S) F. Так как
(S) F ,
то |- и, следовательно, |- S.
Метод резолюций работает со стандартной формой формул, называемой предложениями. Предложением называется бескванторная дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений по следующему алгоритму.
Построить предварённую нормальную форму формулы. Напомним, что для этого нужно:
преобразовать формулу к приведённому виду, т.е. исключить операцию и спустить операцию отрицания до атомарных формул;
провести разделение связанных переменных;
вынести операции связывания переменных в начало формулы.
Преобразовать предварённую нормальную форму в предклазуальную, т.е. привести матрицу U нормальной формы к КНФ.
Провести сколемизацию нормальной формы (построить клазуальную нормальную форму, исключив операции связывания переменных).
Удалить операции (дизъюнкции клазуальной нормальной формы составят искомое множество предложений).
Далее к предложениям, полученным из формул множества и из формулы S, применяется правило резолюции. Сформулируем это правило для исчисления высказываний, а, затем, обобщим его для исчисления предикатов.
Определение. Пусть – предложения исчисления высказываний, такие что,. Правило вывода
называется правилом резолюции исчисления высказываний, предложения – резольвируемыми, а– резольвентой.
Замечание. Многие рассмотренные ранее правила вывода являются частными случаями правила резолюции. Например, основное правило исчисления ИВ – правило заключения можно представить в виде .
Таким образом, множество предложений будет являться противоречивым, если в результате последовательного применения правила резолюции, получим пустую формулу, которую будем обозначать . Действительно, если резольвента пуста, то резольвируемые предложения – взаимно противоположные высказывания и система предложений противоречива.
Задание 1. Доказать методом резолюций |-.
Решение. В данном примере – пусто, . Преобразуем формулув множество предложений.
A
A
Применив к предложениям 1, 3 правило резолюции, получим пустую формулу, то есть противоречие. Следовательно, формула S является выводимой из пустого множества посылок или теоремой рассматриваемой теории.
Для того чтобы сформулировать правило резолюции для исчисления предикатов введём понятие унификатора.
Определение. Подстановкой сигнатуры называется конечное множество вида , где– терм сигнатуры, отличный от переменных и все переменныеразличны.
Например, множества иявляются подстановками сигнатуры.
Пусть U – формула, а – подстановка сигнатуры . Обозначим через формулу, полученную заменой всех вхожденийна термы.
Определение. Подстановка сигнатуры называется унификатором для множества формул сигнатуры, если . Множество формулсигнатуры, называется унифицируемым, если для него существует унификатор сигнатуры .
Например, множество формул сигнатурыунифицируемо, так как подстановкаявляется его унификатором.
Определение. Пусть и– подстановки сигнатуры. Композицией подстановок и (обозначается ) называется подстановка, которая получается из множества вычеркиванием всех элементов, для которых, и всех элементов, для которых.
Пример. Пусть ,. Тогда=, а так каки, то.
Определение. Унификатор для множества формул сигнатуры называется наиболее общим унификатором (НОУ), если для каждого унификатора сигнатуры этого множества существует подстановка сигнатуры такая, что .
Так для множества наиболее общим унификатором является подстановка.
Определение. Пусть – предложения исчисления предикатов, такие что,, а атомарные формулыунифицируемы наиболее общим унификатором. Правило вывода
называется правилом резолюции исчисления предикатов.
Задание 2. Проверить G |-, где
: ,,,.
Решение. Выпишем множество предложений , S, пронумеровав их.
Далее будем добавлять предложения в это множество, применяя правило резолюции с возможной предварительной унификацией. Рядом с новым предложением будем указывать способ его получения (правило резолюции или унификация) и номера предложений, к которым он применялся.
R (1, 5)
(2, 6)
R (6, 7)
(4, 8)
R (8, 9)
Следовательно, G |-.
Работа метода резолюций может иметь следующие варианты результатов:
на очередном шаге получено пустое предложение и, следовательно, формула S является следствием (теорема доказана);
если во множестве предложений нет новых резольвируемых предложений, то теорема опровергнута;
множество предложений постоянно пополняется новыми предложениями (зацикливание), что означает, что средств данной теории недостаточно ни для того, чтобы доказать теорему, ни для того, чтобы её опровергнуть.
Представим алгоритм работы метода резолюций на языке описания алгоритмов. Результат 1 – если S выводимо из , 0 – в противном случае. Обозначим M – множество предложений, C – множество предложений, полученное из и S. Функция choose выполняет выбор резольвируемых предложений, R – вычисляет резольвенту.
while C
begin choose ()
if then return 0
R()
end
return 1