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

Третья глава ("Интеллектуальный бектрекинг (intelligent backtracking)") посвящена решению проблемы "отхода" (backtracking). В ней ставится задача показать возможности аналитического подхода для решения проблемы "отхода" и обосновать тезис о совместимости существующих в ТПВ методов поиска "в глубину" и "в ширину". Для этого здесь построено исчисление поиска вывода — исчисление "интеллектуального бектрекинга" (на основе системы поиска, предложенной И.В. Ежковой [15]), в котором возможно сочетание этих методов.

В первом параграфе ("Постановка проблемы: и ") задается тема исследования, которая определяется противопоставлением существующих в теории поиска вывода двух стратегий поиска — методом "поиска в глубину" и методом "поиска в ширину". Пусть нам дана формула Ф и некоторое множество формул — мир S. Ставится задача найти такую подстановку, которая превратила бы результат подстановки формулы Ф — Ф* — в формулу, выводимую из формул мира S. Если, например, даны формула Ф1: P(x) & Q(y) & R(z,y) & S(x,a) и некоторый мир S1:

P(a), P(b),

Q(a), Q(c), Q(d),

R(b,c), R(b,d),

S(b,b),S(b,a),S(b),

то для получения вывода формулы Ф1* в мире S1 необходимо, чтобы каждый конъюнктивный член формулы Ф1* совпадал с некоторой элементарной формулой из S1.. Эту задачу можно решить, например, составив систему уравнений на термах формулы Ф1* и мира S1 и найти пересечение для значений одинаковых переменных формулы. Если это пересечение для каждой переменной формулы Ф1* не пусто, то система уравнений имеет решение(я).

Использование метода "поиска в ширину" предполагает на каждом уровне решения системы уравнений находить все возможные решения для каждой переменной. Составим систему уравнений для данного примера и решим ее методом "поиска в ширину". Система уравнений выглядит так:

1. x = a, b( для первого конъюнктивного члена формулы )

2. y = b, c, d

3. ( z = b & y = c ), ( z = b & y = d )

4. x = b

Найдем пересечение значений для каждой переменной формулы Ф1*. Из п.1 и п. 4 видно, что решением для x является одноэлементное множество {b}, из п.3 — решением для z также является {b}. При анализе пп.2 — 3 видно, что решением для y является двухэлементное множество {c, d}. Таким образом, подстановки {x/b, y/c, z/b} и {x/b, y/d, z/b} превращают формулу Ф1 в формулу Ф1*, выводимую в мире S1, т.е. являются искомым решением.

Другим подходом к решению данной задачи, который особенно оправдан при "больших" мирах S, является "поиск в глубину", суть которого заключается в поиске на каждом уровне лишь первого возможного решения, удовлетворяющего условиям задачи. Для данной системы уравнений, на первом уровне будет выбрано значение x = a, на втором — y = b, что приводит к "неудаче" на третьем уровне. Так возникает проблема "отхода", которая связана с тем, что при использовании метода поиска "в глубину" находится лишь первое локальное решение, которое в общем случае может оказаться неверным, и подлежит пересмотру и при дальнейшем поиске.

Во втором параграфе ("Неформальное введение в "интеллектуальный бектрекинг" (intelligent backtracking)") дается общая схема "интеллектуального бектрекинга" (intelligent backtracking), который был предложен для преодоления недостатков тактики "наивного бектрекинга" ("naive backtracking") за счет использования аналитического подхода к построению выводов. Основная идея "интеллектуального бектрекинга" заключается в анализе полученной при "неудачном" означивании информации для выяснения возможных "причин" неудачи с целью их блокирования при следующих попытках означивания. Для пояснения сути работы "интеллектуального бектрекинга" (без учета совпадения предикатных букв и местности предикатов) предлагается конструкция двоичного дерева поиска подстановок (см. рисунок ниже), вершины которого соответствуют означиваемым термам; «левые» ветви — сделанным в процессе поиска подстановкам (подстановки обозначены знаком «/», например x/a); "правые" ветви — запретам на ту или иную подстановку (запрет обозначается с помощью знака «j», например x j a):

X

/ \

xja/ \x/a

Y / \ Y

yjd/ \y/d yjd/ \y/d

Z / \ Y / \

zjc/ \z/c yjb/ \y/b

W / \ / \ Z

wjc/ \w/c zjc/ \z/c

U / \ / \ W

uja/ \u/a wjc/ \w/c

/ \ W / \



Предложенная конструкция дерева поиска подстановок позволяет организовывать как процесс поиска подстановок, так и тактику "интеллектуального отхода" при неудачах.