Переходя к фразовой форме логики предикатов, при которой допускается запись формул только через операторы  ,  и  , правило можно записать как:

B₁ B₂ B₃  … B_k  A (k  0)

или, используя правило Де Моргана в дизъюнктивной форме, удобной для автоматического логического вывода

B₁ B₂  B₃  … B_k  A (k0).

Здесь А и В_i - литералы, т.е. позитивные или негативные атомарные формулы, а фраза - множество литералов, соединенных операторными знаками , обобщающая понятие импликации.

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

? – Q₁  Q₂ …  Q_n , (n  0).

Считается, что переменные предикатов в вопросе связаны квантором существования. Вычисление логической программы Р состоит в построении примера заданного вопроса, логически выводимого из Р. Этот процесс является по существу автоматическим доказательством теорем в формальной системе исчисления предикатов первого порядка. Наиболее рационален в этом случае метод с применением принципа резолюции Робинсона [5, 8].

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

29

логическому противоречию (пустому множеству).

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

Р(а) Q (b,c),

Q(x,y) R(x,y)

содержится пара предикатов Q(b,c) и Q(b,c), соответствующих правилу резолюции, поэтому к программе может быть добавлена фраза-резольвента и все три фразы могут быть использованы в последующих резолюциях.

Таким образом, правило резолюции объединяет правило модус поненс и унификацию. Последняя позволяет строго сопоставлять аргументы, учитывая, что все переменные во фразе программы неявно имеют кванторы существования и общности. Например, во фразе

Q(x,y) R(x,y)

подразумевается наличие кванторов, т.е.

xy(Q(x,y) R(x,y)).

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

В процессе логического вывода в ответ на запрос-цель Q из логической программы Р вычисляется ответ (решение) путем построения последовательности текущих целей-резольвент при многократном использовании правила резолюции. Ответ положителен, если Q выводим из программы Р, и отрицателен в противном случае. Для доказательства

30

выводимости применяется процедура опровержения (доказательство от противного), при которой цель добавляется к исходной логической программе в виде отрицания. Для новой логической программы с отрицанием цели используются соответствующие стратегии применения правила резолюции и доказывается выводимость цели. Наиболее часто применяется нисходящая стратегия поиска "в глубину". Приведем пример.

Пусть имеется логическая программа из четырех фраз:

Р(а) Q(a, b);

Q(x ,y) R(x, y);

S(b);

R(a, b).

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

добавляем к программе отрицание цели Р(а) и проводим первую резолюцию,в результате которой Р(а) резольвируется с фразой Р(а) Q(а, b), давая новую фразу программы Q(а, b),

добавляем фразу Q(а, b) и проводим вторую резолюцию, в результате которой Q(а, b) резольвируется с фразой Q(х, у) R(х, у), давая новую фразу программы Q(а, b),

добавляем фразу R(а,b) и проводим третью резолюцию, в результате которой эта фраза резольвируется с фразой R(a, b), давая пустую фразу, что означает противоречие.

Ввиду того, что добавление отрицания цели Р(а) приводит к противоречию, сама цель Р(а) выводится из логической программы (является её следствием), и может быть принято положительное решение (ответ на запрос). Заметим, что стратегия решения "в глубину" при движении по дереву промежуточных целей - резольвент не является единственной. Возможны стратегии "в ширину" или смешанные.

Принятие решений на основе логического вывода с использованием языка исчисления предикатов первого порядка в настоящее время автоматизировано и легко реализуется на ЭВМ. При этом исходная логическая

31

программа, формализующая продукционную базу знаний, составляется на языке PROLOG [13]. Она декларативна и не содержит описания алгоритма решения задачи. Интерпретатор этого языка реализует правило резолюции и способен отвечать на запросы, проводя каждый раз доказательство, аналогичное приведенному в примере. По существу, интерпретатор является встроенной в язык машиной вывода и хорошо работает при решении простых задач. В сложных случаях, требующих других стратегий поиска, используются встроенные предикаты управления решением задачи, включая механизм повторения (предикат fail ) и отсечения (предикат cut). Первый предикат требует перебрать все варианты решения, т.е. провести поиск полным перебором, второй - ограничивает перебор вариантов, чтобы сократить поиск или устранить лишние решения. Заметим, что включение механизма повторения позволяет выявить все множество решений, если их несколько.

Рассмотрим простой пример сборки двух деталей роботом. Пусть требуется собрать детали типа 1 и 2, каждая из которых имеет два типоразмера, так, чтобы собирались в пары детали одного типоразмера. Продукционная база знаний для описания этой задачи имеет вид.

Факты: 1. деталь1=тр1.

2. деталь2=тр1.

3. деталь1=тр2.

4. деталь2=тр2.

Правила: 5. ЕСЛИ деталь1=тр1 И деталь2=тр1

ТО сборка11.

6 ЕСЛИ деталь1=тр2 И деталь2=тр2