8.4. Процедурная дедукция в системе PLANNER
Система PLANNER явилась одной из первых попыток разработки языка программирования задач искусственного интеллекта, базирующегося на идеях автоматического доказательства теорем. Хотя разработчикам и не удалось в полной мере реализовать задуманное, созданное подмножество языка, получившего название Micro-PLANNER, нашло применение в системах планирования, в частности в программе SHRDLU, представленной в главе 2. Ниже мы обсудим те аспекты системы PLANNER, которые имеют отношение к представлению знаний.
Система PLANNER моделировала состояние некоторой области рассуждений в терминах ассоциативной базы данных, которая содержала как утверждения, так и теоремы, функционирующие как процедуры. Утверждения представляли собой списки типа "предикат-аргумент", подобные тем, что используются в LISP. Например:
(BLOCK B1) (ON Bl TABLE)
(ANTE (BLOCK X) (ASSERT (ON X TABLE)))
Выше был приведен пример антецедентной теоремы. Это название акцентирует внимание на том, что нас интересует только логическая связь между антецедентом и консек-вентом (по аналогии с правилом modus ponens), а не связь между отрицанием консеквен-та и отрицанием антецедента (по аналогии с правилом modus fallens). Мы говорим, что в действительности эта теорема является процедурой, поскольку в ней содержится управляющая информация. Ее функционирование во многом напоминает демонов в системе фреймов, описанных в главе 6.
Система PLANNER поддерживает и другой вид процедур, которые получили наименование консеквентной теоремы. Пример процедуры такого типа приведен ниже:
(CONSE (MORTAL X) (GOAL (MAN X))).
Консеквентные теоремы могут также манипулировать базой данных. Например, для того чтобы положить блок В1, на котором ничего не стоит, на блок В2, на котором также ничего не стоит, нужно отыскать, на чем же стоит блок В1, удалить соответствующее утверждение и сформировать новое, которое говорит, что блок В1 стоит на блоке В2.
(CONSE (ON X Y)
(GOAL (CLEAR X)) (GOAL (CLEAR Y))
(ERASE (ON X Z)) (ASSERT (ON X Y)))
Из этого краткого описания читатель может сделать заключение, что в системе PLANNER управляющая информация явно представлена в базе данных процедур, а не скрывается в компоненте, ведающем стратегией выполнения доказательства теорем, как это делается в системах, работающих на основе метода опровержения резолюций. Достоинство такого подхода состоит в том, что можно решить в каждом конкретном случае, какие правила влияния следует применять. Кроме того, в нашем распоряжении оказывается довольно эффективный инструмент моделирования изменения состояния задачи.
С концепцией процедурной дедукции связана проблема полноты. Система доказательства является полной, если все тавтологии, т.е. тривиально истинные выражения вроде (р v —pi), могут быть выведены в ней как теоремы. В системе PLANNER это свойство отсутствует. Мы уже обращали внимание на то, что нельзя сформировать выражение (MORTAL SOCRATES) из базы данных, в которой содержатся
(MAN SOCRATES)
(CONSE (MORTAL X)
(GOAL (MAN X))).
В следующем разделе мы кратко остановимся на системах, в которых была предпринята попытка устранить эти недостатки.