Второй важный подход к индуктивному логическому программированию предусматривает обращение обычного процесса дедуктивного доказательства. Метод обратной резолюции основан на том наблюдении, что если классификация Classifications примера следует из выражения BackgroundAHypothesisADescriptions, то должна существовать возможность доказать этот факт с помощью метода резолюции (поскольку метод резолюции является полным). А если есть возможность "провести доказательство в обратном направлении", то можно найти такую гипотезу Hypothesis, через которую проходит это доказательство. Поэтому задача состоит в том, чтобы найти способ обращения процесса резолюции.

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

Начальные этапы процесса обратной резолюции показаны на рис. 19.9; на этих этапах вся работа сосредоточивается на положительном примере Grandparent

{George, Anne). Процесс начинается с конца доказательства (который обозначен квадратом в нижней части рисунка). Предполагается, что резольвента С представляет собой пустое выражение (т.е. противоречие), а в качестве С2 берется выражение

, которое является отрицанием целевого примера. В первом обратном этапе используются выражения С и С2 и формируется выражение Grandparent {George, Anne), соответствующее С1 На следующем этапе это выражение берется в качестве С, выражение Parent {Elizabeth,Anne) используется в качестве С2, а в качестве с1 формируется следующее выражение:

На последнем этапе данное выражение рассматривается как резольвента. Если в качестве С2 берется выражение Parent {George, Elizabeth), то одним из возможных выражений d становится гипотеза:

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

Grandparent{George,Anne).

Рис. 19.9. Начальные этапы в процессе обратной резолюции. Затененные выражения сформированы на этапах обратной резолюции из выражений, находящихся справа и внизу. Незатененные выражения взяты из множеств Descriptions и Classifications