12.3.6. Стратегии исходных данных

Чтобы завершить обсуждение стратегий, учитывающих ход вывода, исследуем более подробно стратегию исходных данных, которая уже упоминалась ранее. Стратегия исходных данных дает доказательство, в котором по крайней мере одно из родительских предложений в каждой резолюции задано. Стратегия исходных данных не полна, но обладает интересными теоретическими свойствами. Ченг (1970) доказал, что стратегия исходных данных проходит тогда и только тогда, когда проходит стратегия предпочтения одночленов. Это позволяет „построить мост“ между подходом к решению задач в пространстве состояний (гл. 11) и подходом формального доказательства теорем. Мы покажем, что стратегия

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

Любой оператор программы GPS или FDS можно записать в виде

где и — правильно построенные выражения, возможно, содержащие функции или переменные. Пусть означает — состояние (цепочка), выводимое из условия решаемой задачи». Задачу в пространстве состояний можно интерпретировать так: „Задан предикат с помощью имеющихся продукций (аксиом) доказать выводимость Если мы хотим сохранить ограничение, что на каждом шаге решения задачи продукции должны применяться только к цепочке, полностью описывающей состояние, то продукцию можно интерпретировать так: „Если s — выводимая цепочка, то — также выводимая цепочка", т. е.

или в дизъюнктивной форме

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

Для иллюстрации разберем простую задачу из элементарной алгебры. Даны правила переписывания (продукции)

Требуется доказать, что правило симметрично, т. е. справедливо правило

Если подойти к этому как к задаче переписывания цепочек, то решением будет

Запишем (82) и (83) в виде предложений, полагая

Отрицание правила (84) имеет вид где

и несущим множеством является Выполняя соответствующие переименования, приходим к такому доказательству:

Этот вывод удивительно короток по сравнению с (85). Альтернативное доказательство с помощью резолюции можно было бы провести, реализуя шаги вывода (85) на простом устройстве. Пусть по правилу означает -шаг доказательства с продукциями. Каждый такой шаг принимает вид

где — литералы, выведенные из без подстановки, так что а второе предложение слева есть правилок в форме предложения. На первом шаге — в точности начальное состояние. Последний шаг —

где

т. е. отрицание целевого состояния. Поскольку в резолюциях вида (89) и (90) участвуют одночлены и исходные данные, существование доказательств при помощи стратегии исходных данных и стратегии предпочтения одночленов гарантируется. Но построение такого доказательства требует предварительного знания доказательства с продукциями. К тому же, как показывает пример (88), доказательство с резолюциями, построенное по доказательству с продукциями, вероятно, не самое изящное из возможных доказательств, основанных на принципе резолюции.

Что случится, если убрать ограничение, требующее, чтобы на каждом шаге доказательства с продукциями оператор применялся ко всей цепочке? Ясно, что это нужно сделать, поскольку в наиболее интересных задачах бывает нужно изменять и компоненты цепочки. Можно по-прежнему переходить от продукций к исчислению предикатов, но это оказывается слишком утомительным. В самом деле, это приведет к рассмотрению бесконечного множества аксиом! Удаление же указанного ограничения нарушает соответствие между Чтобы проиллюстрировать это, попробуем с помощью правила

доказать, что

Очевидно, что это тривиально, если можно применить к подцепочкам и Если воспользоваться упомянутым выше переходом к исчислению предикатов, получаем задачу, относящуюся к доказательству теорем:

Попытки решить эту задачу должны убедить читателя, что для вывода пустого предложения не годится, поскольку нельзя разрешить с атомами терма

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

соответствующее продукции

которая есть не что иное, как частный случай продукции После добавления (95) к аксиомам (94) находим решение (тривиальные подстановки опущены):

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