Васильев Станислав Николаевич АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО И СИНТЕЗ ТЕОРЕМ В ЯЗЫКЕ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ Институт проблем управления им. В.А.Трапезникова РАН

ПРИМЕНЕНИЯ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ Патрульный самолет для оперативной разведки и наведения

СОДЕРЖАНИЕ Введение. Язык L позитивно-образованных формул для представления знаний. Исчисление J позитивно-образованных формул для обработки знаний. О применениях в автоматизации исследований, проектировании и управлении. О модификациях базового исчисления. Проблема неполноты информации: логические уравнения, минимальное дооснащение. Ограничения и проблемы.

встраивание интеллектных компонент: распознавания образов, обучения, планирования действий и др. встраивание цифровых преобразователей КЛАССИЧЕСКИЕ ТЕХНИЧЕСКИЕ СРЕДСТВА АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ встраивание высшей интеллектуальной функции: целеполагания СИСТЕМЫ ИНТЕЛЛЕКТНОГО УПРАВЛЕНИЯ (ИНФОРМАЦИОННО- УПРАВЛЯЮЩИЕ СИСТЕМЫ С ИНТЕЛЛЕКТНЫМИ И СМЕШАННЫМИ МОДЕЛЯМИ УПРАВЛЕНИЯ) СИСТЕМЫ ИНТЕЛЛЕКТУАЛЬНОГО УПРАВЛЕНИЯ ИНФОРМАЦИОННО- УПРАВЛЯЮЩИЕ СИСТЕМЫ (ЦИФРОВОЕ УПРАВЛЕНИЕ НЕПРЕРЫВНЫМИ ОБЪЕКТАМИ) ЭВОЛЮЦИЯ СИСТЕМ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ

Нейроуправление Управление на основе знаний (и нечетких логик, в частности) Эволюционные алгоритмы Традиционный искусственный интеллект Традиционное управление 1980г. Цифровое и логическое (автоматное) управление Двоичные переменные {1, 0} Непрерывные (неограниченные) переменные (-,+ ) II.Теория управленияI. Искусственный интеллект ИНТЕЛЛЕКТНОЕ УПРАВЛЕНИЕ – пограничная область двух дисциплин: время Непрерывные (ограниченные) и двоичные переменные [0,1], {1, 0}

ИЕРАРХИЯ УРОВНЕЙ УПРАВЛЕНИЯ Объект управления 1. Программное управление 2. Позиционное управление 3. Идентификационное управление 4. Адаптивное управление 5. Интеллектное управление (без целеполагания) 6. Интеллектуальное управление (с целеполаганием) Среда Уровни управления

«Знаниевые» системы

Умозаключения на основе богатых (мощных) логик (медленные и высокоуровневые интеллектные процессы формирования управления) ПРОБЛЕМЫ СМЕШИВАНИЯ УПРАВЛЕНИЙ В ОБЪЕДИНЕНИИ ИНТЕЛЛЕКТНЫХ КОМПОНЕНТ Уровни интеллекта Инструктивные (логически ограниченные) умозаключения (продукционные: если … то …) Рефлекторные реакции (стереотипное и высокопроизводительное формирование управлений на искусственных нейронных сетях) Наблюдения (входы) Смешивание управлений (выходы) Повышение уровня интеллекта Повышение скорости вычислений Goal- oriented level Reactive behavior level

СПЕЦИФИКА ПРИМЕНЕНИЯ ЛОГИЧЕСКОГО ПОДХОДА К ИНТЕЛЛЕКТНОМУ УПРАВЛЕНИЮ Для охвата более широкого класса задач необходимо обеспечить выразительность языка (ввести кванторы и предикаты вместо пропозициональности). В сравнении с off-line задачами более остро стоят проблемы: учета ресурсных ограничений ( времени, отпущенного на формирование управления в масштабе реального протекания процессов; ограниченности памяти; неполноты информации и т.п.); эффективности дедукции (по возможности, необходимо уменьшить пространство поиска, хотя увеличивается длина выводов, Г.С.Цейтин, 1968, R.Statman, 1975, В.П.Оревков, ; необходимо обеспечить совместимость логики с эвристиками).

К ИНТЕЛЛЕКТНОМУ УПРАВЛЕНИЮ СИСТЕМОЙ КАБИН ЛИФТА Этажи Кабина Команды Критерии качества: среднее время ожидания; доля долгих ожиданий (больше 60 сек.); количество переадресаций; энергопотребление; Направления движения Вызов вверх (с временем ожидания) Вызов вниз

ТРАДИЦИОННЫЙ ПОДХОД К ЗАДАЧЕ x(t+1)=f(x(t), u(t,x(t), v(t), w(t)), t), t=0,1,2,… x 1, …, x n – местоположения кабин лифта; x n+1, …, x 2n – логические переменные (направления движения кабин); v(t) – вектор вызовов с этажей; w(t) – команды изнутри кабин; u(t,x,v,w) – вектор управлений (назначений кабин); q 1 – среднее время ожидания min; q 2 – доля долгих (более 60 сек.) ожиданий min; q 3 – количество переназначений min;..... (комфорт, энергопотребление и т.д.). ЗАДАЧА. Синтезировать u в классе Парето-оптимальных решений. Известный метод. Call Assignment Method – численный метод векторной оптимизации. НЕДОСТАТОК. Жесткость математических моделей. Полезно использовать мягкие (логические) модели. МОДЕЛЬ:

ПРИМЕНЕНИЕ ЛОГИКИ В ЗАДАЧАХ УПРАВЛЕНИЯ В РЕАЛЬНОМ ВРЕМЕНИ: АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ - это предсказать и оценить свойства траекторий системы при альтернативных управлениях (за интервал времени между двумя моментами корректировки управления), отбрасывая нерациональные траектории. Этот подход означает непрерывный синтез теорем о свойствах траекторий вместо АДТ. Используются: 1) аксиома существования следующего момента времени t:T(t) t :T(t ), N(t,t ), где T(t) «t – момент времени», N(t,t ) «момент времени t непосредственно следует за t», 2) соответствующая стратегия вывода. Метод заключается не в доказательстве априори данной теоремы, а в выводе следствий из знаний, т.е. в виде свойств траекторий.

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ Цель управления и возможности средств достижения цели описываются в логическом языке L формулами F и G соответственно. Из вывода извлекается последовательность действий. Управление Цель управления Спецификация F и G Автоматическое доказательство теоремы (АДТ) F G Извлечение плана из вывода

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

Построена новая первопорядковая логика с классической семантикой, полная относительно выводимости и с рядом не обеспечивавшихся раньше в литературе особенностей, в числе которых: свойство сильной модифицируемости семантики (немонотонность логики, конструктивность, динамичность и др.), высокая совместимость с эвристиками в приложениях к автоматизации планирования действий, управлению со структурной реконфигурацией и др. (С.Н.Васильев и др. Интеллектное управление динамическими системами, М.- ФМЛ, 2000). В развитие этой логики разработан метод автоматического гипотезирования, т.е. порождения условий выводимости хорновских и некоторых других формул, эффективно совмещающий в себе возможности систем автоматической дедукции и процедур генерализации первопорядковых формул (индуктивного типа, С.Н.Васильев, СМЖ, 1997). НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ

Основной алфавит: символы, обозначающие переменные x, y, …; константы a, b, …; функциональные символы +, -1, …; предикатные символы, =, … Термы : x + a, x -1, … Атомы : x 0, y=x+2, НЕЧЕТНОЕ (x), ВОЗРАСТАЕТ (давление ), … Конъюнкты : 1) конечное множество атомов (рассматриваемое конъюнктивно), 2) False или 3) True (пропозициональные константы). Элементарные формулы: это – формулы X : A и – формулы X : A : False, где X – множество переменных, A – конъюнкт. К ПРЕДСТАВЛЕНИЮ ЗНАНИЙ: ПЕРВОПОРЯДКОВЫЙ ЯЗЫК L ПОЗИТИВНО ОБРАЗОВАННЫХ ФОРМУЛ (ПО-ФОРМУЛ)

Основной алфавит: символы, обозначающие переменные x, y, …; константы a, b, …; функциональные символы +, -1, …; предикатные символы, =, … Термы : x + a, x -1, … Атомы : x 0, y=x+2, НЕЧЕТНОЕ (x), ВОЗРАСТАЕТ (давление ), … Конъюнкты : 1) конечное множество атомов (рассматриваемое конъюнктивно), 2) False или 3) True (пропозициональные константы). Элементарные формулы: это – формулы X : A и – формулы X : A : False, где X – множество переменных, A – конъюнкт. Формулы : 1) если F 1, …, F n – формулы, то X : A ( F 1, …, F n ) – формула ; ( содержательно ветвление ( при n 2) понимается как конъюнктивное) ; К ПРЕДСТАВЛЕНИЮ ЗНАНИЙ: ПЕРВОПОРЯДКОВЫЙ ЯЗЫК L ПОЗИТИВНО ОБРАЗОВАННЫХ ФОРМУЛ (ПО-ФОРМУЛ) &

Основной алфавит: символы, обозначающие переменные x, y, …; константы a, b, …; функциональные символы +, -1, …; предикатные символы, =, … Термы : x + a, x -1, … Атомы : x 0, y=x+2, НЕЧЕТНОЕ (x), ВОЗРАСТАЕТ (давление ), … Конъюнкты : 1) конечное множество атомов (рассматриваемое конъюнктивно), 2) False или 3) True (пропозициональные константы). Элементарные формулы: это – формулы X : A и – формулы X : A : False, где X – множество переменных, A – конъюнкт. Формулы : 1) если F 1, …, F n – формулы, то X : A ( F 1, …, F n ) – формула ; ( содержательно ветвление ( при n 2) понимается как конъюнктивное) ; 2) если F 1, …, F n – формулы, то X : A ( F 1, …, F n ) – формула ; (ветвление ( при n 2 ) – дизъюнктивное) ; К ПРЕДСТАВЛЕНИЮ ЗНАНИЙ: ПЕРВОПОРЯДКОВЫЙ ЯЗЫК L ПОЗИТИВНО ОБРАЗОВАННЫХ ФОРМУЛ (ПО-ФОРМУЛ) V

Основной алфавит: символы, обозначающие переменные x, y, …; константы a, b, …; функциональные символы +, -1, …; предикатные символы, =, … Термы : x + a, x -1, … Атомы : x 0, y=x+2, НЕЧЕТНОЕ (x), ВОЗРАСТАЕТ (давление ), … Конъюнкты : 1) конечное множество атомов (рассматриваемое конъюнктивно), 2) False или 3) True (пропозициональные константы). Элементарные формулы: это – формулы X : A и – формулы X : A : False, где X – множество переменных, A – конъюнкт. Формулы : 1) если F 1, …, F n – формулы, то X : A ( F 1, …, F n ) – формула ; ( содержательно ветвление ( при n 2) понимается как конъюнктивное) ; 2) если F 1, …, F n – формулы, то X : A ( F 1, …, F n ) – формула ; (ветвление ( при n 2 ) – дизъюнктивное) ; 3) формулы – это – и – формулы. К ПРЕДСТАВЛЕНИЮ ЗНАНИЙ: ПЕРВОПОРЯДКОВЫЙ ЯЗЫК L ПОЗИТИВНО ОБРАЗОВАННЫХ ФОРМУЛ (ПО-ФОРМУЛ) Только 2 логических символа: и !!!

СЕМАНТИКА ЯЗЫКА ПО-ФОРМУЛ Семантика по-формулы определяется обычной (теоретико-модельной, дескриптивной) семантикой соответствующей формулы ( )* классического первопорядкового исчисления предикатов. Соответствие устанавливается так: 1)если A Con, A {F, T}, тогда A = { : A}, F = False, T = True (пропозициональные константы); 2)( X : A)* = x 1 … x m A x 1 … x m { : A}, где {x 1, x 2, …, x m } = X; 3)( X: A :False)* = x 1 … x m (A False) x 1 … x m (A ) x 1 … x m { : A} ; 4)( X : A Ф)* = x 1 … x m (A (Ф)*) = x 1 … x m ( A ( {( )*: Ф}) ); 5)( X : A Ф)* = x 1 … x m (A (Ф)*) = x 1 … x m ( A ( {( )*: Ф}) ).

СЕМАНТИКА ЯЗЫКА ПО-ФОРМУЛ Семантика по-формулы определяется обычной (теоретико-модельной, дескриптивной) семантикой соответствующей формулы ( )* классического первопорядкового исчисления предикатов. Соответствие устанавливается так: 1)если A Con, A {F, T}, тогда A = { : A}, F = False, T = True (пропозициональные константы); 2)( X : A)* = x 1 … x m A x 1 … x m { : A}, где {x 1, x 2, …, x m } = X; 3)( X: A :False)* = x 1 … x m (A False) x 1 … x m (A ) x 1 … x m { : A} ; 4)( X : A Ф)* = x 1 … x m (A (Ф)*) = x 1 … x m ( A ( {( )*: Ф}) ); 5)( X : A Ф)* = x 1 … x m (A (Ф)*) = x 1 … x m ( A ( {( )*: Ф}) ). Теорема: Язык L полон относительно выразительной силы исчисления предикатов (1-го порядка).

При переводе исходной формулы в язык дизъюнктов первоначальная структура знаний разрушается! ПОЧЕМУ ЯЗЫК L ЛУЧШЕ? – ОН ЛАКОНИЧЕН И СОХРАНЯЕТ ЭВРИСТИЧЕСКУЮ СТРУКТУРУ ЗНАНИЙ, оперируя естественными ТК-конструкциями

CТРУКТУРА Позитивно-Образованных ФОРМУЛ (пример) Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n … … … … False S:S: Z: C

CТРУКТУРА Позитивно-Образованных ФОРМУЛ Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Конъюнктивное ветвление … … … … Z: C False S:S:

CТРУКТУРА Позитивно-Образованных ФОРМУЛ Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление … … … … Z: C False S:S:

CТРУКТУРА Позитивно-Образованных ФОРМУЛ Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База … … … … Z: C False S:S:

GENERAL STRUCTURE of PCF-formulae Questions leafs Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y m :B m conjunctive branching Atom base … … … … Z:C False disjunctive branching

CТРУКТУРА Позитивно-Образованных ФОРМУЛ Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База Вопросы … … … … Z: C False S:S:

ЛОГИЧЕСКИЙ ВЫВОД ( в исчислении J с правилом вывода ω ) Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База Вопросы Листья … … … … Z: C False S:S:

ЛОГИЧЕСКИЙ ВЫВОД ( в исчислении J с правилом вывода ω ) Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База Вопросы Листья … … … … Z: C Если B 1 A с подстановкой переменных : Y 1 X, то факты C добавляются к базе А : False S:S:

ЛОГИЧЕСКИЙ ВЫВОД ( в исчислении J с правилом вывода ω ) Z m :D m Z 1 :D 1 X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База Вопросы Листья … … … … Z: C Если B 1 A с подстановкой переменных : Y 1 X, то факты C добавляются к базе А : False S:S: C

CТРУКТУРА Позитивно-Образованных ФОРМУЛ (в общем случае) Z m :D m Z 1 :D 1 True X:A Y 1 :B 1 Y n :B n Дизъюнктивные ветвления Конъюнктивное ветвление База Листья Корень Подформулы … … … … Z: C False S:S:

ЛОГИЧЕСКИЙ ВЫВОД с ИЛИ-параллелизмом: опровержение баз выполняется независимо Z m :D m Z 1 :D 1 True X:A Y 1 :B 1 Y n :B n Дизъюнктивное ветвление База Вопросы Корень … … … … Z: C False … Так как для поиска логического вывода в одной ветви доказательства необходим достаточно большой объем вычислений, а коммуникационные затраты при этом минимальны, то для реализации механизма выбрана библиотека стандарта MPI.

ЛОГИЧЕСКИЙ ВЫВОД с параллелизмом обработки разных вопросов (к одной базе): распараллеливание вопросно-ответной процедуры. Z m :D m Z 1 :D 1 True Y 1 :B 1 Y n :B n Вопросы … … … … Z: C False … X:A При этом объем вычислений, приходящихся на один вопрос, невелик, то при использовании распределенных решений, например библиотеки MPI, возможно снижение эффективности из-за коммуникационных затрат. В связи с этим, для организации параллельной обработки вопросов из сформированной алгоритмом очереди вопросов использована библиотека OpenMP.

ЛОГИЧЕСКИЙ ВЫВОД с параллелизмом поиска ответов B i A на выделенный вопрос Y i :B i : распараллеливание унификации Z m :D m Z 1 :D 1 True Y 1 :B 1 Y n :B n … … … … Z: C False … X:A S.Ferilli, N. Mauro, T. Basile, and F. Esposito «θ-Subsumption and Resolution: A New Algorithm», ISMIS 2003, LNAI 2871, pp. 384–391, [2 S.Ferilli, N.Mauro, T. Basile, and Floriana Esposito «A Complete Subsumption Algorithm», AI*IA 2003, LNAI 2829, pp. 1–13, 2003.

НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ Переформулировка Примера 2 (под метод «от противного»): (Программа, закономерности) (Данные, факты) O(И,П), O(П,С) (Задача (точнее, отрицание ее спецификации)) x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) 1)

НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ Переформулировка Примера 2 (под метод «от противного»): (Программа, закономерности) (Данные, факты) O(И,П), O(П,С) (Задача (точнее, отрицание ее спецификации)) Промежуточная подстановка: И / x, П / y, C / z. Получим: x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) 1)

НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ Переформулировка Примера 2 (под метод «от противного»): (Программа, закономерности) (Данные, факты) O(И,П), O(П,С) (Задача (точнее, отрицание ее спецификации)) Промежуточная подстановка: И / x, П / y, C / z. Получим: O(И,П), O(П,С), Д(И,C) x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) 1) 2)

НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ Переформулировка Примера 2 (под метод «от противного»): (Программа, закономерности) (Данные, факты) O(И,П), O(П,С) (Задача (точнее, отрицание ее спецификации)) Промежуточная подстановка: И / x, П / y, C / z. Получим: O(И,П), O(П,С), Д(И,C) Завершающая подстановка (ответ): И / x '. Получим: x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) 1) 2)

НОВЫЕ МЕТОДЫ ДЕДУКЦИИ И ГИПОТЕЗИРОВАНИЯ Переформулировка Примера 2 (под метод «от противного»): (Программа, закономерности) (Данные, факты) O(И,П), O(П,С) (Задача (точнее, отрицание ее спецификации)) Промежуточная подстановка: И / x, П / y, C / z. Получим: O(И,П), O(П,С), Д(И,C) : False (конец опровержения). Завершающая подстановка (ответ): И / x '. Получим: x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) x' : Д (x', C) : False x, y, z : O (x, y), : Д(x, z) O (y, z) 1) 2) 3)

Пример 6: рекурсивные вычисления факториала: :P(1, 1) x : P (1O, x) : False m,n : P (m, n) : P(m+1, n (m+1)) Программа параметр цикла Дано 1!=1 ( x: P(1O, x) ) Требуется вычислить 1O! ПодстановкиБаза данных 1/m,1/n : : P(1, 1), P(2, 2) 2/m,2/n : : P(1, 1), P(2, 2), P(3, 6) Подстановки База данных 9/m, 9/n : : P(1, 1), P(2, 2),..... P(9, ) 10/m, 10/n : : P(1, 1), P(2, 2),..... P(9, ) P(10, ) Ответ: / x : False

К ФОРМАЛИЗАЦИИ ЗНАНИЙ В ЯЗЫКЕ L ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ (ПО-ФОРМУЛ) Пример. Для некоторых агентов доступны все рабочие станции региональной сети. Ни один агент не имеет доступа к рабочим станциям нашего учреждения. Следовательно, ни одна рабочая станция сети не является рабочей станцией нашего учреждения. Формализация этого утверждения в обычном языке исчисления предикатов приведет к формуле (1) Доказательство (1) логически эквивалентно опровержению формулы Она в языках дизъюнктов (J.A.Robinson, 1965, R.Kowalski, 1974, A.Colmerauer, 1987, A.Nerode, W.Kohn, 1993) и по-формул соответственно запишется: База «данных» Запросы к БД Цель вывода: получить противоречие (False) S(a) ( P(y) L(a,y)) ( S(z) N(u) L(z,u)) P(b) N(b)

ВЫВОД ПРОТИВОРЕЧИЯ за 2 шага применения унарного правила ω или за 4 шага применения бинарного правила резолюции ω θ ={ z y } ω2ω2 θ = { x x 1, z y 1 } S(a) ( P(y) L(a,y) ( S(x) N(y) L(x,y)) P(b) N(b) методом резолюций (за 4 шага) : в исчислении J :

ОСОБЕННОСТИ ИСЧИСЛЕНИЯ J Исчисление над новым языком L (полным, но с меньшим разнообразием формул): одна аксиома T F (не схема!), эквивалентная False, и единственное правило вывода. Правило вывода является одноместной (унарной) операцией эквивалентного преобразования формул из L; для сравнения, самый популярный метод резолюций (J. Robinson) использует двухместную операцию резольвирования, что повышает комбинаторность поиска вывода.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (ЯЗЫКА L И ИСЧИСЛЕНИЯ J ) 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (ЯЗЫКА L И ИСЧИСЛЕНИЯ J ) 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон. 2) По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов (метода резолюций), а для пропозициональных формул - в сравнении с КНФ/ДНФ.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон. 2) По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов (метода резолюций), а для пропозициональных формул - в сравнении с КНФ/ДНФ. 3) По-формула имеет простую и регулярную структуру, т.е. при считывании текста формулы она обладает в определенном смысле предсказуемостью структуры, ввиду поочередного появления в каждой ветви - и -узлов.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон. 2) По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов (метода резолюций), а для пропозициональных формул - в сравнении с КНФ/ДНФ. 3) По-формула имеет простую и регулярную структуру, т.е. при считывании текста формулы она обладает в определенном смысле предсказуемостью структуры, ввиду поочередного появления в каждой ветви - и -узлов. 4) Отрицание по-формулы получается просто инвертированием,. Если по-формула не содержит листа то она невыводима. Отсутствие этого листа - признак выполнимости формулы.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон. 2) По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов (метода резолюций), а для пропозициональных формул - в сравнении с КНФ/ДНФ. 3) По-формула имеет простую и регулярную структуру, т.е. при считывании текста формулы она обладает в определенном смысле предсказуемостью структуры, ввиду поочередного появления в каждой ветви - и -узлов. 4) Отрицание по-формулы получается просто инвертированием,. Если по-формула не содержит листа то она невыводима. Отсутствие этого листа - признак выполнимости формулы. 5) Нет необходимости удалять кванторы процедурой скулемизации, увеличивающей сложность термов и в целом формулы.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА 1) По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон. 2) По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов (метода резолюций), а для пропозициональных формул - в сравнении с КНФ/ДНФ. 3) По-формула имеет простую и регулярную структуру, т.е. при считывании текста формулы она обладает в определенном смысле предсказуемостью структуры, ввиду поочередного появления в каждой ветви - и -узлов. 4) Отрицание по-формулы получается просто инвертированием,. Если по-формула не содержит листа то она невыводима. Отсутствие этого листа - признак выполнимости формулы. 5) Нет необходимости удалять кванторы процедурой скулемизации, увеличивающей сложность термов и в целом формулы. 6) В по-формализме исходная эвристическая структура знания сохраняется лучше.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования. 8) Техника вывода (опровержения) анализирует только ближайшую окрестность корня по-формулы, что позволяет сфокусировать внимание без потери полноты вывода.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования. 8) Техника вывода (опровержения) анализирует только ближайшую окрестность корня по-формулы, что позволяет сфокусировать внимание без потери полноты вывода. 9) Техника вывода может формулироваться в содержательных терминах вопросно-ответной процедуры вместо технических терминов формальной выводимости.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования. 8) Техника вывода (опровержения) анализирует только ближайшую окрестность корня по-формулы, что позволяет сфокусировать внимание без потери полноты вывода. 9) Техника вывода может формулироваться в содержательных терминах вопросно-ответной процедуры вместо технических терминов формальной выводимости. 10) Вывод хорошо совместим с эвристиками конкретных приложений, а также с общими эвристиками управления выводом. Вывод состоит из крупно-блочных шагов, хорошо «наблюдаем и управляем».

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования. 8) Техника вывода (опровержения) анализирует только ближайшую окрестность корня по-формулы, что позволяет сфокусировать внимание без потери полноты вывода. 9) Техника вывода может формулироваться в содержательных терминах вопросно-ответной процедуры вместо технических терминов формальной выводимости. 10) Вывод хорошо совместим с эвристиками конкретных приложений, а также с общими эвристиками управления выводом. Вывод состоит из крупно-блочных шагов, хорошо «наблюдаем и управляем». 11) Техника вывода допускает естественный ИЛИ-параллелизм.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 7) Исчисление J имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении, например, с правилом резольвирования. 8) Техника вывода (опровержения) анализирует только ближайшую окрестность корня по-формулы, что позволяет сфокусировать внимание без потери полноты вывода. 9) Техника вывода может формулироваться в содержательных терминах вопросно-ответной процедуры вместо технических терминов формальной выводимости. 10) Вывод хорошо совместим с эвристиками конкретных приложений, а также с общими эвристиками управления выводом. Вывод состоит из крупно-блочных шагов, хорошо «наблюдаем и управляем». 11) Техника вывода допускает естественный ИЛИ-параллелизм. 12) Выводы получаются легко интерпретируемыми человеком.

ОСОБЕННОСТИ ПО-ФОРМАЛИЗМА (продолжение) 13) Базовое исчисление J обладает свойством простой и сильной модифицируемости семантики. 14) Описанные язык L и исчисление J приведены в варианте без функциональных символов и допускают переформулировку на общий случай. Вместе с тем вопросы работы с равенствами, поддержки индукции и некоторые другие логические вычисления пока остались неисследованными, хотя разработан метод гипотезирования, совмещающий возможности разработанных дедуктивных средств с решением первопорядковых логических уравнений и похожий на процедуры абдукции и генерализации первопорядковых формул. PROLOG-3 и CLP-стиль напоминают это, но соотносятся с методом гипотезирования примерно как метод резолюций и обратный метод Маслова с по-формализмом. 15) Эффективность организации вопросно-ответной процедуры может зависеть от класса решаемых задач. 16) Имеются примеры комбинаторно сложных задач, трудных для известных в литературе систем АДТ и просто решенных в по-формализме, реализованном в виде программной системы КВАНТ/1. Система АДТ реализована на языке программирования С++ с использованием стандартной библиотеки шаблонов STL для обеспечения кроссплатформенности (на кластере под управлением ОС Linux). В качестве коммуникационных средств параллельного программирования используются стандарт передачи сообщений MPI и библиотека функций OpenMP для программирования с разделяемыми переменными.

Таким образом, несмотря на обычные трудности: полуразрешимость исчисления предикатов (A. Church, A. Turing, 1936), вычислительную сложность проблемы разрешимости теоретически разрешимых теорий (их практическая неразрешимость); «практическая разрешимость вместо теоретической» (В.М. Глушков, 1989), монотонность исчисления предикатов, которая ограничивает применение классической логики в задачах с изменяющимся миром, плохую совместимость с эвристиками предметной области, недостаточность одной логики (нужны конструктивные, темпоральные, немонотонные и др. логики, гипотезирование, абдукция и т.д.),... предложенный подход к выбору базовых выразительных и дедуктивных средств позволяет, по крайней мере, для многих важных классов задач преодолеть немонотонность и рекурсивность, повысив адаптируемость базовых средств под классы задач и эффективность поиска выводов. Однако в системе логической обработки знаний «общего» вида остается проблема неполноты описания предметной области, что может приводить к неразрешимости задачи, а также проблемы быстродействия в задачах жесткого реального времени.

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

К ИНТЕЛЛЕКТНОМУ УПРАВЛЕНИЮ СИСТЕМОЙ КАБИН ЛИФТА Этажи Кабина Команды Критерии качества: среднее время ожидания; доля долгих ожиданий (больше 60 сек.); количество переадресаций; энергопотребление; Направления движения Вызов вверх (с временем ожидания) Вызов вниз

ПРИМЕНЕНИЕ ЛОГИКИ J В ЗАДАЧАХ УПРАВЛЕНИЯ В РЕАЛЬНОМ ВРЕМЕНИ: АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ - это предсказать и оценить свойства траекторий системы при альтернативных управлениях (за интервал времени между двумя моментами корректировки управления), отбрасывая нерациональные траектории. Этот подход означает непрерывный синтез теорем о свойствах траекторий вместо АДТ. Используются: 1) аксиома существования следующего момента времени t:T(t) t :T(t ), N(t,t ), где T(t) «t – момент времени», N(t,t ) «момент времени t непосредственно следует за t», 2) соответствующая стратегия вывода. Метод заключается не в доказательстве априори данной теоремы, а в выводе следствий из знаний, т.е. в виде свойств траекторий.

ИНТЕЛЛЕКТНОЕ УПРАВЛЕНИЕ ЛИФТАМИ: СРАВНЕНИЕ С ТРАДИЦИОННЫМ МЕТОДОМ Call Assignment Method – численный метод многокритериальной оптимизации: Обозначения: – вызов вниз, – вызов вверх.

ТРАДИЦИОННЫЙ ПОДХОД К ЗАДАЧЕ x(t+1)=f(x(t), u(t,x(t), v(t), w(t)), t), t=0,1,2,… x 1, …, x n – местоположения кабин лифта; x n+1, …, x 2n – логические переменные (направления движения кабин); v(t) – вектор вызовов с этажей; w(t) – команды изнутри кабин; u(t,x,v,w) – вектор управлений (назначений кабин); q 1 – среднее время ожидания min; q 2 – доля долгих (более 60 сек.) ожиданий min; q 3 – количество переназначений min;..... (комфорт, энергопотребление и т.д.). ЗАДАЧА. Синтезировать u в классе Парето-оптимальных решений. Известный метод. Call Assignment Method – численный метод векторной оптимизации. НЕДОСТАТОК. Жесткость математических моделей. Полезно использовать мягкие (логические) модели. МОДЕЛЬ:

ИНТЕЛЛЕКТНОЕ УПРАВЛЕНИЕ ЛИФТАМИ: СРАВНЕНИЕ С ТРАДИЦИОННЫМ МЕТОДОМ Метод интеллектного управления состоит в логическом упреждающем моделировании динамики системы при альтернативных управлениях и логической оценке качества: Он предпочтительнее известного метода векторной оптимизации (Call Assignment Method), в силу большей адаптивности к условиям эксплуатации (тип здания, специфика некоторых этажей, время суток и т.п.)

АНАЛОГИЯ С ИЗВЕСТНЫМ КОМБИНИРОВАННЫМ ПРИНЦИПОМ УПРАВЛЕНИЯ Принцип обратной связи + принцип компенсации возмущений (J.V. Poncelet) Например, компенсация – на основе статистического предсказания сигналов (А.Н. Колмогоров, А. Хинчин, Н. Винер). Комбинированный принцип используется в САУ с 40 гг. (В.С. Кулебакин, Б.Н. Петров, Г.М. Уланов, А.Г. Ивахненко и др.). В нашем случае формирование обратной связи комбинируется с логическим упреждающим моделированием и оценкой применимости свойств траекторий. Для оценки могут привлекаться эвристики статистической и другой природы.

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

D B (f) B A (g) A G (h) D G?G? D B (f) A (g) G (h) Исходное Конструктивные Задача состояние возможности (цель, конечное состояние) _______________________________________________________________________________________________________________________________________________ Ответ: h(g(f( вход ))) – способ задействования возможностей для получения выхода. (непроцедурный стиль постановки и решения задачи) ОСНОВНАЯ ИДЕЯ АВТОМАТИЗАЦИИ ПРОФЕССИОНАЛЬНОЙ ДЕЯТЕЛЬНОСТИ Пример (формализация в булевской импликативной логике c конструктивной семантикой): рассмотрим формулу D & (D B) & (B A) & (A G) G в конструктивной семантике, A, B, C, D, G – булевские переменные. ВХОДыВХОДы ВыХОДыВыХОДы Дескриптивный вывод и конструктивный совпадают вход выход

БЗ – База знаний. АДТ– Модуль автоматического доказательства теорем. Объект управления (телескоп) Планета Система интеллектного управления АДТ Теорема Синтезированное управление Текущее состояние БЗ НАВЕДЕНИЕ ТЕЛЕСКОПА НА ЦЕНТР ПЛАНЕТЫ В НЕПОЛНОЙ ФАЗЕ (на основе автоматического доказательства теорем, А.А.Фельдбаум, 1960)

НАВЕДЕНИЕ НА ЦЕНТР ПЛАНЕТЫ В НЕПОЛНОЙ ФАЗЕ

ЛОКАЛЬНЫЙ ПОИСК ДЛЯ СКОЛЬЗЯЩЕГО РЕЖИМА

НЕОБХОДИМОСТЬ КОНСТРУКТИВНОЙ ЛОГИКИ Во многих случаях классический вывод не годится для решения прикладных задач, называемых конструктивными. Их особенность заключается в том, что по выводу требуется произвести некоторое построение, заданное целью задачи.* Так, если цель есть дизъюнкция A(x) B(x), то вывод должен давать способ определения по параметрам x, входящим в А и В, какой из случаев имеет место для каждого конкретного набора параметров. Аналогично, если цель есть x А(x), то из вывода должен извлекаться способ построения такого x. В более общем случае : А обозначает конструктивную возможность обеспечить истинность А. __________________________ *) Классический вывод не удовлетворяет этим условиям. Это связано с тем, что в классической логике истинен закон исключенного третьего (tertium non datur): A A. Конструктивная (интуиционистская) логика была аксиоматизирована А. Гейтингом в 1930 г., а в 1932 г., до известных работ Г. Генцена, А.Н. Колмогоров предложил интерпретацию интуиционистских исчислений как исчислений задач. Логика программирования исследована в 80-е гг. Г.Е.Минцем, а также Н.Н.Непейводой (мультилогиковые подходы, выводы в форме графов и т.д.).

(A B) C, (A & B) C – интуиционистски неэквивалентны, но переводятся в одну и ту же по-формулу : True ( : C, :A : B : False) Исчисление задач F : False (доказать невыполнимость F ) с единственной аксиомой : False (Ф) : False и единственным правилом вывода). Любая задача F G может быть заменена выводом в исчислении J по-формулы : True : True ( F, ( G) *). Часть интуиционистских формул не имеют адекватного перевода в язык L по-формул. Например,

Выявлены возможности сильной модифицируемости семантики ранее разработанной в институте первопорядковой логики позитивно- образованных формул, состоящие в том, что только ограничениями применения правила вывода базовой логики получаются логические выводы С требуемыми свойствами: конструктивности, немонотонности, темпоральности и др. Для любой задачи, специфицируемой первопорядковой формулой F G, где F – произвольная формула, описывающая условия и конструктивные средства решения задачи (F непротиворечива и имеет конструктивную интерпретацию всех дизъюнкций и кванторов существования), G – цель, представимая по-формулой в классе формул x 1 … x m (A y i 1... y i m i B i ), где A, B 1, …, B k – конъюнкты, всякий J-вывод по-представления формулы F G конструктивен. k i=1 ИССЛЕДОВАНИЕ НОВЫХ ЛОГИК С НЕКЛАССИЧЕСКОЙ СЕМАНТИКОЙ Теорема о конструктивности выводов:

Развита теория функциональной адаптивности управляемых систем со структурной реконфигурацией на базе конструктивных логических исчислений, предложенных ранее. Пример: структурно реконфигурировать систему управления ориентацией космического аппарата с П-регулятором (h) после обнаружения и локализации отказа, например, датчика (f 1 ) угла. Вместо нормальной структуры h ( f 1, f 2, f 3 ) выводится послеаварийная структура h ( F ( f 2, f 3, g 1, g 2, g 3 ), f 2, f 3 ). h u F f2f2 f3f3 g1g1 g2g2 g3g3 u h f1f1 f2f2 f3f3 Датчики углов (один отказал) П-регулятор Нормальная структур h ( f 1, f 2, f 3 ) : Послеаварийная структура h ( F ( f 2, f 3, g 1, g 2, g 3 ), f 2, f 3 ): – программное средство вычисления угла рысканья по измеряемым двум другим углам и трем скоростям (в выводе используются спецификации программ и аппаратных компонент с последующим извлечением из вывода целевой структуры). F ЛОГИЧЕСКАЯ ТЕОРИЯ ФУНКЦИОНАЛЬНОЙ АДАПТИВНОСТИ УПРАВЛЯЕМЫХ СИСТЕМ x y z x y z ~ ~ ~

ПРИМЕР ФОРМАЛИЗАЦИИ ЗАДАЧИ ПЛАНИРОВАНИЯ ПЕРЕМЕЩЕНИЯ ГРУЗА ВНЕ ХОРНОВСКОГО ЯЗЫКА Имеется два корабля A и B, принимающие груз, поднимаемый двумя аппаратами r 1 и r 2. Известно, где на дне находится груз, который нужно перенести на один из кораблей. Логическая формализация этой обстановки и цели выводит за хорновский формализм ПРОЛОГа, но остается в области применимости исчисления J c. Задачу можно формализовать с помощью следующих правил (действий АНПА). 1) Переместиться к грузу. 2) Если груз и АНПА находятся в одной позиции и схват АНПА свободен, то: либо АНПА может захватить груз (при этом схват переходит в состояние «занят»), либо, если рядом находится второй АНПА, то они оба одновременно могут захватить груз и перейти в занятое состояние. 3) Если АНПА с грузом находится рядом с кораблем, то выгрузить груз (с переходом схвата в состояние «свободен»). 4) Если два АНПА с грузом находятся рядом с кораблем, то выгрузить груз (с переходом схватов в состояние «свободен»). 5) Определить, какой корабль ближе (недальше). Цель задается следующим утверждением: груз выгружен на корабль А, либо на корабль B.

СПОСОБЫ ПРИМЕНЕНИЯ ЛОГИКИ ДЛЯ ФОРМИРОВАНИЯ УПРАВЛЕНИЯ 1.АВТОМАТИЧЕСКОЕ РАЗВЕРТЫВАНИЕ ТЕОРИИ (АРТ), т.е. вывод логических следствий (может быть, дескриптивный) на некоторую глубину просмотра при альтернативных управлениях из конечного набора с оценкой предпочтительности развертываемых «картин мира». 2. АВТОМАТИЧЕСКОЕ КОНСТРУКТИВНОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМЫ (АДТ) F G, где формула F описывает условия и конструктивные средства достижения цели управления, а формула G описывает цель управления, с последующим извлечением управления (последовательности действий) из доказательства. Цель достигается, если не будет неучтенных изменений в мире, иначе требуется итерирование АДТ для корректировки управления. 3. АВТОМАТИЧЕСКАЯ ДЕДУКЦИЯ С ГИПОТЕЗИРОВАНИЕМ (АДГ), т.е. проталкивание «зависшего» вывода порождением гипотез как дополнительных условий достижимости цели управления.

ЛОГИЧЕСКИЕ УРАВНЕНИЯ В ДЕСКРИПТИВНОЙ И КОНСТРУКТИВНОЙ СЕМАНТИКАХ Гипотезирование в задачах с неполной информацией или недостающими средствами D D B C E D&E H K H G K G G? Данные Цель Программа D G ( G недостижима) D&B С – вопрос пользователю: А) верна ли импликация? Б) ввести программу вычисления С по D и B. Логическое уравнение: X & « Данные» & « Программа» G (X= D&B С - решение уравнения ). Автоматизация синтеза диалога!

ЛОГИЧЕСКИЕ УРАВНЕНИЯ В ДЕСКРИПТИВНОЙ И КОНСТРУКТИВНОЙ СЕМАНТИКАХ Гипотезирование в задачах с неполной информацией или недостающими средствами D D B C E D&E H K H G K G G? Данные Цель Программа Непроцедурное программирование, Интеллектное планирование и управление Интеллектный поиск, Интеллектный диалог (интерфейс с пользователем) Автоматизация исследований D G ( G недостижима) Приложения: D&B С – вопрос пользователю: А) верна ли импликация? Б) ввести программу вычисления С по D и B.

РЕШЕНИЕ ЛОГИЧЕСКИХ УРАВНЕНИЙ

ПАРАМЕТРИЗАЦИЯ РЕШЕНИЙ ЛОГИЧЕСКИХ УРАВНЕНИЙ

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: Отрицание: ( False False Отрицание спецификации задачи False Начальная программа:

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: 1) После применения абдукции: Отрицание: ( False False Отрицание спецификации задачи -- False False Начальная программа: - ---

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: 1) После применения абдукции: Отрицание: ( False False Отрицание спецификации задачи -- False False Начальная программа: True,, False 2) После применения :

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: 1) После применения абдукции: Отрицание: ( False False Отрицание спецификации задачи -- False False Начальная программа: True,, False 2) После применения : 3,4) После двух применений :,, False

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: 1) После применения абдукции: Отрицание: ( False False Отрицание спецификации задачи -- False False Начальная программа: True,, False 2) После применения : 3,4) После двух применений :,, False 5) После применения : False

ПЛАНИРОВАНИЕ ДЕЙСТВИЙ С МИНИМАЛЬНЫМ ДООСНАЩЕНИЕМ Пример : Дано: 1) После применения абдукции: Отрицание: ( False False Отрицание спецификации задачи -- False False Начальная программа: True,, False 2) После применения : 3,4) После двух применений :,, False 5) После применения : False Ответ: ( ) – минимальное дооснащение ( и - пустые)

ГИПОТЕЗИРОВАНИЕ КАК «ПРОТАЛКИВАНИЕ ВЫВОДОВ» В ПО-ФОРМАЛИЗМЕ X : A Y: B Z : A(Z / X) – – – U : B (Z / X, U / Y) Формирование гипотезы Ф обеспечивает доступ к знаниям, если нет ответа на Y: B. Итерационный процесс чередования вывода и гипотезирования в случае неуспеха (при исчерпании временного ресурса вывода) завершается применением радикальной гипотезы: Ф = Z : A(Z / X),… : False. Ф

ЛOГИЧЕСКИЕ УРАВНЕНИЯ В АНАЛИЗЕ МОДЕЛЬНЫХ АНАЛОГИЙ 1 ая модель 2 ая модель свойства отображения отношения ………...

ЛОГИЧЕСКИЕ УРАВНЕНИЯ ДЛЯ ПОЛУЧЕНИЯ НОВЫХ ТЕОРЕМ (РАЗВИТИЯ МАТЕМАТИЧЕСКИХ ТЕОРИЙ) Если интерпретировать логическое уравнение (т.е. логическую формулу с известными и неизвестными членами) как заготовку будущей (формируемой) теоремы, например, как заготовку, в которой частично отсутствуют посылки, то вышеупомянутый метод гипотезирования обеспечивает автоматизацию получения самих текстов новых теорем. На этом пути создана метатеория т.н. редукторов и найдены сотни нетривиальных теорем в динамике непрерывно-дискретных, логико- динамических и других классов систем, в теории управления, задачах оптимального управления и многокритериального принятия решений, теории алгебраических систем и других теориях. В качестве лишь примера упомянем, например, тот факт, что этот метод решения логических уравнений перекрывает большую часть результатов монографии A. Michel e.a. «Qualitative Theory of Dynamical Systems», NY-Basel, p.

ЗАКЛЮЧЕНИЕ Ограничения предложенной технологии и задачи на будущее: Синтезируемые решения (планы, управления, программы) скорее рациональны, чем оптимальны. В общем случае обеспечение оптимальности требует дополнительных затрат ресурсов для получения и многокритериального сравнения разных решений между собой.

ЗАКЛЮЧЕНИЕ (продолжение) Ограничения предложенной технологии и задачи на будущее: Синтезируемые решения (планы, управления, программы) скорее рациональны, чем оптимальны. В общем случае обеспечение оптимальности требует дополнительных затрат ресурсов для получения и многокритериального сравнения разных решений между собой. Рассмотренные задачи управления принадлежат классу задач не более, чем мягкого реального времени.

ЗАКЛЮЧЕНИЕ (продолжение) Ограничения предложенной технологии и задачи на будущее: Синтезируемые решения (планы, управления, программы) скорее рациональны, чем оптимальны. В общем случае обеспечение оптимальности требует дополнительных затрат ресурсов для получения и многокритериального сравнения разных решений между собой. Рассмотренные задачи управления в реальном времени принадлежат классу задач мягкого реального управления. Новые классы задач, вообще говоря, требуют адаптации базовых средств дескриптивной позитивной логики (такой адаптацией охвачены, например, некоторые классы задач, потребовавшие формализации в стиле монотонных, темпоральных, конструктивных логик).

ЗАКЛЮЧЕНИЕ (продолжение) Ограничения предложенной технологии и задачи на будущее: Синтезируемые решения (планы, управления, программы) скорее рациональны, чем оптимальны. В общем случае обеспечение оптимальности требует дополнительных затрат ресурсов для получения и многокритериального сравнения разных решений между собой. Рассмотренные задачи управления в реальном времени принадлежат классу задач мягкого реального управления. Новые классы задач, вообще говоря, требуют адаптации базовой средств дескриптивной позитивной логики (такой адаптацией охвачены, например, некоторые классы задач, потребовавшие формализации в стиле монотонных, темпоральных, конструктивных логик). Для охвата параллельных программ с циклами требуется наращивание дедуктивно-абдуктивных методов планирования действий процедурами индукции.

ЗАДАЧИ НА БУДУЩЕЕ: ПРОБЛЕМЫ ФУНКЦИОНАЛЬНОЙ НЕПОЛНОТЫ СОВРЕМЕННЫХ СИСТЕМ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА 1.Проблемы физико-логического интерфейса и архитектур (M.Mукаидоно, 1986, G.Saridis, 1996, И.З.Батыршин, 2007): - автоматизации восприятия (перцепции) и оценки значимости внешних сигналов; встраивание нейросетевых средств для поддержки взаимодействия когнитивных функций восприятия и распознавания образов с логическим умозаключением; - автоматизации формирования понятий и базовых закономерностей.

ЗАДАЧИ НА БУДУЩЕЕ (продолжение): ПРОБЛЕМЫ ФУНКЦИОНАЛЬНОЙ НЕПОЛНОТЫ СОВРЕМЕННЫХ СИСТЕМ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА 1.Проблемы физико-логического интерфейса и архитектур (M.Mукаидоно, 1986, G.Saridis, 1996, И.З.Батыршин, 2007): - автоматизации восприятия (перцепции) и оценки значимости внешних сигналов; встраивание нейросетевых средств для поддержки взаимодействия когнитивных функций восприятия и распознавания образов с логическим умозаключением; - автоматизации формирования понятий и базовых закономерностей. 2.Проблемы функционирования в условиях неполноты информации: - обучения и самообучения; - индукции и абдукции.

ЗАДАЧИ НА БУДУЩЕЕ (продолжение) : ПРОБЛЕМЫ ФУНКЦИОНАЛЬНОЙ НЕПОЛНОТЫ СОВРЕМЕННЫХ СИСТЕМ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА 3. Проблемы актуализации памяти: - иррелевантности знаний решаемой задаче (A.Levy, R.Fikes, V.Sagiv, 1997); - фокусировки внимания; - противоречивости знаний.

ЗАДАЧИ НА БУДУЩЕЕ (продолжение) : 4. Проблемы целеполагания: Полученные результаты, как и другие современные достижения в области интеллектного управления, относятся к проблематике автоматизации поиска способов достижения поставленных извне целей. Достижения в автоматизации целеполагания и пересмотра критериев качества управления совсем незначительны, что и определяет наиболее трудные проблемы интеллектного управления на будущее. Возникают проблемы: - автоматизации самомотивации и использования эмоционального настроя; - автоматизации пересмотра критериев эффективности (качества) достижения цели; - самоцелеполагания; - группового взаимодействия в социуме (кооперативного, конкурентного и смешанного) и пересмотр целей (мультиагентные системы).

СПАСИБО ЗА ВНИМАНИЕ! ВОПРОСЫ???

Васильев Станислав Николаевич АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО И СИНТЕЗ ТЕОРЕМ В ЯЗЫКЕ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ Институт проблем управления им. В.А.Трапезникова РАН СПАСИБО ЗА ВНИМАНИЕ! ВОПРОСЫ???