Васильев С.Н. - Логический подход к управлению динамическими системами (1072115), страница 2
Текст из файла (страница 2)
Следует заметить, что, по крайней мере, в отечественной литературе на возможность и перспективность использования автоматического доказательства теорем в теории и практике управления указал еще в 1960 г. А.А. Фельдбаум [16].
На наш взгляд, проникновение полных первопорядковых логик и методов автоматизации логического вывода (в частности, в форме АДТ) в сферу интересов и компетентности специалистов по теории управления является весьма существенным, позволяя развить теорию управления в направлении расширения потенциала решения сложных задач управления, увеличения степени автоматизации, создания СИУ, в большей степени оправдывающих свое название, благодаря повышению уровня их интеллектуальности. При этом теория управления и искусственный интеллект становятся значительно более совместимыми, поскольку предикатные языки (1-го и более высоких порядков) существенно более выразительны и охватывают вещественные и другие переменные. Грубо говоря, выразительная сила предикатных языков так соотносится с выразительной силой булевских (пропозициональных) языков, как выразительная сила языка математической теории управления соотносится с выразительной силой языка двоичной арифметики. Предикатные языки позволяют формализовать более широкие знания для последующей обработки машинно-ориентированными правилами. Каждый шаг вывода формализует не столько специальный (локальный) переход от условий к действию (как при использовании инструктивных знаний), выражающий более или менее очевидным образом отдельный шаг приближения к цели управления, сколько интуитивное представление человека о правильности (логичности) умозаключений, т.е. имеет более универсальный характер.
Вместе с тем в АДТ, как в математически строгой части направления “General Reasoning” (“Рассуждения общего вида”, т.е. рассуждения, не стесненные, например, сильно ограниченным синтаксисом представления знаний в системах, основанных на правилах), остаются и дают знать о себе старые проблемы, породившие разные новые концепции организации компьютерных рассуждений: немонотонные логики (Nonmonotonic Logics), неформальные логики (Informal Logics), аргументирование (Argumentation), реторика (Rhetoric), пересмотр взглядов (Change of View), практические рассуждения (Practical Reasoning) и др. [17].
Неустранимо принципиальное противоречие между выразительностью формальных языков и разрешимостью проблемы дедукции (А.Тьюринг, А.Черч). Более того, даже теоретически разрешимые теории или их фрагменты могут быть практически неразрешимы по причине высокой сложности вычислений. Несмотря на вот уже 40 лет декларируемую важность эвристик для поиска вывода, а также опыта, в том числе ставшего алгоритмическим знанием, нет понимания механизмов их усвоения и использования. В частности, из-за эвристик может теряться полнота, но не должна теряться корректность. Необходимы новые идеи для придания “второго дыхания” системам автоматизации рассуждений (ср. ситуацию с нейросетями, п. 2).
Нам удалось средствами позитивных логических исчислений, разработанных в ИДСТУ СО РАН и обсуждаемых далее, обеспечить так называемую “практическую разрешимость” в смысле В.М. Глушкова, когда в дополнение к теоретической универсальности (полноте) или вместо нее система автоматизации дедукции обладает в конкретной, может быть, достаточно узкой, предметной области “творческими способностями”, соизмеримыми с интеллектом специалистов рассматриваемой области. При этом огромная роль отводится эффективной совместимости логики с эвристиками и адаптируемости логики под специфику предметной области. Свойство практической разрешимости обнаруживается здесь на конкретных задачах интеллектного управления динамическими системами и, в частности, проявляется в преодолении проблем немонотонности, рекурсивности, обеспечения конструктивности выводов и др. Это утверждает нас в позиции, что “логика станет для ИИ тем же, чем является математика для науки” [17].
-
Представление и обработка знаний
средствами позитивных исчислений
Разработан язык позитивно-образованных формул (по-формул) [18]. Он лучше приспособлен, чем известные, для усвоения как эвристик, так и опыта, поскольку достаточно однороден и в то же время хорошо структурирован. Это полный язык первого порядка, формулы которого представляются как деревья: каждый узел суть позитивный квантор, т.е. выражение, содержащее последовательно знак квантора или
, множество индивидных переменных и условие на эти переменные, именуемое конъюнктом. Конъюнкт – это множество атомов или False (без ограничения общности рассматривается случай отсутствия функциональных символов). По определению,
для любого конъюнкта
. По каждой ветви знаки кванторов чередуются. Пустое
обозначается True.
Семантика -узлов такова: по-формула
понимается в исчислении предикатов (ИП) как формула
где
– образ по-формулы
в ИП,
совпадает с
если
иначе
. При
получаем просто формулу
Семантика
-узлов определяется аналогично (с заменой
на
, а обеих связок
на
); при
получаем конъюнктивное ветвление, а при
Без ограничения общности можно считать, что всякая по-формула начинается с корня
(дизъюнкция при
), и рассматривать ее как непустое множество деревьев с экзистенциальными корнями и листьями.
Позитивное исчисление суть пара
где
– аксиома,
– правило вывода. В качестве аксиомы выбрано противоречие
поскольку всякий
-вывод по-формулы
будет опровержением
.
Узлы следующие непосредственно за корнем (базой)
, называются вопросами, и, если
, где
– подстановка, то говорим, что вопрос
имеет ответ
. Правило вывода
в
состоит в использовании ответа. Выводом называется последовательность по-формул, начинающаяся с
и заканчивающаяся аксиомой
, а каждое применение правила вывода соответствует переходу от рассматриваемой формулы к непосредственно следующей по правилу
. Таким образом, поиск вывода можно представить как некоторую вопросно-ответную процедуру.
Пусть может быть пустым. Правило вывода
, примененное к
, дает результат
и имеет вид
где вопрос и подстановка (ответ)
таковы, что
а множества
состоят из новых, различных переменных. Используются упрощения
если
Ш.
Теорема 1 [18]. Исчисление корректно и полно. Иначе говоря, во-первых, для любой по-формулы
имеет место логическая эквивалентность
а во-вторых,
выводимо в
тогда и только тогда, когда
общезначимо.
В частности, для любых по-формул и
, где
– посылка задачи
), а
– цель задачи, таких, что
– логическое следствие
, средствами
задача разрешима, т.е. формула
выводима в
, где
– отрицание
(получаемое простым инвертированием в
символов
).
Пример 1. Отрицание формулы ИП
в по-формализме может иметь вид:
Следующая последователь-ность по-формул является
-выводом формулы
:
,
,
,
-
Особенности по-формализма
Хотя семантика по-формул очень прозрачная и определяется как обычная (классическая, теоретико-модельная) семантика соответствующих образов этих формул в ИП, по-формулы довольно необычны по своей форме, а по-формализм в целом имеет ряд важных особенностей, расширяющих потенциал логического подхода к представлению и обработке знаний и определяющих его эффективность в приложениях (см. п.п. 7-10). Рассмотрим эти особенности.
1. По-формула имеет крупно-блочную структуру, все элементы которой суть только позитивные кванторы всеобщности и существования. Тем не менее, язык по-формул полон относительно выразительности первопорядковых языков.
2. По-представление для первопорядковых формул более компактно, чем в языке дизъюнктов [19] (в методе резолюций), как и для пропозициональных формул – в сравнении с представлениями в стандартных нормальных формах (дизъюнктивных и конъюнктивных).
3. По-формула имеет простую и регулярную структуру, т.е. при считывании текста формулы она обладает в определенном смысле предсказуемостью структуры, ввиду поочередного появления в каждой ветви - и
-узлов.
4. Отрицание по-формулы получается просто инвертированием символов .
5. Нет необходимости предварительно в исходной первопорядковой формуле удалять кванторы существования процедурой скулемизации (как это требует применение метода резолюций), увеличивающей сложность термов и в целом формулы.
6. В по-формализме исходная эвристическая структура знания сохраняется лучше, благодаря тому, что естественно-языковое представление знаний никогда не использует “теоретических” кванторов и, наоборот, широко задействует типовые кванторы
++),
++). Использование в по-формулах позитивных кванторов как частного случая типовых кванторов означает, что выражения
имеют очень простой (и эффективный для обработки по-формул) вид (конъюнкции атомов). По-структура особенно близка к исходной структуре знания, если оно записано как выражение, образованное из литералов (атомов и/или их отрицаний) с помощью позитивных кванторов и логических связок
, т.к. в этом случае по-структура может отличаться от исходной просто появлением кванторов
(вместо упомянутых связок
) и/или заменой отрицаний атомов
подформулой
.
7. Исчисление имеет единственное, унарное и крупно-блочное правило вывода, благодаря чему размерность комбинаторного пространства поиска выводов уменьшается в сравнении с правилом резольвирования в методе резолюций, которое хотя тоже является единственным правилом, но бинарное и мелко-блочное.