Содержание к диссертации
ВВЕДЕНИЕ 4
L Актуальность задачи поиска вывода 7
2. Цель работы и задачи диссертации 9
3- Методы построения алгоритма и исследований 11
Апробация работы 11
Научная новизна и практическая ценность результатов работы 12
Личный вклад 13
Основные положения, выносимые па защиту 4 * 14
Постановка задачи 15
Обзор родственных работ 18
10. Структура работы 21
ГЛАВА I. ЛОГИЧЕСКАЯ СИСТЕМА S5 (КТ45) 22
1.1. Синтаксис и семантика модальной логики S5 22
1.1 Л, Семантика возможных миров 26
1 Л.2. Свойство немонотонности автоэпистемической логики 29
1ЛЗ. Автоэпистемическая логика, ее язык, синтаксиси семантика 31
1ЛА Семантика возможных миров автоэпистемической логики 34
1X Понятие мультимножества и исчисление секвенций для системы S5 36
1.2Л. Общая схема обратного метода установления выводимости 38
1.3. Прямое исчисление S5seq и обратное исчисление S5*nv 39
1а выводы по главе 44
щ ГЛАВА П. ИСЧИСЛЕНИЕ ПУТЕЙ ДЛЯ СИСТЕМЫ S5 45
2Л. Исчисление путей S5*pATh (прямое исчисление путей) 45
2.2. Обратное исчисление путей S5*nv 48
23. выводы по главе 50
ГЛАВА Ш. УСТРАНЕНИЕ ИЗБЫТОЧНОСТЕЙ ИСЧИСЛЕНИЯ ПУТЕЙ...51
ЗЛ. Критерии избыточности для обратного метода 51
3.2. Стратегия Ф-упорядочения 56
3.2.1. Алгоритм упорядочения 61
* 3.3. Полнота обратного метода исчисления S5% без секвенций, не относящихся
к«»> 71
Предпосылка как критерий избыточности 81
Общий алгоритм установления выводимости 91
Выводы по главе 92
ГЛАВА IV. ПРИМЕНЕНИЕ ОБРАТНОГО МЕТОДА УСТАНОВЛЕНИЯ
ВЫВОДИМОСТИ ДЛЯ МЕХАНИЗМА ВЫВОДА ЭКСПЕРТНЫХ
СИСТЕМ 93
4.1. Пример оболочки экспертной системы на основе классического нечеткого
ВЫВОДА 96
4.2. Практической применение обратного метода установления выводимости для
автоэпистемичекой логики 101
Оценка актуарных гипотез ПФР 102
Анализ производственной мощности предприятия 109
4.3. Выводы по главе 116
ЗАКЛЮЧЕНИЕ 117
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ 120
ПРИЛОЖЕНИЕ 1 128
ПРИЛОЖЕНИЕ 2 129
ПРИЛОЖЕНИЕ 3 130
ПРИЛОЖЕНИЕ 4 131
ПРИЛОЖЕНИЕ 5 140
ПРИЛОЖЕНИЕ 6 148
Введение к работе
В последнее время интенсивно рассматриваются вопросы автоматизации процессов получения решений компьютерными программами - это связано не только с классическими задачами искусственного интеллекта доказательства теорем и построения советующих экспертных систем, но и с бурным развитием и внедрением в производственный процесс корпоративных информационных ERP— систем, CRM-систем [], программ управления технологическими процессами, задач извлечения данных и знаний: анализ данных, анализ документов, поиск по смыслу в Internet, распознавание текста и так далее [9]. Несмотря на то, что для решения указанных вопросов успешно применяются такие технологии, как нейронные сети, семантические сети и фреймы, набирает рост и интерес к традиционному логическому методу хода рассуждений за счет привлечения неклассических модальных логик. Наличие большого числа эвристик в рассуждениях соответствующих систем, их неспособность всегда четко обосновать свое решение ставят под сомнение применение нелогических способов рассуждений. В свою очередь, вывод, опирающийся на одну из модальных логик, сохраняет строгость и обоснованность классических аксиоматических систем вывода, однако при этом он гибок за счет наличия операторов а (необходимости) и 0 (возможности). Так же многие модальные логики обладают свойством немонотонности, позволяющим пересматривать свои выводы в процессе рассуждения.
В частности, проблему построения доказательства заданного целевого утверждения для экспертной системы можно свести к проблеме поиска вывода формул определенного логико-математического языка в соответствующем исчислении. Для теорий, основанных на классической логике, исходным пунктом в решении проблемы поиска вывода является, как правило, решение проблемы поиска вывода в исчислении предикатов первого порядка, на базе которого (добавляя те или иные аксиомы и правила вывода) осуществляется формализация различных математических теорий. Имеются многочисленные работы как в области теории логического вывода в классическом исчислении предикатов и
теории разрешимых фрагментов этого исчисления, так и в области практического построения алгоритмов программ автоматического поиска вывода. Для автоматизации доказательства недостаточно решить удовлетворительно проблему автоматического поиска вывода в исчислении предикатов, особенно в случае, когда соответствующее теории исчисление имеет дополнительные правила вывода. Такой случай имеет место, например, при задании исчисления с равенством путем добавления не только аксиом, но и правил для равенства. Для успешной формализации желательно, чтобы методика построеїшя алгоритмов автоматического поиска вывода допускала распространение на различные системы. Один из успешных примеров реализации такого алгоритма, реализующего обратный метод установления выводимости для модальной логики КТ9 описал в работе В.В. Бурлуцкого [б]. В нем используется логика знаний, где оператор интерпретируется как «известно».
Рассмотрим основные подходы для модифицируемых рассуждений, К основным семействам немонотонных логик [33], [34], [7] можно отнести:
Логики умолчаний [72], Они позволяют формализовать модифицируемые рассуждения с помощью правил вывода, присущих области применения. Эти знания выражают правила вида «большинство птиц летает» в форме «если непротеворечив (выполним) вывод, что некая отдельная птица может летать, то она летает». Здесь есть возможность выражать правила с исключениями, не перечисляя сами эти исключения,
Модальные немонотонные логики Мак-Дермотта [62], [63]. Эти логики базируются на аксиоматических системах модальной логики и предназначены для характеризации множеств взаимно «выполнимых» утверждений, которые можно вывести из какого-то задаваемого множества посылок,
Автоэпистемические логики [67], [68], [69]. Это реконструкция немонотонных логик Мак-Дермотта, Взяв какую-либо систему модальной логики, предполагают, что некий идеально разумный агент рассуждает интроспективным образом в рамках выбранной системы и на основе своих
собственных предположений. Рассуждения, проводимые агентом, являются модифицируемыми, ибо относятся к определенному состоянию знаний, которое может оказаться изменчивым. Хотя автоэпистемические логики и логики умолчаний создавались для различных применений, их выразительные возможности часто бывают равносильными [55]. Особо стоит отметить подходы через минимизацию [34], предназначенные для формализации модифицируемых рассуждений и естественно вписывающиеся в
рамки классической логики. Вывод в таких системах основан на минимизагщонных соглашениях для стратегии обращения к неизвестным сведениям- Будучи примененным к базам данных, содержащим только сведения в элементарной логической форме, такое соглашение состоит в опровержении все еще незаписанной информации; истинной предполагается информация, явно присутствующая в базе данных, а вся остальная позитивная информация считается ложной. При обобщении на базы знаний эти соглашения состоят в
более громоздких условиях минимальности, связанных с множествами определенных сущностей, удовлетворяющих некоторым формулам данной базы знаний. В качестве указанных минимизационных соглашений могут служить гипотеза замкнутого мира [71], [73], [75], [76], которая формулируется в виде принципов и методов, позволяющих управлять запросами базы знаний немонотонным образом по отношению к эволюции содержимого этой базы. Соглашения могут также принимать вид аксиом или схем аксиом, которые должны быть добавлены к рассматриваемой базе знаний, например, аксиом пополнения [57], [75], [76], [77] или аксиом очерчивания [60], [61] [58], [59]. В логическом программировании, например, в языке Пролог [5], [32], [1] специальные операторы аппроксимируют логическое отрицание с помощью некоторой конечной процедуры отрицания через неудачу [34], [57], [77], Эти операторы позволяют доказать модифицируемым образом, что некое утверждение нельзя вывести на основе знаний, имеющихся в логической программе, В наиболее общем виде минимизационные соглашения представляются различными операциями разграничения областей истинности предикатов и формул из базы
знаний, а также разграничения множеств и областей констант и функций этой базы. Эти операции взаимодействуют согласно определенным приоритетам и являются выразителями специфической рациональности рассуждающего агента [44], [34].
Укажем, что большинство методов формализации модифицируемых рассуждений обосновывается с помощью логического семантического анализа, часто с применением ослабленных отношений семантического следования. Данные отношения свойственны логическим системам, позволяющим осуществлять вывод утверждений в определенных моделях посылок.
Похожие диссертации на Обратный метод установления выводимости для автоэпистемической логики и его применение в экспертных системах
