Содержание к диссертации
Введение
Глава 1. Анализ методов логического вывода и систем обработки знаний... 11
1.1 Методы логического вывода 11
1.1.1 Формальные системы 11
1.1.2 Формальная система исчисления высказываний 11
1.1.3 Классификация методов логического вывода 14
1.1.4 Метод деления дизъюнктов 16
1.1.5 Абдуктивный логический вывод 19
1.1.5.1 Понятие абдуктивного вывода 19
1.1.5.2 Подходы к характеристике абдуктивного вывода 22
1.1.5.3 Подходы креализации абдуктивного вывода 23
1.1.5.4 Применение абдукции 24
1.2 Системы обработки знаний 26
1.2.1 Определение и структура систем обработки знаний 26
1.2.2 Классификация систем обработки знаний 29
1.2.3 Принципы функционирования систем обработки знаний 31
1.2.4 Методика построения систем обработки знаний 33
1.2.5 Стратегии получения знаний 35
1.2.6 Оценка эффективности систем обработки знаний 41
1.3 Методы формирования знаний в СОЗ 43
1.3.1 Классификация методов формирования знаний в СОЗ 43
1.3.2 Индуктивное обучение 44
1.3.2.1 Структурно-логические методы 44
1.3.2.2 Признаковые методы 46
1.3.2.3 Методы извлечения знаний из баз данных 48
1.3.3 Обучение на основе дедукции 49
1.3.4 Обучение на основе аналогии 50
1.3.5 Обучение на основе абдукции 51
1.4 Выводы по главе 1 53
Глава 2. Разработка методов логического вывода с изменением посылок 55
2.1 Постановка задачи логического вывода 55
2.2 Метод добавления посылок 60
2.2.1 Теоретические основы метода 60
2.2.2 Пример логического вывода 68
2.3 Метод удаления посылок 76
2.3.1 Теоретические основы метода 76
2.3.2 Пример логического вывода 82
2.4 Абдуктивный метод модификации посылок 90
2.4.1 Теоретические основы метода 90
2.4.2 Пример логического вывода 95
2.5 Выводы по главе 2 104
Глава 3. Разработка модуля формирования знаний 109
3.1 Структура модуля формирования знаний 109
3.1.1 Обобщенная структура модуля 109
3.1.2 Детализированная структура модуля 111
3.2 Принципы функционирования и построения систем обработки знаний с модулем формирования знаний 114
3.2.1 Режимы работы системы обработки знаний 114
3.2.2 Режим дедуктивного вывода 114
3.2.4 Создание базы знаний 120
3.2.5 Особенности построения систем обработки знаний с модулем формирования знаний 121
3.3 Оценка эффективности систем обработки знаний с модулем формирования знаний 125
3.3.1 Критерии эффективности 125
3.3.2 Расчет времени обучения 125
3.3.3 Расчет степени модификации 128
3.4 Выводы по главе 3 132
Глава 4. Разработка программных реализаций модуля формирования знаний 134
4.1 Разработка программных реализаций методов с изменением посылок 134
4.1.1 Общая характеристика программных реализаций 134
4.1.2 Программа реализации метода добавления посылок 135
4.1.2.1 Структура программы 135
4.1.2.2 Разработка интерфейса пользователя 138
4.1.3 Программа реализации метода удаления посылок 142
4.1.3.1 Структура программы 142
4.1.3.2 Разработка интерфейса пользователя 144
4.1.4 Программа реализации абдуктивного метода модификации посылок 147
4.1.4.1 Структура программы 147
4.1.4.2 Разработка интерфейса пользователя 150
4.2 Разработка системы поддержки принятия решений по выбору сотовых телефонов 153
4.2.1 Общие характеристики 153
4.2.2 Структура системы 154
4.2.3 База знаний. 155
4.2.4 Режим консультации 159
4.2.5 Режим обучения 159
4.2.6 Разработка интерфейса пользователя 162
4.3 Разработка программной модели системы распознавания символов... 166
4.3.1 Общие характеристики 166
4.3.2 Структура системы 166
4.3.3 Режимы работы 168
4.3.5 Топологические признаки распознавания 169
4.3.6 Представление символов в базе знаний 174
4.3.7 Режим обучения 1764.3.8 Разработка интерфейса пользователя 177
4.4 Выводы по главе 4 180
Заключение 182
Список сокращений 188
Библиографический список 189
- Формальная система исчисления высказываний
- Постановка задачи логического вывода
- Структура модуля формирования знаний
- Разработка программных реализаций методов с изменением посылок
Введение к работе
Актуальность темы исследования. В настоящее время интеллектуальные системы получили широкое распространение. В наибольшей степени это утверждение справедливо для экспертных систем, систем поддержки принятия решений, интеллектуальных баз данных, систем распознавания образов. Лучшим подтверждением успешности интеллектуальных систем может служить тот факт, что многие подобные системы перешли в разряд повседневных программ.
Но, несмотря на имеющиеся успехи, остаются и проблемы в разработке интеллектуальных систем. В частности, если система претендует на «интеллектуальность», то она должна обладать развитыми способностями к обучению. В современных интеллектуальных системах наибольшие успехи в обучении достигнуты при использовании нейронных сетей.
Процесс обучения с применением нейросетевых технологий начинается с предъявления системе набора обучающих примеров, состоящих из входных и выходных сигналов. Затем нейронная сеть автоматически подстраивает свои синаптические веса таким образом, что при последующем предъявлении входных сигналов на выходе получаются требуемые сигналы. Недостатком данного подхода являются трудности, возникающие при попытках семантической интерпретации механизмов работы нейронной сети. Кроме того, малоисследованным остается вопрос, каким образом представляются знания в нейронных сетях.
Указанные недостатки отсутствуют в системах на основе баз знаний, использующих для обучения логический вывод (ЛВ). При этом под способностью к обучению понимается возможность создания базы знаний, а также пополнение и модификация правил в базе знаний под влиянием вновь полученной информации.
Большинство современных интеллектуальных систем, использующих ЛВ, позволяет модифицировать базу знаний только в ручном режиме. Поль-
зователь может вносить новые правила и удалять старые, при этом система осуществляет только контроль непротиворечивости информации, а существующая информация никак не учитывается. Возможны ситуации, когда вместо добавления пяти новых правил, без учета уже существующих, требуется добавить всего одно, которое дополняет имеющуюся информацию.
Известные методы формирования знаний (или методы машинного обучения), позволяющие автоматически изменять базу знаний, основаны на применении индуктивного ЛВ. Индукция подразумевает наличие достаточно представительной выборки обучающих примеров, которая обобщается посредством сгенерированных правил.
В связи с этим представляет интерес машинное обучение на основе абдукции, которое позволяет ограничиться небольшим числом наблюдений (от одного) и дает возможность максимального учета существующей в базе знаний информации.
Кроме того, использование абдуктивного вывода позволяет интеллектуальным системам приобрести некоторые свойства, ранее доступные лишь на основе нейросетевого подхода, например, возможность автоматической модификации («настройки») базы знаний под воздействием небольшого набора обучающих заключений, которые должны выводиться (или не выводиться) из посылок этой базы знаний.
Однако в настоящее время абдуктивный вывод в методах формирования знаний либо не применяется, либо используется в качестве вспомогательного.
Таким образом, является актуальной задача разработки методов и средств, основанных на абдуктивном ЛВ, для формирования баз знаний в интеллектуальных системах.
Значительный вклад в разработку и исследование методов обучения интеллектуальных систем внесли М. Л. Цетлин, М. М. Бонгард, Я. 3. Цыпкин, Д. А. Поспелов, В. К. Финн, Г. С. Осипов, В. Н. Вагин, Т. А. Гаврилова, В. Ф. Хорошевский, П. Гаек, Т. Гавранек, С. Осуга (S. Osuga), Ю. Саэки
(U. Saeki), А. Сэмюэль (A. Samuel), Э. Хант (E. Hunt), Д. Марин (J. Marin), Ф. Стоун (P. Stone), P. Михальски (R. Michalski), Д. Карбонелл (J. Carbonell), Т. Митчелл (Т. Mitchell), Д. Куинлан (J. Quinlan).
Абдуктивный JIB исследовался в работах Ч. С. Пирса (С. S. Pierce),
В. К. Финна, В. Н. Вагина, Е. Ю. Головиной, Д. А. Страбыкина,
М. Л. Долженковой, Д. Габбая (D. Gabbay), П. Сметса (P. Smets), К. Бутилье (С. Boutilier), П. Флеча (P. Flach), А. Какаса (A. Kakas), К. Иноуэ (К. Inoue), Ч. Сакама (С. Sakama), Дж. Джозефсона (J. Josephson), С. МакИлрайта (S. Mcllraith), Дж. Пола (G. Paul) и др.
Целью исследования является разработка абдуктивных методов модификации посылок в исчислении высказываний и построение на основе этих методов модуля формирования знаний для интеллектуальных систем.
Для достижения указанной цели необходимо разработать:
метод добавления посылок;
метод удаления посылок;
абдуктивный метод модификации посылок;
структуру, принципы функционирования и критерии эффективности модуля формирования знаний;
программные реализации абдуктивных методов модификации посылок и интеллектуальных систем с модулем формирования знаний.
Методы исследования. Для достижения поставленной в работе цели использовались методы научного анализа и синтеза, теории множеств, теории графов, математической логики, теории логического и объектно-ориентированного программирования.
Научная новизна исследования состоит в следующем:
- разработан метод добавления посылок в исчислении высказываний,
позволяющий находить такие посылки, при добавлении которых в базу зна
ний требуемое заключение становится выводимым, и отличающийся от из
вестных абдуктивных методов тем, что находится не единственная посылка,
а семейство множеств дополнительных посылок, определяющее различные варианты пополнения базы знаний;
разработан метод удаления посылок в исчислении высказываний, позволяющий находить такие посылки, при удалении которых из базы знаний требуемое заключение становится невыводимым, и отличающийся от известных методов тем, что находится не единственная посылка, а семейство множеств удаляемых посылок, определяющее различные варианты исключения посылок;
разработан абдуктивный метод модификации посылок в исчислении высказываний, отличающийся процедурой комбинированного добавления и удаления посылок базы знаний с использованием трех методов ЛВ - дедуктивного вывода, метода добавления посылок и метода .удаления посылок, и позволяющий автоматически модифицировать посылки с учетом существующей информации;
введены операции над семействами множеств дизъюнктов - произведения семейств, дизъюнктивного добавления дизъюнкта к семейству дизъюнктов, конъюнктивного умножения семейства на логическую переменную, позволяющие в результате логического вывода получать не отдельную посылку или множество посылок, а семейство множеств посылок;
предложены критерии эффективности модуля формирования знаний на основе абдуктивного метода модификации посылок - время обучения при модификации посылок и степень модификации базы знаний, позволяющие проводить сравнение различных реализаций модуля и оценивать степень использования существующей информации при модификации базы знаний.
Практическая ценность исследования состоит в следующих результатах:
разработаны структура и алгоритм функционирования модуля формирования знаний на основе абдуктивного метода модификации посылок;
выделены особенности построения и предложены алгоритмы функционирования интеллектуальных систем с модулем формирования знаний;
разработаны программные реализации методов добавления, удаления и модификации посылок;
разработана программная модель системы поддержки принятия решений с возможностью обучения при помощи модуля формирования знаний;
разработана программная модель системы обработки знаний для распознавания символов с возможностью обучения посредством модуля формирования знаний.
Внедрение результатов исследования. Полученные теоретические и практические результаты использованы в НИР, выполняемых в рамках гранта РФФИ проект № 06-01-00089-а по тематике «Адаптивные системы логического вывода», а также в учебном процессе Вятского государственного университета и Вятского государственного гуманитарного университета в рамках дисциплин «Теория логического вывода», «Системы искусственного интеллекта», «Основы искусственного интеллекта», «Базы знаний и экспертные системы», что подтверждается соответствующими актами о внедрении.
Апробация работы. Основные положения и результаты исследования докладывались и обсуждались на Всероссийской ежегодной научно-технической конференции ВятГУ «Наука-производство-технологии-экология», г. Киров (2004, 2005, 2006 гг.), на Всероссийской научно-практической конференции «Актуальные проблемы гуманитарных и экономических наук», г. Киров (2004 г.).
Публикации. По теме исследования опубликовано 9 работ, из них 5 статей, 4 тезисов докладов.
Структура и объем исследования. Диссертационная работа состоит из введения, четырех глав, заключения, библиографического списка (включающего 167 наименований) и списка сокращений. Основная часть работы изложена на 203 страницах и содержит 43 рисунка и 3 таблицы.
Формальная система исчисления высказываний
Рассмотрим ФС ИВ I [97]. Зададим её следующим образом. 1) Алфавит. Символами ИВ I являются: - символы высказываний (переменные) А, В, С,..., А], Вь Сь--.; - значения истинности (константы) 1 - истина (true) и 0 - ложь (false); - логические связки л (конъюнкция), v (дизъюнкция), -п (отрицание), ь- (импликация), (эквивалентность), = (знак логического вывода); - служебные символы «(» и «)». 2) Формулы. Формулы ИВ I строятся по следующим правилам: - любая переменная или константа есть формула; - если А и В - формулы, то каждое из выражений -А (А), АлВ, AvB, Ah- B, А+-+В есть формула; - других правил образования формул нет. 3) Аксиомы. В качестве аксиом используются следующие схемы формул (X, Y, Z - любые формулы): - Хн Х; - XAYH YAX; - (XVY)AZH XAZVYAZ. 4) Правила вывода. . . , X,XH Y - Modus ponens ; - Modus toilens =-1—; X - Правило переноса. а) В выражении рлХн- Y конъюнктивный сомножитель р может быть перенесен через знак «ь- ». При этом он инвертируется и дизъюнктивно складывается с формулой Y: PAXH Y= XI- YV р. б) В выражении Xf- Yvq дизъюнктивное слагаемое q может быть перенесено через знак «(-»». При этом оно инвертируется и конъ юнктивно умножается на формулу Y: Xh- Yvq= XA q h Y. - Правило разъединения-соединения. а) Для конъюнктивных сомножителей: XH- YAZ= XH- Y, Xh- Z. б) Для дизъюнктивных слагаемых: XVYH Z= XH Z, Yf- Z. Для упрощения записи формул введем некоторые соглашения. - Будем всегда опускать внешние скобки. - В целях сокращения числа внутренних скобок в формулах воспользуемся правилами силы операций. Перечислим введенные логические связки в порядке убывания их силы: —і, л, v, ь- , «- . - Если запись формулы не вызывает разночтений, то не будем указывать знак конъюнкции, записывая соединяемые им формулы рядом без интервала. Введем ряд определений. Переменную или её отрицание будем называть литералом. Формулу вида Xb Y назовем секвенцией. Причем X — тело, или антецедент секвенции, a Y - голова, или консеквент.
Аксиомы и правила вывода предложенного исчисления позволяют преобразовать любую формулу исчисления в секвенцию, в антецеденте которой содержится конъюнкция, а в консеквенте - дизъюнкция переменных.
Секвенцией-дизъюнктом называется секвенция, в теле которой находится константа «1», а голову составляет дизъюнкция литералов.
Доказательством в ФС ИВ I называется конечная последовательность секвенций, каждая из которых или является аксиомой исчисления, или получена из предыдущей секвенции по одному из правил вывода ФС. Заключительная секвенция такой последовательности называется доказуемой секвенцией, или теоремой. Формула X называется доказуемой в исчислении I, если доказуема секвенция 1н Х.
Выводом секвенции SN из множества Н секвенций в исчислении I называется последовательность секвенций Si, S2, ...Sj, ..., SN, В которой каждая секвенция Sj либо является аксиомой исчисления I, либо принадлежит множеству Н, либо получена из предыдущих секвенций по одному из правил вывода исчисления I.
При этом секвенции множества Н называется посылками (исходными посылками, исходными секвенциями), секвенция SH называется логическим следствием секвенций множества Н.
Схемой вывода логического следствия называется ориентированный граф, вершинами которого являются номера секвенций посылок, причем входящие дуги помечены переменными или константами из левых, а исходящие - из правых частей секвенций, и вершины соединены между собой (рис. 1.1).
Существует множество способов классификации методов ЛВ, например по форме представления данных, направленности, используемым логическим законам, принципам доказательств теорем и т. д. [97]. Для целей настоящего исследования представляется полезным следующий способ классификации методов ЛВ (см. рис. 1.2).
Все методы ЛВ делятся на два вида - достоверный и правдоподобный. Достоверный ЛВ - это ЛВ в традиционном понимании математической логики. В достоверном ЛВ применяются только такие правила вывода, которые позволяют из набора исходных истинных формул получить лишь истинные формулы-заключения [46]. К достоверному выводу относится дедуктивный логический вывод (ДЛВ), представленный множеством.методов. Самый распространенный на сегодняшний день - метод резолюции. Также можно назвать метод Эрбрана, различные виды методов вывода на графах, метод деления дизъюнктов (ДД) и т. д. [18, 97].
В разделе 1.1.4 будет рассмотрен один из методов достоверного ЛВ, применяемый в данной работе, а именно, метод ДД.
Термин «правдоподобное рассуждение» введен Д. Пойа [74]. В правдоподобном ЛВ используются такие правила вывода, которые позволяют из набора исходных истинных формул получить формулы, об истинности которых можно говорить лишь с некоторой долей уверенности.
Постановка задачи логического вывода
В разделе 1.1.3 была приведена классификация методов ЛВ (см. рис. 1.2). В соответствии с делением ЛВ на дедуктивный, индуктивный, вывод по аналогии и абдуктивный можно говорить о соответствующих типах задач ЛВ. Однако цели настоящего исследования диктуют необходимость рассмотрения другой классификации задач. Основой классификации является воздействие применяемого метода ЛВ на исходную информацию.
Предлагается разделить все задачи ЛВ в РІВ І на два вида - без изменения и с изменением исходной информации. Способами решения задач являются методы, приведенные нарис. 1.2.
1. Задачи логического вывода без изменения исходной информации Такие задачи решаются при помощи ДЛВ и вывода по аналогии. Приведем несколько типов таких задач. Пусть имеется множество исходных посылок и заключение. - Задача определения выводимости. Требуется определить, является ли заключение логическим следствием исходных посылок. - Задача поиска решения. Требуется найти хотя бы одно решение, т. е. хотя бы одно подмножество исходных посылок, логическим следствием которых является заключение. - Задача поиска всех решений. Требуется найти все решения, т. е. все такие подмножества исходных посылок, логическим следствием которых является заключение. - Задача определения степени достоверности. Имеются два аналогичных предположения. Требуется установить степень достоверности одного из предположений по степени достоверности другого.
2, Задачи логического вывода с изменением исходной информации Подобные задачи решаются на основе методов дедукции, индукции и абдукции. Изменять (т. е. добавлять и/или удалять) исходную информацию возможно двумя способами — изменяя исходные посылки и/или заключение. Поэтому задачи данного класса можно разделить на три типа: с изменением посылок, с изменением заключения, с изменением посылок и заключения. Приведем примеры задач каждого типа.
1) Задачи с изменением посылок. Имеется множество исходных посылок и заключение.
- Задача добавления посылок. Требуется определить выводимость заключения из исходных посылок. В случае неудачного окончания вывода найти такое множество посылок, при добавлении которого во множество исходных посылок заключение становится выводимым.
- Задача удаления посылок. Требуется определить выводимость заключения из исходных посылок. В случае удачного окончания вывода найти такое множество посылок, при исключении которого из множества исходных посылок заключение становится невыводимым.
- Задача модификации посылок. Данная задача является составной, так как включает в себя две предыдущие задачи, и формулируется следующим образом. Задано исходное множество посылок и множество выводимых заключений, состоящее из двух подмножеств - подмножества заключений, которые должны выводиться из посылок, и подмножества заключений, которые не должны выводиться из посылок. Требуется изменить исходное множество посылок таким образом, чтобы заключения из обоих подмножеств заключений удовлетворяли заданным условиям выводимости.
2) Задачи с изменением заключения. Имеется множество исходных по сылок и заключение.
- Задача изменения заключения для выводимости. Требуется опреде лить выводимость заключения из исходных посылок. В случае неудачного окончания вывода найти множество таких заключений, которые, во-первых, получены путем модификации исходного заключения, во-вторых, являются следствиями исходных посылок.
- Задача изменения заключения для невыводимости. Требуется опреде лить выводимость заключения из исходных посылок. В случае удачного окончания вывода найти множество таких заключений, которые, во-первых, получены путем модификации исходного заключения, во-вторых, не являют ся следствиями исходных посылок.
3) Задачи с изменением посылок и заключения. Имеется множество исходных посылок и заключение.
- Задача добавления посылок и изменения заключения для выводимости. Требуется определить выводимость заключения из исходных посылок. В случае неудачного окончания вывода найти множество М посылок и множество N заключений (полученных путем модификации исходного заключения). Причем при добавлении множества М во множество исходных посылок заключения множества N становятся логическими следствиями исходных посылок.
- Задача удаления посылок и изменения заключения для невыводимости. Требуется определить выводимость заключения из исходных посылок. В случае удачного окончания вывода найти множество М посылок и множество N заключений (полученных путем модификации исходного заключения). Причем при исключении множества М из множества исходных посылок заключения множества N перестают быть логическими следствиями исходных посылок.
Структура модуля формирования знаний
В главе 1 была рассмотрена обобщенная структура СОЗ (см. рис. 1.3), состоящая из четырех основных подсистем - ПСИИ, ПСЛВ, ПСПДЗ и ПСО. Отмечалось, что наличие развитой ПСО является одним из признаков действительно интеллектуальных систем.
Также в главе 1 рассматривались два типа реализации ПСО - на основе модуля приобретения знаний (автоматизированное пополнение БЗ с участием эксперта) и на основе модуля формирования знаний (автоматическое пополнение БЗ). Указывалось, что на сегодняшний день среди методов формирования знаний наиболее широко применяемыми являются методы ИЛВ. Однако отмечалось, что обучение на основе абдукции имеет ряд преимуществ перед другими методами обучения, таких как возможность использования небольшого числа наблюдений (начиная с одного), возможность максимального учета существующей в БЗ информации, возможность использования как положительных, так и отрицательных наблюдений, возможность наполнения первоначально пустой БЗ.
В настоящей работе предлагается новый вид модуля формирования знаний - на основе абдуктивного метода модификации посылок. Такие модули могут входить в состав СОЗ и придавать им возможность обучения новой информации за счет модификации посылок базы знаний. Также наличие подобного модуля позволяет СОЗ автоматически наполнять пустую базу знаний.
Принцип действия рассматриваемого модуля формирования знаний основан на абдуктивном методе модификации посылок. Модуль применяется в случае: - создания информации «с нуля» в ПСПДЗ; - модификации существующей информации в ПСПДЗ.
Модуль формирования знаний реализует автоматическую модификацию посылок базы знаний на основании некоторого множества заключений, поступающего от пользователя или внешней среды через ПСИИ. Модуль формирования знаний имеет структуру, показанную на рис. 3.1, синтезированную на основе метода модификации посылок, рассмотренного в главе 2.
На рис. 3.1 представлен модуль формирования знаний, входящий в ПСО, а также ПСПДЗ и ПСИИ. Модуль формирования знаний состоит из блоков, реализующих преобразования на базе следующих методов: - метода определения выводимости (блок классификации заключений и блок проверочного вывода); - метода добавления посылок (блок добавления посылок); - метода удаления посылок (блок удаления посылок). Для обеспечения совместной работы всех блоков и реализации алгоритма метода модификации посылок служит блок управления и контроля. Рассмотрим подробно каждый блок модуля.
Блок классификации заключений служит для разделения множества входных заключений на классы в соответствии с требованиями выводимости и реальной выводимостью заключений из множества исходных посылок.
Блок добавления посылок получает на вход множество исходных посылок (из базы знаний системы) и множество заключений из класса п/р (в этот класс входят заключения, которые на текущем шаге не выводятся, однако требуется, чтобы они выводились). На выход данного блока поступают семейства множеств (для каждого заключения - свое семейство) таких посылок, при добавлении которых во множество исходных посылок требования выводимости для данных заключений удовлетворяются.
На вход блока удаления посылок поступают множество исходных посылок и заключения, входящие в класс р/п (такие заключения, которые на текущем шаге выводятся, но требуется обеспечить их невыводимость из исходных посылок). Выходом блока являются семейства множеств посылок (для каждого заключения - свое семейство), при удалении которых из множества исходных посылок обеспечивается невыводимость соответствующих заключений.
Блок проверочного вывода I позволяет определить, имеются ли конфликты требований выводимости для классов п/р и п/п. Такие конфликты могут возникать, когда блок добавления посылок предлагает такое множество посылок, при объединении которого с множеством исходных посылок нарушаются требования выводимости заключений класса п/п.
Блок проверочного вывода II решает аналогичную задачу для классов р/п и р/р. В этом случае конфликты могут возникать, когда для обеспечения требований выводимости заключений класса р/п удаляются такие посылки, которые служили для выводимости заключений класса р/р.
Блок контроля служит для проверки на наличие во множестве заключений, разделенных на классы, заключений в классах р/п и п/р. Результат проверки возвращается в блок управления. Также данный блок служит для выявления ситуации зацикливания.
Блок управления предназначен для синхронизации работы всех блоков модуля формирования знаний и ПСПДЗ, управления потоками данных, реализации основного цикла метода модификации посылок. Ещё одна функция данного блока - разрешение ситуаций зацикливания посредством применения безусловной модификации через блок добавления или блок удаления посылок.
Таким образом, разработана структурная схема модуля формирования знаний, составляющего основу ПСО СОЗ. Также представлены структурные связи модуля с ПСИИ и ПСПДЗ. Схема синтезирована на основе метода модификации посылок. Особенностью схемы является наличие блоков добавления посылок, удаления посылок и классификации заключений, реализующих добавление посылок, удаление посылок и определение выводимости. Структурная схема модуля позволяет реализовать ПСО аппаратным, программным или аппаратно-программным способами.
Разработка программных реализаций методов с изменением посылок
Программа Addition of premises представляет собой программную реализацию метода добавления посылок в ИВ и предназначена для исследования данного метода.
Программа реализации метода добавления посылок состоит из пяти основных блоков - пользовательского интерфейса, преобразования посылок, реализации процедуры вывода, построения формулы дополнительных посылок, создания семейства множеств дополнительных посылок.
Блок пользовательского интерфейса выполняет следующие функции: - ввод пользователем исходных посылок и заключения с клавиатуры или из файла в виде секвенций; - вывод результата работы программы в текстовое поле и в файл. Результатом является семейство множеств дополнительных посылок, причем каждому семейству присваивается коэффициент глубины вывода. Также результатом работы программы может быть сообщение о том, что дополнительные посылки не требуются, так как заключение выводится из множества исходных посылок; - вывод протокола работы программы в специальное текстовое поле. В протокол заносится время начала и окончания текущего сеанса работы, индексы выполненных процедур, полученные остатки и их произведение, вычисленные дополнения, части формулы дополнительных посылок, признаки решения и окончания вывода; - сохранение протокола работы в текстовый файл.
Блок преобразования посылок получает на вход множество исходных посылок в виде секвенций и секвенцию-заключение, а на выходе выдает множество исходных посылок в виде дизъюнктов и дизъюнкт-заключение. Преобразование осуществляется с помощью правила переноса. Исходные посылки и заключение как в виде секвенций, так и в виде дизъюнктов хранятся в программе в массивах строк.
Блок реализации процедуры вывода осуществляет выполнение процедуры вывода W и операции ДД. На вход данного блока поступают множество М дизъюнктов исходных секвенций и дизъюнкт-заключение d. В результате операции ДД формируются остатки исходных дизъюнктов . Остатки перемножаются, и полученное произведение с помощью правила разъединения-соединения преобразуется во множество секвенций, которые в свою очередь образуют новые выводимые дизъюнкты-заключения. Так же формируется новое множество Mi исходных дизъюнктов, и с помощью операции группового деления дизъюнктов вычисляется дополнение д. Таким образом, на выходе рассматриваемого блока получаются множество m новых дизъюнктов-заключений, множество Mi новых исходных дизъюнктов, дизъюнкт-дополнение д, а также признаки решения q и окончания вывода р.
Блок построения формулы дополнительных посылок требуется для создания формулы, из которой после окончания процесса вывода получается семейство множеств дополнительных посылок. Входом для данного блока являются дизъюнкт-дополнение д и признаки решения q и окончания вывода р, полученные в результате выполнения процедуры вывода W. В рассматриваемом блоке реализуются функции вычисления общих признаков решения Qh, окончания вывода Рь и коэффициента глубины вывода к, а также следующие операции над семействами множеств: - операция произведения семейств множеств, обозначаемая символом - операция дизъюнктивного сложения семейства множеств дизъюнктов и отдельного дизъюнкта, обозначаемая символом « v »; - операция конъюнктивного умножения семейства множеств дизъюнктов и логической переменной, обозначаемая символом «л».
Блоки реализации процедуры вывода и построения формулы дополнительных посылок работают совместно и выполняют многократные преобразования. На каждом шаге блок реализации процедуры вывода применяет W-процедуру к имеющимся множествам исходных дизъюнктов и дизъюнктов-заключений, образуя новые выводимые и исходные дизъюнкты, используемые на следующем шаге. Результаты работы этого блока поступают на вход блока построения формулы дополнительных посылок, в котором строится формула семейства множеств дополнительных посылок О на случай неуспешного окончания вывода. Процесс вывода заканчивается, когда для каждого выводимого на очередном шаге дизъюнкта или будет получено решение (q=0), или будет установлено, что продолжение вывода невозможно (р=1).
Причем вывод завершается успешно, если для всех выводимых на последнем шаге дизъюнктов были получены решения (q=0).
На выходе блока построения формулы после окончания процесса вывода получается формула дополнительных посылок (хранящаяся в виде строки).
Блок создания семейства множеств дополнительных посылок начинает свою работу после окончания процесса вывода. На вход этого блока приходит формула семейства множеств дополнительных посылок Q, которую требуется преобразовать в несколько отдельных множеств. В случае неудачного окончания вывода выходом данного блока является семейство множеств дополнительных посылок Л, причем ранее не выводимое заключение становится выводимым из объединения любого из этих множеств с множеством исходных посылок. Каждое из множеств, входящих в Л, проходит проверку на противоречивость с множеством исходных посылок. Кроме того, каждому множеству из Л присваивается коэффициент глубины вывода.
Результирующее семейство множеств дополнительных посылок Л в случае неудачного окончания вывода передается для вывода в блок пользовательского интерфейса. При успешном окончании вывода пользователю выдается соответствующее сообщение.
