Формальная теория структурных моделей описания информационных систем и методы установления выводимости

• Автор: Новосельцев, Виталий Борисович
• Шифр специальности: 05.13.01
• Научная степень: Докторская
• Год защиты: 2006
• Место защиты: Томск
• Количество страниц: 207 с. : ил.

Введение.

Глава 1. Логические подходы к управлению знаниями.

1.1. Подход на базе классических и интуиционистских теорий

1.2. Модальные логики.

1.3. Дескриптивные логики.

1.4. Выводы.

Глава 2. Структурные функциональные модели

2.1. Язык теории. Основные определения

2.2. Нерекурсивные детерминированные Смодсли.

2.3. Рекурсивные детерминированные Смодели.

2.4. Интерпретация Смодели.

2.5. Выводы.
Глава 3. Установление выводимости в РДСмодели
3.1. Формальное исчисление. Правила вывода
3.1.1. Исчисление .
3.1.2. Корректность и полнота исчисления 5
3.2. Стратегия и алгоритм вывода в классе РДС.
3.2.1. Описание алгоритма.
3.2.2. Корректность алгоритма построения вывода.
3.2.3. Особенности введения рекурсии
3.3. Проблемы реализации систем построения вывода.
3.4. Выводы.
Глава 4. Модальная логика и обратный метод
4.1. Базовые понятия и соглашения.
4.1.1. Синтаксис и семантика логики КТ.
4.1.2. Мультимножества и секвенции.
4.1.3. Прямое и обратное исчисление секвенций для логики знания .
4.2. Исчисление путей для логики КТ
4.2.1. Прямое исчисление путей.
4.2.2. Обратное исчисление путей.
4.3. Анализ избыточностей и полнота К4
4.4. Выводы
Глава 5. Фупорядочснис
5.1. Определения и соглашения
5.2. Полнота КЬ без секвенций, относящихся к
5.3. Предпосылка как критерий избыточности.
5.4. Выводы
Заключение.
Список цитируемой литературы


Они также могут быть использованы для реализации и исследования экономических моделей с конкурентным взаимодействием субъектов, децентрализованных комплексов управления сложными прикладными структурами, распределенных информационных систем различного назначения. Апробация работы. International Symp. Международная конференция «Всесибирские чтения но математике и механике. Korean-Russian International Symposium on Science and Technology -KORUS , Новосибирск, НГТУ. Формальная теория структурных рекурсивных импликативных моделей SR для описания моделей различных прикладных областей. Эффективные обратные стратегии и алгоритмы установления выводимости формулы в теории SR. Формальный подход к установлению выводимости формул для модальных систем классов КТ и КТ (S5) с использованием обратного метода. Строго обоснованные стратегии сокращения пространства поиска вывода в модальных системах на базе Ф-упорядочсния, обеспечивающие реализацию надежных и эффективных интеллектуальных программных комплексов. Объем и структура диссертации. Диссертация включает введение, пять глав, заключение и список литературы; общий объем составляет 7 страниц, включая иллюстрации. Глава 1. Возможности организации и автоматической (алгоритмической) обработки информации привлекала внимание исследователей с давних нор. По сути дела первые такие попытки восходят к временам Эвклида, которому приписывается формулирование алгоритма поиска наибольшего общего делителя двух целых чисел. С появлением и развитием компьютерной техники и соответствующего программно-математического инструментария интерес к исследованиям в отмеченной области только возрос, причем значительные усилия прикладываются к вопросам моделирования интеллектуальных процессов. Можно утверждать, что приоритеты в /Г-области сместились - от инженерных расчетов мы все более переходим к анализу когнитивной информации. Рассмотрим наиболее популярные технологии управления знаниями, в той или иной степени опирающиеся на логический аппарат. Логика, как инструмент анализа абстрактных построений, связанных с моделированием «интеллектуальных» процессов, предлагает широкий набор теорий, обеспечивающих работу со знаниями. Понятие «знание» при этом трактуется, разумеется, не в общефилософском смысле, а значительно уже. В частности, размеченные дуги в семантических сетях или фишки (переходы) в сетях Петри также могут быть промоделированы нагруженными импликациями. Зачастую, проблема построения выводов из некоторых исходных данных заключается в том, что анализ антецедента простой импликации типа «если Р, то Q» связан с необходимостью учета контекста, в котором данное предложение имеет место, то есть с учетом пути, приведшего к посылке импликации. Традиционно считается, что устанавливать выводимость целевой формулы в рамках некоторой теории следует, продвигаясь от этой формулы к аксиомам теории. Основным мотивом при этом является желание избежать излишних построений. Однако это разумное, в общем-то, желание осложняется необходимостью производить возвраты в процессе поиска, когда выясняется, что очередная подцель не может быть реализована. Таким образом, за «минимальность» вывода приходится платить накладными расходами (и неестественностью) при организации бэктрекинга. Подходы, когда доказательство осуществляется в «обратном» направлении (от аксиом), свободны от возвратов, но, без применения специальных стратегий, приводят к существенному (как правило, экспоненциальному) росту пространства вывода. ПО), которые поддерживают так называемый обеспеченный вывод. Обеспеченность вывода здесь понимается следующим образом: применение правил построения заключений из ранее определенных фактов не зависит от текущего состояния системы либо определяется сірого заданными метаправилами, а правил и метаправил - существенно ограниченное количество. К теориям подобного сорта, в частности, можно отнести классическую механику, радиотехнику (без учета квантовых эффектов) и ряд иных хорошо формализованных предметных областей. Проблемы выводимости для таких ПО достаточно глубоко исследованы в ряде работ отечественных и зарубежных авторов, главным образом, в связи с решением задачи автоматического синтеза расчетных проірамм (см. Минц и Тыугу ], [Минц ], [Неиейвода ,] и др.