4.4. Вывод на основе правила резолюции

Правило резолюции (или резолюция) уже рассматривалось во второй главе. Это правило гласит, что из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая — его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания. Резолюция записывалась в следующем виде:

В логике предикатов первого порядка она выглядит так же. Формулы а, Р, у в ней являются формулами этой логики. Введем по аналогии с обобщенным правилом модус поненс обобщенное правило резолюции, или обобщенную резолюцию:

Здесь обозначает литерал, такой, - что при при Аналогичный смысл имеет символ в литерале Подстановка означает формулу, получающуюся из формулы результате подстановки 8 во все ее атомы. Суть обобщенного Правила модус поненс можно Выразить следующим образом. Если существует истинная формула

являющаяся дизъюнкцией литералов и истинна формула

также являющаяся дизъюнкцией литералов , и в этих формулах предикатные символы литералов одинаковы и для атомов существует унификация 5, делающая их одинаковыми (записывается как Унификация то можно вывести истинную формулу, получающуюся в результате подстановки 8 в дизъюнкцию исходных формул после удаления в них литералов Выведенную таким образом истинную формулу называют резольвентой. Так же как и в случае резолюции для логики высказываний, обобщенную резолюцию можно выразить с использованием импликации.

Обратим внимание, что исходные формулы в обобщенной резолюции и резольвента являются дизъюнкцией литералов. Обычно такие формулы называют клйузальными формами, или клаузами. Таким образом, использование резолюции для вывода требует клаузальной формы представления знаний. Это, в свою очередь, означает, что база знаний, вывод для которой осуществляется на основе обобщенной резолюции, должна представлять собой совокупность клауз, понимаемых в целом как формула, являющаяся конъюнкцией клауз. Формулы такого типа обычно называют конъюнктивными нормальными формулами.

4.4.1. Прямой вывод на основе резолюции

Вернемся теперь к примеру с кубиками и повторим прямой вывод той же целевой формулы, но уже используя обобщенную резолюцию. Заметим, что формулы (4.130), (4.135) уже являются клаузами. Остальные формулы с помощью простейших преобразований на основе закона легко, преобразуются в клаузы. В результате вместо (4.136) — (4.141) получим следующие формулы.

Формулы, определяющие условия дополнения действий:

Формулы, определяющие условия переходов состояний среды:

Целевая формула. Целевая формула в соответствии с рис. 4.1 является конъюнкцией литералов и при прямом выводе, как и в случае использования обобщенного правила модус поненс, будет выводиться для каждого литерала, входящего в ее состав, раздельно

Вывод. Используя унифицированные клаузы (4.130), (4.151), которые после унификации превращаются в клаузы (4.158), (4.159), получаем резольвенту (4.160):

Используя клаузы (4.134), (4.160), получаем резольвенту

Используя эту резольвенту и унифицированную клаузу (4.154), которая после унификации превратилась в клаузу (4.162), получаем резольвенту (4.163):

Затем, используя клаузы (4.130), (4.134) и унифицированный резольвент (4.163), получаем резольвенту

Аналогично можем получить следующие резольвенты:

Итак, кубики А и могут быть перемещены на стол, в результате чего кубики В и С окажутся свободными. После этого, используя клаузы (4.134), (4.135), (4.165) и клаузу (4.152), которая после унификации превращается в клаузу (4.169), получаем резольвенту (4.170)

Наконец, воспользовавшись клаузами (4.134), (4.135), (4.165), (4.170) и клаузой (4.155), которая после унификации превращается в клаузу (4.171), получим резольвенту (4.172):

Таким образом, снова имеем истинные атомы на , на (В, Стол), на (С, Стол), на (D, Стол). Согласно правилу введения конъюнкции, вновь делаем заключение об истинности целевой формулы на на (В, Стол) на (С, Стол) на (D, Стол). На этом прямой вывод с использованием обобщенного правила резолюции завершен.

Достоинством использования обобщенного правила резолюции для прямого вывода является способность выводить большее количество формул по сравнению с выводом на основе обобщенного правила модус поненс. В процессе вывода база знаний по-прежнему разрастается за счет занесения в нее вновь выводимых формул. Некоторые из этих формул могут оказаться ненужными для вывода целевой формулы.

Как уже говорилось, Робинсон предложил использовать обобщенную резолюцию для создания стратегии вывода, в основе которой лежит опровержение, и и доведение до противоречия. Идея этой стратегии вывода состоит в следующем. Предположим необходимо вывести истинность целевой формулы а. Делается опровержение этой формулы, т.е. предполагается истинным ее отрицание . Эта формула, являющаяся отрицанием целевой, заносится в базу знаний. После этого, если, начиная обратный вывод с формулы -1 а, удастся установить противоречие, т.е. вывести пару литералов Р и то считается, что сделанное предположение об истинности отрицания целевой формулы ошибочно (опровергнуто) и делается заключение об истинности целевой формулы а. Если в результате рассмотрения всех возможных путей вывода такого противоречия установить не удастся, то считается, что целевая формула является ложной.

Рассмотрим стратегию обратного вывода на основе опровержения для примера с кубиками.

4.4.2. Обратный вывод на основе опровержения и обобщенной резолюции

Как уже отмечалось, вывод истинности целевой формулы может осуществляться по очереди литерал за литералом. Поэтому рассмотрим его только для одного литерала на целевой формулы (4.157). Опровержением литерала на является литерал на . Обратный вывод начинается именно с этого литерала. Для того чтобы можно было детально проследить процесс вывода, будем записывать на каждом шаге вывода с помощью обобщенной резолюции три формулы — две исходные и резольвенту, нумеруя по ходу вывода получаемые резольвенты, а также указывая для каждого шага используемые подстановки и подчеркивая те литералы, которые в резольвенту не попадают:

(см. скан)

(см. скан)