Комбинация прямой и обратной систем

Мы рассмотрели один ограниченный случай (прямая система) и другой ограниченный случай (обратная система). Возникает естественная идея: объединить эти два ограниченных случая в надежде получить неограниченный.

В результате объединения прямой и обратной систем дедукции на основе правил получается следующее: имеются факты, представленные в форме И/ИЛИ, имеются цели, представленные в форме И/ИЛИ, и имеются два сорта правил: прямые правила в форме L —» W, обратные правила в форме W —> L. Они будут навстречу друг другу наращивать графы решения, пока эти графы не столкнутся. Другими словами, мы вводим три вида резолюции:

  • 1) резолюция фактов и прямых правил, являющаяся частным случаем метода резолюций Робинсона, которую мы уже обсудили;
  • 2) резолюция целей и обратных правил, которая является частным случаем двойственного метода резолюций;
  • 3) резолюция фактов и целей.

Последняя называется правилом гашения.

Правило гашения заключается в следующем: две вершины гасят друг друга, если они унифицируются либо гасятся исходящие из них ^-связки.

Условие окончания выглядит в этом случае гак: корень фактов гасит корень целей, и подстановки на дугах соответствия согласованы.

Рассмотрим позитивный пример, чтобы понять преимущества комбинированной прямой и обратной системы (это пример уже рассматривался в п. 4.1.8):

существуют умные студенты программисты знают метод резолюций

Факт:

Обратное правило:

Прямое правило: студенты не знают метода резолюций

Цель: существуют умные не программисты

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

В результате решение находится достаточно легко (рис. 4.5). На этом рисунке гашение обозначено более жирными стрелками.

Комбинация прямой и обратной систем дедукции

Рис. 4.5. Комбинация прямой и обратной систем дедукции

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

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

Нижняя формула является логическим следствием верхней формулы

& В) v (С & D) —> А & v С) & D.

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

Неполнота правила гашения

Рис. 4.6. Неполнота правила гашения

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

Остается открытым вопрос: можно ли подправить форму И/ИЛИ таким образом, чтобы резолюция фактов и целей сделалась состоятельной и полной так же, как резолюция фактов и правил и резолюция правил и целей.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >