4.2. Прямой и обратный вывод

Наиболее распространенными являются два типа вывода: прямой и обратный. До сих пор как во второй главе, так и в настоящей в примерах со средой чудовища использовался прямой вывод. Будем полагать, что все формулы, входящие в постановку задачи, образуют некоторую начальную базу знаний.

Идея прямого вывода основана на следующих шагах. На первом шаге подбирается правило вывода, условие которого можно образовать из формул начальной базы знаний с использованием, если это необходимо, унификации. Обычно начинается все с формул, представляющих знания о начальном состоянии среды. По правилу вывода получаются новые истинные формулы, являющиеся его унифицированным следствием. Эти формулы помещаются в начальную базу знаний, в результате чего она превращается в другую базу знаний, из нее извлекаются новые формулы, и все повторяется сначала до тех пор, пока на очередном шаге унифицированное следствие не совпадет с целевой формулой. Таким образом, в процессе прямого вывода на каждом его шаге база знаний пополняется выведенными истинными формулами.

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

4.2.1. Постаиовка задачи в среде кубиков

Формулы, определяющие начальные знания агента. Имеем среду, состоящую из стола и кубиков на нем. Каждый из кубиков может лежать либо непосредственно на столе, либо на одном из других кубиков, образуя с кубиками, лежащими под ним, столик. Стрлбики могут быть любой высоты. Пусть начальное состояние среды кубиков следующее: кубики Си лежат на столе, кубик А лежит на кубике С, кубик D на кубике В (рис. 4. 1).

Рис. 4.1. Начальное и целевое состояния среды кубиков

Начальное состояние среды кубиков можно описать следующими атомами:

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

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

Формулы, определяющие условия перехода состояний средьп

Целевая формула. В соответствии с рис. 4.2 целевой будет следующая формула:

4.2.2. Прямой вывод

Начнем с формулы (4.136), унифицируя которую получим формулы следующие формулы:

На основании обобщенного правила модус поненс и формул (4.130), (4.134), (4.132), (4.135), (4.143), (4.144) делаем заключение о возможности выполнения действия по перемещению кубиков А и D на стол: истинны атомы переместить (А, Стол), переместить (D, Стол). Эти атомы помещаются в исходную базу знаний. Далее можно воспользоваться формулами (4.138), (4.139), унифицируя которые получим формулы

В результате кубики А и D оказались на столе. Кубики С и В никуда не перемещались и, согласно начальному состоянию, остались на столе. Используя формулу (4.137), получим унифицированную формулу на (А, Стол) а свободен (А) а свободен (В) => переместить (А, В). (4.149) Наконец, воспользовавшись формулой (4.138), получим унифицированную формулу

Рис. 4.2. (см. скан) Граф прямого вывода в среде кубиков

Таким образом, Имеем истинные атомы на , на Стол), на (С, Стол), на (Д Стол). Согласно правилу введения конъюнкции, делаем заключение об истинности целевой формулы на на (В, Стол) а на (С, Стол) на (Д Стол). На этом прямой вывод завершен. На рис. 4.2 показан граф вывода указанной целевой формулы. В процессе прямого вывода база знаний разрастается, в нее заносятся вновь выводимые формулы. Некоторые из них могут оказаться ненужными для вывода целевой формулы. Таких «лишних» формул может быть достаточно много. Например, на рис. 4.2 ненужной является формула свободен

4.2.3. Обратный вывод

Обратный вывод начинается с целевой формулы на на (В, Стол) на (С, Стол) на (D, Стол). Для нашего примера его можно проследить по тому же графу на рис. 4. 2. Только в отличие от прямого вывода, который осуществлялся в направлении стрелок, обратный вывод осуществляется против направления стрелок. Кроме того, ненужных формул не выводится, что делает его в ряде случаев более эффективным, особенно, если для вывода целевых формул достаточно незначительной части базы знаний.

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

Первая группа вопросов связана с понятием полноты исчисления. Если все общезначимые формулы выводятся в данном исчислении и только они, то его называют яалным. В противном случае исчисление называют неполным. Если в нашем распоряжении (распоряжении агента) имеется некоторое исчисление, то как определить, является ли оно лолным?

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

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

Прежде, чем переходить к ответу на перечисленные выше вопросы, ответим на более простой. Если формула выводима в каком-либо исчислении (не обязательно полном), то выводима ли она при использовании той же системы

аксиом и единственного правила вывода — обобщенного правила модус поненс? Вернемся к примеру со средой кубика.

Предположим, что в начальной базе знаний имеются аксиомы

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

Если в базе данных имеются аксиомы

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