Процедурная дедукция в системе PLANNER

8.4. Процедурная дедукция в системе PLANNER

Система PLANNER явилась одной из первых попыток разработки языка программирования задач искусственного интеллекта, базирующегося на идеях автоматического доказательства теорем. Хотя разработчикам и не удалось в полной мере реализовать задуманное, созданное подмножество языка, получившего название Micro-PLANNER, нашло применение в системах планирования, в частности в программе SHRDLU, представленной в главе 2. Ниже мы обсудим те аспекты системы PLANNER, которые имеют отношение к представлению знаний.

Система PLANNER моделировала состояние некоторой области рассуждений в терминах ассоциативной базы данных, которая содержала как утверждения, так и теоремы, функционирующие как процедуры. Утверждения представляли собой списки типа "предикат-аргумент", подобные тем, что используются в LISP. Например:

(BLOCK B1) (ON Bl TABLE)

Теоремы же в действительности представляли собой выражения, в которых можно было проследить влияние одних термов на другие. Например, теорема

(ANTE (BLOCK X) (ASSERT (ON X TABLE)))

в действительности является процедурой, которая говорит: "Если утверждается, что X это блок, то также утверждается, что X находится на столе". Таким образом, если существует утверждение (BLOCK B1), то можно также считать утверждением и выражение (ON Bl TABLE). Функция ASSERT добавляет собственный конкретизированный аргумент (т.е. аргумент, которому присвоено определенное значение) в базу данных.

Выше был приведен пример антецедентной теоремы. Это название акцентирует внимание на том, что нас интересует только логическая связь между антецедентом и консек-вентом (по аналогии с правилом modus ponens), а не связь между отрицанием консеквен-та и отрицанием антецедента (по аналогии с правилом modus fallens). Мы говорим, что в действительности эта теорема является процедурой, поскольку в ней содержится управляющая информация. Ее функционирование во многом напоминает демонов в системе фреймов, описанных в главе 6.

Система PLANNER поддерживает и другой вид процедур, которые получили наименование консеквентной теоремы. Пример процедуры такого типа приведен ниже:

(CONSE (MORTAL X) (GOAL (MAN X))).

Эта процедура может быть прочитана так: "Для того чтобы показать, что X смертен, покажите, что X — человек". Если выражение, которое нужно доказать (цель), сформулировано в виде (MORTAL SOCRATES) (Сократ смертен), то в качестве подцели будет выступать выражение (MAN SOCRATES) (Сократ человек). Функция GOAL организует поиск в базе данных собственного конкретизированного аргумента. Однако не удастся использовать эту теорему для перехода от утверждения (MAN SOCRATES) (Сократ человек) к утверждению (MORTAL SOCRATES) (Сократ смертен).

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

(CONSE (ON X Y)

(GOAL (CLEAR X)) (GOAL (CLEAR Y))

(ERASE (ON X Z)) (ASSERT (ON X Y)))

Задавшись целью (ON Bl B2), если на Bl и на В2 ничего не стоит, PLANNER выполнит необходимые операции с базой данных. Таким образом, консеквентная теорема поддерживает в системах автоматизации планирования работу механизма реализации операторов, подобных тем, которые мы видели в программе STRIPS (см. главу 3).

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

С концепцией процедурной дедукции связана проблема полноты. Система доказательства является полной, если все тавтологии, т.е. тривиально истинные выражения вроде (р v —pi), могут быть выведены в ней как теоремы. В системе PLANNER это свойство отсутствует. Мы уже обращали внимание на то, что нельзя сформировать выражение (MORTAL SOCRATES) из базы данных, в которой содержатся

(MAN SOCRATES)

(CONSE (MORTAL X)

(GOAL (MAN X))).

Это те издержки, с которыми нужно смириться, если мы хотим объединить управляющую информацию с пропозициональным представлением. К сожалению, система PLANNER оказалась не более эффективной, чем системы, основанные на теоремах резолюций. Это произошло потому, что использованная в ней управляющая информация страдает "близорукостью", отсутствует общая стратегия, а имеющийся набор теорем позволяет формулировать локальные решения, которые могут давать, а могут и не давать желаемый эффект. Отсутствует в PLANNER и возможность каким-то образом формировать суждения о механизме управления, что-то вроде метаправил, о которых шла речь в главе 5.

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