И что Зима если Январь
Выводим, что НЕ (темно и январь и холодно)
В том случае, если S1 имеет тот же вид, а S2 - факт
S2: Ak
причем Аk является одним из предикатов из S1, шаг вывода только вычеркивает Аk из S1 и получается резольвента
S: ù (A1,..., Ak-1, Ak+1,..., An)
Данный шаг вывода можно иллюстрировать следующим примером
Допуская, что НЕ (темно и зима и холодно)
И что Зима
Выводим, что: НЕ (темно и холодно)
4.5.3. Простая резолюция сверху вниз
Рассмотренные выше правила применяются на каждом шаге вывода только к двум родительским предложениям. Вместе с тем описание любой области знания содержит множество ППФ.
Рассмотрим процесс логического вывода для примера, когда знания выражаются двумя предложениями.
S2: получает (студент, стипендию) сдает (успешно, сессию, студент)
S3: сдает (успешно, сессию, студент)
Задача, которую надо решить, состоит в том, чтобы ответить на запрос
Получает ли студент стипендию?
Когда используется обычная система логического вывода, то такой вопрос представляется в виде отрицания
S: ù получает (студент, стипендию)
и система должна отвергнуть это отрицание при помощи других предложений, демонстрируя, что данное допущение ведет к противоречию.
Этот подход часто применяется в математике и называется доказательством от противного.
Теперь представим себе, что исходная логическая модель, составленная из трех предложений S1, S2,S3 поступает на вход системы логического вывода ЭВМ.
ШАГ 1
Система на первом шаге применит правило (*) к родительским предложениям S1 и S2 и получит резольвенту:
S: ù сдает (успешно, сессию, студент)
ШАГ 2
Используя правило (**) к S и S3 система выводит противоречие:
S`:
Таким образом, для доказательства противоречивости S1 S2 S3 оказалось достаточно двух шагов вывода.
Если считать, что S2 и S3 не противоречат друг другу, то они совместно противоречат S1, т. е.
подтверждают отрицание S: ù S1: ù (ù получает (студент, стипендию))
или другими словами подтверждают предложение:
Получает (студент, стипендию)
и ответом на исходную задачу является «ДА ».
Логический вывод, который порождает последовательность отрицаний, такую как (S1, S, S`) в рассмотренном примере, называется резолюцией сверху вниз.
4.5.4. Общая резолюция сверху вниз
В общем случае предикаты и ППФ в качестве термов содержат не только константы, но и переменные и функции. Рассмотрим два родительских предложения:
S1: ù получает (студент, У)
S2: получает (Х, стипендию) сдает (успешно, Z, X)
К ним непосредственно нельзя применить правило резолюции, т.к. они не содержат одинаковых предикатов в левой части импликации и в отрицании. Данные предложения содержат три переменных X, Y, Z, которые неявно универсально квантированы.
Рассмотрим первое предложение, S1, которое утверждает, что:
Для всех У студент не получает У
Причем выражение «для всех» понимается как «для всех индивидуумов из какой либо области, выбранной для интерпретации предложений». При интерпретации S1 и S2 по крайней мере один индивидуум У будет связан с именем «стипендия » и поэтому непосредственным следствием S1 является более конкретное предложение:
S1`: ù получает (студент, стипендию)
Аналогично рассматривается S2 на области интерпретации S1 и S2 и, выбирая для Х, индивидуум с именем «студент », получаем более конкретное предложение:
S2`: получает (студент, стипендию) сдает (успешно, Z, студент)
Теперь имеем два предложения S1` и S2`, которые удовлетворяют условию применимости правила резолюции, а именно наличию одинаковых предикатов в левой части импликации и в отрицании. Поэтому резольвентой S1` и S2` будет:
S: ù сдает (успешно, Z, студент)
Предикат
Получает (студент, стипендию)
называется общим примером родительских предикатов
Получает (Х, стипендию)
Получает (студент, У)
и получен с помощью унификатора вида
Q = { Х:= студент, У:= стипендия}
4.5.5. Унификаторы и примеры унификации
Унификатором называется множество присваиваний вида
Q = {X1:= t1,..., Xn:= tn}
где Хi - переменная, а ti – терм, применение которых к двум выражениям дает одинаково общие примеры.
На практике унификаторы определяют сравнивая по очереди соответствующие аргументы предикатов и выписывая те присваивания термов переменным, которые сделали бы эти аргументы одинаковыми.
Рассмотрим ряд примеров унификации (таблица 4.1):
Таблица 4.1
Примеры унификации
| Родительские предложения | Унификатор | Общий пример |
| p(5), p(5) | Q- пустое множество (не заменяется ни одна переменная) | p(5) |
| p (x), p(5) | Q = {x:=5} | p(x)Q = p(5)Q = p(5) |
| p(x), p(y) | Q = {x:=y} | p(y) |
| p(x, y), p(5, x) | Q = {x:=5, y=x} = = {x:=5, y:=5} | p(x,y)Q = p(5,x)Q = p(5,5) |
| ù p(5, x) p(x, y) ← q(x) | Q = {x:=5, y:=5} | p(5,5) резольвента: s: ù q(x)Q = ù q(s) |
4.5.6. Решение задач и извлечение ответа.
Решение задачи с использованием логического программирования разбивается на 3 этапа:
На первом этапе необходимо сформулировать наши знания и допущения о предметной области в виде множества ППФ
На втором этапе нужно выразить конкретную задачу, поставленную на предметной области, как запрос об одном или нескольких отношениях. Обычно запрос ставится как исходное отрицание.
Составление допущений и исходного запроса завершается работа программиста, цель которой - сформулировать задачу.
Третий шаг выполняется компьютером, который пытается решить задачу, строя доказательство от противного. Он строит вывод сверху вниз, начиная с исходного отрицания, и порождает последовательность отрицаний
D1, D2,..., D
Если может быть построен вывод, заканчивающийся отрицанием
Dn = (противоречие),
то этот вывод, называемый успешным выводом, сразу дает решение поставленной задачи.
Рассмотрим все эти три этапа на примере вычислительной задачи нахождения значения факториала некоторого числа.
На первом этапе необходимо в виде ППФ сформулировать наши знания о вычислении факториала, которые можно представить двумя предложениями:
S1: факториал (0,1)
S2: факториал (х,у) х>0, факториал (х-1, у), у=у х
На втором этапе конкретную задачу, например, вычисление значение факториала трех (т.е. 3!), формулируем в виде запроса как исходного отрицания:
D1: ù факториал (3, z)
На третьем этапе система логического вывода выполнит следующую последовательность этапов вывода на основе резолюции (таблица 4.2)
Таблица 4.2
Вывод на основе резолюции
| Шаг вывода | Родительские предложения | Унификатор | Отрицание (резольвента) |
| D1, S2 | Q = {x:=3, y:=z, y1:=y/x} = = {x:=3, y1:= z/3} | D2: ù факториал (2, z/3) | |
| D2, S2 | Q = {x:=2, y:=z/3, y1:=y/x} = = {x:=2, y1:= z/6} | D3: ù факториал (1, z/6) | |
| D3, S2 | Q = {x:=1, y:=z/6, y1:=y/x} = = {x:=1, y1:= z/6} | D4: ù факториал (0, z/6) | |
| D4, S1 | Q = {z/6:=1} = {z:=6} | |
Полученное на 4 шаге противоречие подтверждает отрицание D1, а стало быть вывод является успешным и дает решение:
факториал (3,z), с унификатором Q = {z:=6}
т.е. факториал (3,6)
Откуда ответ, выдаваемый системой логического вывода: z:=6