 |
Автоматическое доказательство теорем методом резолюций
|
|
|
|
Алгоритм, который проверяет соотношение G |-T S для формулы S, множества формул G и теории T называется алгоритмом автоматического доказательства теорем. Для прикладных исчислений первого порядка такое доказательство проводится методом резолюций.
Метод резолюций работает со стандартной формой формул, называемой предложениями. Предложением называется бескванторная дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений по следующему алгоритму.
1. Построить предварённую нормальную форму формулы. Напомним, что для этого нужно:
a) преобразовать формулу к приведённому виду, т.е. исключить операцию ® и спустить операцию отрицания до атомарных формул;
b) провести разделение связанных переменных;
c) вынести операции связывания переменных в начало формулы.
2. Преобразовать предварённую нормальную форму в предклазуальную, т.е. привести матрицу U нормальной формы к КНФ.
3. Провести сколемизацию нормальной формы (построить клазуальную нормальную форму, исключив операции связывания переменных).
4. Удалить операции Ù (дизъюнкции клазуальной нормальной формы составят искомое множество предложений).
Далее к предложениям, полученным из формул множества G и из формулы Ø S, применяется правило резолюции.
Определение. Пусть 
– предложения исчисления предикатов, такие что 
, 
, а атомарные формулы 
унифицируемы наиболее общим унификатором t. Правило вывода
называется правилом резолюции исчисления предикатов, предложения 
– резольвируемыми, а 
– резольвентой.
Таким образом, множество предложений будет являться противоречивым, если в результате последовательного применения правила резолюции, получим пустую формулу, которую будем обозначать š. Действительно, если резольвента пуста, то резольвируемые предложения – взаимно противоположные высказывания и система предложений противоречива.
|
|
|
Работа метода резолюций может иметь следующие варианты результатов:
1) на очередном шаге получено пустое предложение и, следовательно, формула S является следствием G (теорема 
доказана);
2) если во множестве предложений нет новых резольвируемых предложений, то теорема опровергнута;
3) множество предложений постоянно пополняется новыми предложениями (зацикливание), что означает, что средств данной теории недостаточно ни для того, чтобы доказать теорему, ни для того, чтобы её опровергнуть.
Представим алгоритм работы метода резолюций на языке описания алгоритмов. Результат 1 – если S выводимо из G, 0 – в противном случае. Обозначим M – множество предложений, C – множество предложений, полученное из G и Ø S. Функция choose выполняет выбор резольвируемых предложений, R – вычисляет резольвенту.
while ÿÏ C
begin choose (
)
if 
then return 0
R(
)
end
return 1
В качестве примера рассмотрим проверку выводимо ли утверждение дядя(cергей, Y) из множества предложений «Родственные отношения» (см. задания для РПР).
Добавим в множество предикат
дядя(X, Y) X – дядя Y
и правило вывода
дядя(X, Y) род(Z, Y) Ù брат(X, Z).
Запишем это правило в виде предложения
82. дядя(X, Y) Ú Ø род(Z, Y) Ú Øбрат(X, Z).
Добавим в множество предложений отрицание проверяемого утверждения
83. Ø дядя(cергей, Y)
и будем применять к предложениям множества правило резолюции.
| 84. дядя(сергей, Y) Ú Ø род(Z, Y) Ú Øбрат(сергей, Z) 85. Ø род(Z, Y) Ú Øбрат(сергей, Z) 86. брат(сергей, Z) Ú Øрод(W, сергей) Ú Øрод(W, Z) Ú Øмуж(сергей) 87. брат(сергей, Z) Ú Øрод(W, сергей) Ú Øрод(W, Z) 88. род(иван, сергей) Ú Øотец(иван, сергей) 89. род(иван, сергей) 90. брат(сергей, Z) Ú Øрод(иван, сергей) Ú Ú Øрод(иван, Z) 91. брат(сергей, Z) Ú Øрод(иван, Z) 92. род(иван, ольга) Ú Øотец(иван, ольга) 93. род(иван, ольга) 94. брат(сергей, ольга) Ú Øрод(иван, ольга) 95. брат(сергей, ольга) 96. Ø род(ольга, Y) Ú Øбрат(сергей, ольга) 97. Ø род(ольга, Y) 98. род(ольга, павел) Ú Ø мать(ольга,павел) 99. род(ольга, павел) 100. Ø род(ольга, павел) 101. ÿ | X=сергей (82) R (83, 84) X=сергей, Y=Z, Z=W (80) R (86, 4) X=иван, Y=сергей (76) R (88, 38) W=иван (87) R (89, 90) X=иван, Y=ольга (76) R (92, 37) Z=ольга (91) R (93, 94) Z=ольга (87) R (95, 96) X=ольга, Y=павел (77) R (98, 68) Y=павел (97) R (99, 100) |
Таким образом, предложение дядя(cергей,Y) выводимо из заданного множества предложений при Y=павел.
|
|
|
Контрольные вопросы и задания
Библиографический список
Основной
1. Судоплатов, С. В. Математическая логика и теория алгоритмов [Текст]: учебник для студ. вузов (гриф МО) / С. В. Судоплатов, Е. В. Овчинникова. - М.; Новосибирск: ИНФРА - М; НГТУ, 2004. - 224 с.
2. Новиков, Ф. А. Дискретная математика для программистов [Текст]: учебное пособие для студ. вузов (гриф МО) / Ф. А. Новиков. - 2-е изд. - СПб.: ПИТЕР, 2006. - 364 с.
3. Лавров, И.А. Задачи по теории множеств, математической логике и теории алгоритмов [Текст] / И.А. Лавров, Л.Л. Максимова - М.: Физматлит, 2002. - 256 с.
4. Верещагин, Н.К. Вводный курс математической логики: учебное пособие / Н.К. Верещагин, В.А. Успенский, В.Е Плиско. – ФИЗМАТЛИТ, 2007. – 126 с. (http://www.iprbookshop.ru)
Дополнительный
5. Кузнецов, О.П. Дискретная математика для инженеров [Текст]: учебник для вузов (гриф Пр. / О.П. Кузнецов - 5-е изд., стер. - СПб.: Лань, 2007. - 400 с.
6. Эдельман, С.Л. Математическая логика [Текст]: учебное пособие для ин-тов / С.Л. Эдельман - М.: Высш. школа, 1975. - 176 с. с ил.
Электронное издание
ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ
Методические указания к практическим занятиям
Для студентов, обучающихся по направлениям
09.03.02 – “Информационные системы и технологии”,
очной формы обучения
Составители БУГАЕВ Юрий Владимирович,
ШУРУПОВА Ирина Юрьевна
Подписано в печать..201. Формат 60х84 1/16
Усл. печ. л.. Тираж экз. Заказ С-
ФГБОУ ВО “Воронежский государственный университет инженерных технологий”
|
|
|
(ФГБОУ ВО “ВГУИТ”)
Отдел полиграфии ФГБОУ ВО “ВГУИТ”
Адрес университета и отдела полиграфии:
394036, Воронеж, пр. Революции, 19
|
|
|
