Введение к работе
Актуальность темы исследования. Одним из многообещающих направлений в вычислительных системах" сегодня являются системы обработки знаний (СОЗ), моделирующие поведение естественного интеллекта Они имеют широкое распространение, а в перспективе смогут применяться практически повсеместно, повышая интеллектуальный уровень вычислительных систем Однако, несмотря на имеющиеся успехи, современные СОЗ имеют ряд недостатков В частности, они не способны решать задачи, требующие наличия достоверного заключения при имеющемся недостоверном Кроме того, современные СОЗ работают неэффективно на параллельных платформах
Можно выделить два основных подхода к моделированию поведения естественного интеллекта Первый из них заключается в моделировании работы структуры мозга Его характерным недостатком является сложность (часто -невозможность) построения семантической картины хода рассуждений Второй подход предполагает моделирование интеллектуальных функций мозга систему понятий, построение рассуждений и другие При этом наиболее часто сейчас используется моделирование рассуждений человека, поскольку имитирует высокоуровневые мыслительные процессы по определенным правилам (например, по правилам логики) и позволяет достаточно просто описывать исходные данные и интерпретировать результат, а также отслеживать ход моделирования
Моделирование рассуждений средствами логики осуществляется при помощи логического вывода (ЛВ) Исходными данными для логического вывода служат формулы посылок и заключения Посылки представляют собой набор фактов и правил вывода и составляют базу знаний (БЗ) Заключение записывается в виде формулы логики и поступает извне в систему ЛВ
Обычно выделяют следующие основные виды логического вывода дедуктивный, абдуктивный и индуктивный Дедуктивный вывод позволяет ответить на вопрос о выводимости заключения Абдуктивный вывод невыводимого заключения позволяет пополнить набор исходных посылок фактами так, чтобы заключение стало следствием БЗ Индуктивный вывод, в отличие от абдуктив-ного, позволяет пополнить набор исходных посылок общими правилами
Данные виды вывода известны достаточно давно и могут применяться для решения широкого круга задач Однако существует класс задач, решить которые применением указанных видов вывода невозможно или затруднительно Данный класс задач предполагает наличие корректной и полной БЗ для некоторой предметной области и недостоверное заключение, требующее преобразования Следовательно, появляется принципиально новая постановка задачи ЛВ модифицировать исходно невыводимое заключение с целью сделать его следствием исходных посылок Данная задача решается посредством применения нового вида ЛВ - логического вывода модифицируемых заключений
В качестве областей применения данного вида вывода можно отметить следующие системы автоматического регулирования, системы корректирующего обучения, грамматический разбор предложений, управление процессами в вычислительных комплексах с динамической архитектурой, экспертные системы, интеллектуальные поисковые машины
В качестве математического аппарата в логике наиболее часто применяются исчисление высказываний и исчисление предикатов первого порядка Первое предоставляет более простые средства; решение при этом производится более просто и быстро, однако ввиду ограничения выразительных способностей исчисления высказываний класс решаемых задач довольно узок Исчисление предикатов первого порядка обладает большими выразительными возможностями, однако средства и методы вывода в исчислении предикатов значительно сложнее. В настоящее время актуальным остается использование как исчисления предикатов первого порядка, так и исчисления высказываний
Одной из тенденций, наблюдаемых в современных ЭВМ (в том числе ПЭВМ), является увеличение количества процессорных элементов (ядер) при относительно небольшом росте производительности каждого ядра Многие методы, использующие последовательный принцип решения задач, не позволяют использовать большую часть вычислительной мощности ЭВМ Возникает необходимость разработки параллельных алгоритмов решения задач
Таким образом, является актуальной задача разработки метода и системы параллельного логического вывода модифицируемых заключений на знаниях, представленных в виде формул исчисления высказываний и исчисления предикатов первого порядка, что позволит расширить класс задач, решаемых СОЗ, построенных на основе системы ЛВ, и повысить скорость их работы
Диссертационные исследования выполнялись в рамках НИР «Теория и применение логического вывода с модификацией заключений» (грант Министерства Образования РФ Е02-2 0-93), а также в рамках НИР «Разработка среды декларативного логического программирования для кластерной вычислительной системы» (ВятГУ, НИР №412)
Область исследований связана с СОЗ, основанными на логике исчисления высказываний или исчисления предикатов первого порядка и использующими логический вывод модифицируемых заключений
Предметом исследований являются методы и средства логического вывода модифицируемых заключений, а также СОЗ различного назначения, использующие представление знаний в виде логических формул и основанные на логическом выводе модифицируемых заключений
Целью исследования является разработка параллельного метода логического вывода модифицируемых заключения для исчисления высказываний и исчисления предикатов первого порядка и построение на его основе машины и системы ЛВ модифицируемых заключений Для достижения цели необходимо решить следующие задачи
-
Разработать параллельный метод логического вывода модифицируемых заключений для исчисления высказываний и исчисления предикатов первого порядка, позволяющий модифицировать невыводимое заключение и сделать его следствием исходных посылок
-
Разработать структуру и алгоритм работы машины параллельного логического вывода модифицируемых заключений
-
Разработать систему логического вывода на основе МЛВ модифицируемых заключений
4 Разработать критерии эффективности работы машины и системы логического вывода модифицируемых заключений
Методы исследования."ДО5!чдЪётиЖейияЕ вставленной в работе цели использовались методы системного анализа и синтеза, теории множеств, теории графов, математической логики, теории логического и объектно-ориентированного программирования
На научную новизну претендуют
-
Метод параллельного логического вывода модифицируемых заключений для логики высказываний и логики предикатов первого порядка, отличающийся от известных методов тем, что к полученным в результате абдуктивного вывода дополнительным посылкам применяются специальная процедура преобразования, позволяющая построить из них дополнения дизъюнктов заключения, метод минимизации заключения, а также параллельный алгоритм оценки вариантов модификации заключения, что позволяет преобразовать невыводимое заключение с целью сделать его следствием исходных посылок
-
Метод минимизации заключения для исчисления высказываний и исчисления предикатов первого порядка, отличающийся от известных методов вывода тем, что для поиска решений использует параллельный поиск по дереву решений с отсечением части ветвей, что позволяет производить удаление из дизъюнктов заключения литералов, не участвующих в процессе вывода
-
Параллельный алгоритм оценки и отбора вариантов модификации дизъюнктов заключения, отличающийся от известных алгоритмов тем, что каждому дизъюнкту ставится в соответствие некоторое числовое значение, полученное применением к дизъюнкту специальной функции оценки, что позволяет из всего множества вариантов модификации исходных дизъюнктов выбрать наилучшие в соответствие с выбранным критерием
-
Критерии оценки эффективности работы машины и системы логического вывода модифицируемых заключений, учитывающие особенности логического вывода делением дизъюнктов, выбранную степень параллелизма, архитектуру вычислительной машины, виды модификации заключения, что позволяет оценить время, затрачиваемое на ЛВ и степень модификации заключения
Практическая ценность исследования состоит в следующем
-
Разработана структура машины логического вывода модифицируемых заключений В отличие от существующих, разработанная МЛВ позволяет распараллелить процесс вывода вплоть до уровня операций унификации литералов, что повышает скорость логического вывода на параллельных вычислительных платформах Кроме того, МЛВ способна выполнять три вида вывода дедуктивный, абдуктивный и вывод модифицируемых заключений
-
Разработана система логического вывода модифицируемых заключений, отличительными особенностями которой являются применение параллельных методов и машины ЛВ, использование двухуровневой базы знаний, наличие блока интерпретации формул, что позволяет строить на основе системы логического вывода высокопроизводительные СОЗ различного назначения
-
Разработаны рекомендации по применению машины и системы логического вывода модифицируемых заключений для интеллектуального управле-
ния вычислительными процессами, в интеллектуальных обучающих системах, в экспертных системах
4 Разработана учебная система логического вывода, отличительными чертами которой являются: реализация нескольких видов логического вывода делением дизъюнктов для исчисления высказываний, в том числе логического вывода модифицируемых заключений, наличие механизма преобразования формул во множество дизъюнктов, интерпретация формул на естественном языке, подробный отчет о ходе вывода Особенности системы позволяют применять ее для изучения видов и методов логического вывода
Внедрение результатов исследования. Полученные теоретические и практические результаты использованы в НИР «Теория и применение логического вывода с модификацией заключений» (грант Министерства Образования РФ Е02-2 0-93), в НИР «Разработка среды декларативного логического программирования для кластерной вычислительной системы» (ВятГУ, НИР №412), а также в учебном процессе в Вятском государственном гуманитарном и Вятском государственном университетах
Апробация работы. Основные положения и результаты исследования докладывались и обсуждались на 5-й международной конференции «Interactive Systems The Problems of Human-Computer Interaction», Ульяновск, 2003, 9-й «Национальной конференции по Искусственному Интеллекту КИИ-2004», Тверь, 2004, Всероссийской ежегодной научно-технической конференции ВятГУ «Наука-производство-технологии-экология», г Киров (2004, 2007 гг)
Публикации. Результаты исследования представлены в 10 работах, из них 5 статей, 4 тезисов докладов
Структура и объем работы. Диссертационная работа состоит из введения, четырех глав, заключения, списка сокращений и библиографического списка (включающего 150 наименований) Основная часть работы изложена на 166 страницах и содержит 33 рисунка и 6 таблиц
