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

Не умаляя современного значения и перспективности этих работ, мы хотим подчеркнуть, что в настоящее время такие средства ИИ, как системы автоматического доказательства теорем (АДТ), которые работают обычно в полной первопорядковой логике, существенно превосходят упомянутые средства ИИ с точки зрения сложности решаемых задач. Эти задачи имеют характер задач на доказательство (см. Wos, Veroff R., 1994), причем планка сложности доказываемых теорем неуклонно повышается. С другой стороны, конкретные достижения на стыке математической логики и ИИ принадлежат, в основном, сфере задач, существенно менее критичных к ресурсным ограничениям (офлайн-задачи), по сравнению с задачами, требующими своего решения в темпе протекания процессов, в контексте которых эти задачи сформулированы (онлайн-задачи). Необходимо дальнейшее развитие систем АДТ и вообще логического подхода к условиям задач реального времени и в реальном мире, вызывающем потребности высокоэффективной автоматизации конструктивных, немонотонных и др. выводов. Этому посвящен данный доклад.

Рассмотрим детальнее главные причины, тормозящие широкое применение логического подхода.

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

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

Основным инструментом нашего подхода являются новые логические исчисления < J, >, где J - некоторое базовое исчисление и - правила, ограничивающие применение правил вывода в J и называемые модификаторами. В отличие от обычных стратегий (или тактик), предназначенных для ограничения пространства поиска, модификаторы могут коренным образом изменить логику базового исчисления для получения выводов с необходимыми свойствами, специфичными в определенных классах задач. Примеры модификаторов обсуждаются ниже. Например, существует модификатор для интуиционистского вывода, получаемого в рамках классического исчисления (см. первый пример в п. 3). По формальному содержанию понятия стратегии и модификатора идентичны, но мы понимаем стратегию как правило, создаваемое только для ограничения пространства поиска вывода, тогда как модификаторы можно интерпретировать, как правила для получения выводов в логиках, отличных от классической.

Чтобы создавать такие модификаторы, необходимо иметь базовый логический язык, сохраняющий эвристическую структуру знаний и обладающий такими свойствами, как регулярность, простота и прозрачная интерпретация не в терминах атомов и связок, а, по крайней мере, в терминах вопросов и ответов. Под регулярностью мы понимаем определенную предсказуемость формульной структуры (слева-направо), заданную порядком связок и чередованием кванторов и приводящую к возможности фокусировки внимания на локальном фрагменте формулы. Для такой роли не годятся ни исчисление предикатов, ни его варианты, например, язык дизъюнктов. Первый не регулярен, последний в большинстве случаев является результатом разрушения структуры знаний. Вообще создание и развитие логических языков, обладающих адаптируемостью к специфике задач, является одной из проблем ИИ. Важным элементом достаточно богатых языков являются те или иные кванторные конструкции. Например, язык многоосновных моделей [1] аппелирует к специализированным кванторам. Упомянем также язык -программирования [2, 3] и многосортный язык [4] для метода резолюций. Мы разработали язык позитивно образованных (по-) формул [5, 6] и соответствующие логические исчисления. Различные приложения к задачам интеллектного управления показали полезность и эффективность разработанного логического аппарата.

Язык по-формул есть полный язык первого порядка, формулы которого представляются как деревья. Каждый узел есть типовый квантор, состоящий из знака квантора или , векторной переменной и типового условия, являющегося конъюнктом, где конъюнкт есть множество атомов или F. По определению, А F справедливо для любого конъюнкта А. По каждой ветви знаки кванторов чередуются. Семантику по-формул см. в [1].

Базовое исчисление классических задач J имеет дело с задачами вида F => F, где F - по-формула, являющаяся конъюнкцией посылки и отрицания цели. Узлы {: В_i}, следующие непосредственно за корнем (базой) :А формулы F , называются вопросами, и, если В_i А, где : : —> - подстановка, то говорим, что вопрос В_i имеет ответ . Правило вывода в J состоит в использовании ответов, в результате чего задача сводится в общем случае к нескольким подзадачам. Выводом задачи F ==> F называется дерево задач, начинающееся с F =>F и заканчивающееся по каждой ветви частным случаем схемы аксиом F(Ф) =>F, а каждое применение правила вывода соответствует переходу от задачи к непосредственно следующим. Таким образом, поиск вывода можно представить как некоторую вопросно-ответную процедуру.

Назовем no-модификатором правило , определяющее для каждой J-задачи, не являющейся примером аксиомы, множество -допустимых ответов. По-модификатор - строгий, если он определяет для каждой J -задачи одноэлементное множество - допустимых ответов и, как следствие, однозначно определяет соответствующее дерево поиска вывода. Строгий модификатор называется непренебрегающим, если для каждой задачи А( B _iФ _i,) => F и каждого неиспользованного в выводе этой задачи ответа В_i А, этот ответ используется в каждой ветви дерева поиска вывода.

Теорема (полноты). Если - строгий непренебрегающий модификатор, то исчисление < J, > полно.

Первый пример использования понятия модификатора приведен в [5]. Там предложен модификатор такой, что задача F => F выводима в < J, > тогда и только тогда, когда F выводимо в интуиционистском исчислении. Из доказательства этого результата получается как следствие, что если в задаче F => G цель G имеет вид (А —> v{ :B _i, i= }), то любой классический вывод задачи в J является конструктивным. Этот результат применен в [7] для решения задачи интеллектного наведения телескопа в центр планеты в неполной фазе.

Второй пример касается рекурсивности, точнее, развертывания некоторой динамической системы во времени. Мы рассматриваем задачу управления группой лифтов в здании (с конечным множеством значений управлений). Логический подход для нее был предложен в [8] и состоит в упреждающем моделировании траекторий в быстром времени для различных допустимых значений управлений (в интервале реального времени между двумя коррекциями управления) и исключении нерациональных (плохих) управлений. Этот подход означает непрерывный синтез теорем о свойствах траекторий в исчислении J для оценки и выбора наиболее предпочтительных управлений. Модификатор этого вывода определяется так, что следующий момент времени порождается лишь тогда, когда по остальным ветвям использованы все ответы. Этот модификатор есть частный случай так называемого модификатора “по приоритетам”. Детальное описание задачи о лифтах дано в [8].

Третий пример касается немонотонных рассуждений в робототехнике. В [9] дан анализ результатов проекта STRIPS, где для планирования действий робота был использован метод резолюций совместно с механизмом забывания фактов. Но комбинация метода резолюций и процедуры забывания в общем случае оказалась довольно неестественной и, насколько нам известно, метод дальнейшего развития не получил. Мы возрождаем его идеи на основе техники модификаторов.

В основе лежит описание действий, как по-формул вида: A(), B*()C(), где символ * принадлежит не объектному, а метаязыку и служит для определения модификатора. Если мы отвечаем на вопрос А(), В*() D, где - подстановка, а база D содержит текущее описание мира, то факты В*() , содержащиеся в D, помечаются знаком * и не могут быть использованы для дальнейшего вывода. Таким образом, мы можем рассуждать немонотонно, оставаясь при этом в рамках классической логики.