4.5.2. Правило резолюции для сложных предложений

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

S₁:  (A₁,... ,A_k, ...,A_n)

S₂: A_k  (B₁, ...,B_m) (где 1<k<n)

Здесь некоторый предикат А_k из отрицания S₁ совпадает с предикатом из левой части S₂. В этом случае шаг вывода заменяет А_k в S₁ на правую часть S₂ и в качестве резольвенты получают отрицание

S:  (A₁, ..., A_k-1, B₁,..., B_m, A_k+1, ..., A_n)

Данное правило проиллюстрируем содержательным примером.

допуская, что Не (темно и зима и холодно)

и что Зима если Январь

выводим, что НЕ (темно и январь и холодно)

В том случае, если S₁ имеет тот же вид, а S₂ - факт

S₂: A_k

причем А_k является одним из предикатов из S₁, шаг вывода только вычеркивает А_k из S₁ и получается резольвента

S:  (A₁, ..., A_k-1, A_k+1, ..., A_n)

Данный шаг вывода можно иллюстрировать следующим примером

допуская, что НЕ (темно и зима и холодно)

и что Зима

выводим, что: НЕ (темно и холодно)

4.5.3. Простая резолюция сверху вниз

Рассмотренные выше правила применяются на каждом шаге вывода только к двум родительским предложениям. Вместе с тем описание любой области знания содержит множество ППФ.

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

S₂: получает (студент, стипендию)  сдает (успешно, сессию, студент)

S3: сдает (успешно, сессию, студент)

Задача, которую надо решить, состоит в том, чтобы ответить на запрос

Получает ли студент стипендию?

Когда используется обычная система логического вывода, то такой вопрос представляется в виде отрицания

S:  получает (студент, стипендию)

и система должна отвергнуть это отрицание при помощи других предложений, демонстрируя, что данное допущение ведет к противоречию.

Этот подход часто применяется в математике и называется доказательством от противного.

Теперь представим себе, что исходная логическая модель, составленная из трех предложений S₁, S₂ ,S₃ поступает на вход системы логического вывода ЭВМ.

ШАГ 1

Система на первом шаге применит правило (*) к родительским предложениям S₁ и S₂ и получит резольвенту:

S:  сдает (успешно, сессию, студент)

ШАГ 2

Используя правило (**) к S и S₃ система выводит противоречие:

S`: 

Таким образом, для доказательства противоречивости S₁ S₂ S₃ оказалось достаточно двух шагов вывода.

Если считать, что S₂ и S₃ не противоречат друг другу, то они совместно противоречат S₁, т. е.

Подтверждают отрицание s:  s1:  (  получает (студент, стипендию))

или другими словами подтверждают предложение:

Получает (студент, стипендию)

и ответом на исходную задачу является «ДА».

Логический вывод, который порождает последовательность отрицаний, такую как (S_{1 ,} S , S`) в рассмотренном примере, называется резолюцией сверху вниз.