Правила вывода L являются обобщением обычных правил вывода исчисления предикатов. Например, правило подстановки формулируется так:

Ф (обобщенное правило подстановки)
(Гi Ф Кi )[Оi]

Понятие вывода в системе L стандартное.

Во второй части параграфа формулируется собственно исчисление поиска интеллектуального бектрекинга, в котором используется основная идея метода метапеременных — не большая, чем это необходимо, уточненность значений термов при подстановке (понятие положительного сопоставления формул является аналогом понятия наиболее общего унификатора в методе резолюций). Определяются правила поиска исчисления и понятие дерева поиска вывода. Формулируется общая стратегия поиска подстановок методом в "глубину", которая сводится к нахождению таких троек Г1К2О3 ,..., Гn КnОn, каждая из которых непротиворечива и совместима с предыдущими непротиворечивыми тройками. При завершении процесса поиска выдается результирующая тройка (Г1 ... Гn) (К1 ... Кn) (О1 ... Оn). Тактика интеллектуального бектрекинга определяет механизм взаимной "перекачки" термов из множества "равенств" в множество "неравенств" при неудачах. Это наглядно представлено на предложенной ранее конструкции двоичного дерева, правые ветви которого соответствуют системе неравенств, а левые — системе равенств. Если в процессе означивания термов появляется сигнал неудачи, то в систему неравенств (равенств) записывается новое неравенство (равенство), полученное в результате анализа возможных "причин неудачи", и процесс поиска продолжается с учетом накопленного "отрицательного" опыта.

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

В заключении главы сформулированное исчисление сравнивается с другими подобными системами, обсуждается вопрос эффективности предложенных систем, а также устанавливается взаимосвязь предложенного метода "интеллектуального бектрекинга" с результатами модификации языка "ПРОЛОГ" (за счет использования операторов "cut", "savecp", "cutto", "get backtracking") и с реализацией идеи "заморозки" вычислений (freeze operation) или "ленивых вычислений" (lazy evalution). На основе проведенного анализа выявляются перспективы дальнейшего развития метода "интеллектуального бектрекинга", а также формулируется тезис о том, что предложенное исчисление поиска возможно использовать как универсальную систему поиска, на базе которой возможно сочетание методов поиска "в глубину" и "в ширину".

Приложение 1 имеет вспомогательный характер и дополняет содержание первой главы диссертации. Здесь сформулирована система натурального вывода и система поиска на основе метода "чередования шагов анализа и синтеза" В.А. Смирнова. "Работа" системы поиска разбирается на примере построения вывода закона Пирса. Главное внимание уделяется обсуждению проблем, возникающих при организации поиска вывода в системах натурального вывода.

В приложении 2 ставится задача построения исчисления поиска вывода с тернарной логической связкой условной дизъюнкции. Связка условной дизъюнкции, введенная А. Черчем [16], обозначается [A, B, C], где A, B, C — пропозициональные формулы. Это запись понимается так: если значение формулы B истинно, то значение формулы [A, B, C] совпадает со значением формулы A, в противном случае, т.е. если значение B ложно, значение [A, B, C] совпадает со значением формулы C. Другие пропозициональные связки конъюнкции, дизъюнкции, импликации, отрицания определяются следующим образом:

A & B = [A, B, f]

A Ъ B = [t, A, B]

A Й B = [B, A, t]
Ш A = [f, A, t]

Связка условной дизъюнкции и константы t и f образуют полную систему связок, что позволяет построить пропозициональное исчисление S [17]. Аксиомами исчисления является стандартный набор аксиом пропозиционального исчисления, записанных в языке исчисления S. Например, аксиома A5 [17] (соответствующая закону утверждения консеквента p Й (q Й p) выглядит так: [[p, q, t], p, t]. Правилами вывода являются правило подстановки (в стандартной формулировке) и аналог правила modus ponens: из [A, B, C] и B следует A.

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