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

Обратный вывод начинается с целевой формулы на (А, В) на (В, Стол)

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

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

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

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

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

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

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

свободен (В),

свободен (В) переместить (В, Стол),

переместить (В, Стол) на (В, Стол).

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

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

свободен (В),

свободен (В) освободить_и_переместить (В, Стол),

освободить_и_переместить (В, Стол) на (В, Стол),

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