Software & Systems

Одним из многообещающих направлений в программных системах являются системы искусственного интеллекта, предполагающие моделирование интеллектуальных функций человека. Можно выделить два основных подхода к моделированию поведения естественного интеллекта. Первый из них заключается в моделировании работы отдельных элементов структуры человеческого мозга. Второй подход предполагает моделирование интеллектуальных функций мозга: систему понятий, построение рассуждений и другие. При этом наиболее часто сейчас используется моделирование рассуждений человека, поскольку оно имитирует высокоуровневые мыслительные процессы по определенным правилам (например, по правилам логики) и позволяет достаточно просто описывать исходные данные и интерпретировать результат, а также отслеживать ход моделирования.

Моделирование рассуждений средствами логики осуществляется посредством логического вывода (ЛВ). В качестве исходных данных для ЛВ служат формулы посылок и заключения. Посылки представляют собой набор фактов и правил вывода и составляют в совокупности базу знаний. Заключение записывается в виде формулы логики и поступает извне в систему ЛВ. Процедуры ЛВ обрабатывают заключение и исходные посылки, и результатом работы может стать сообщение о корректности заключения или модификация исходных посылок.

Обычно выделяют следующие основные виды ЛВ: дедуктивный, абдуктивный и индуктивный. Дедуктивный вывод позволяет ответить на вопрос, является ли заключение следствием исходных посылок. Абдуктивный вывод дедуктивно невыводимого заключения позволяет пополнить набор исходных посылок фактами так, чтобы заключение стало следствием базы знаний. Индуктивный вывод, в отличие от абдуктивного, позволяет пополнить набор исходных посылок общими правилами.

Данные виды вывода известны достаточно давно и могут применяться для решения определенных задач. Однако существует класс задач, решить которые применением указанных видов вывода невозможно или затруднительно. Этот класс задач предполагает наличие корректной и полной базы знаний для некоторой предметной области и недостоверное заключение, требующее преобразования. Следовательно, появляется принципиально новая постановка задачи ЛВ: модифицировать исходно невыводимое заключение с целью сделать его следствием исходных посылок. Задача решается посредством применения ЛВ модифицируемых заключений, который предполагает выполнение над невыводимым заключением последовательно трех действий: расширения формулы заключения добавлением литералов к его дизъюнктам, минимизации формулы заключения путем исключения части литералов, не требуемых для вывода заключения, и оценки вариантов модификации дизъюнктов заключения с целью отбора оптимальных дизъюнктов.

Структура системы ЛВ

В системах обработки знаний ЛВ выполняется специальным компонентом – машиной ЛВ (МЛВ). От эффективности работы МЛВ в значительной степени зависит эффективность работы построенной на ее основе системы обработки знаний. В качестве одного из требований к высокопроизводительным программным реализациям МЛВ необходимо указывать возможность распараллеливания процесса вывода. Для реализации данного требования МЛВ в своей работе должна использовать параллельные методы ЛВ, например, вывод делением дизъюнктов (см.: Страбыкин Д.А. Логический вывод в системах обработки знаний. СПб: Изд-во СПбГЭТУ,1998 и Страбыкин Д.А., Томчук М.Н. Логический вывод с модификацией заключения в исчислении высказываний. // Сб. науч. тр. Киров: Вятский научный центр, 2003).

Кроме МЛВ, система ЛВ должна также включать подсистему хранения данных и знаний, подсистему заключений и интерфейс. Структура системы ЛВ приведена на рисунке.

Опишем назначения блоков системы ЛВ.

Блоки интерфейса

Блок классификации входной информации воспринимает входную информацию от внешней программы, и, в зависимости от ее вида, направляет в соответствующий блок модуля вывода.

Блок построения интерпретации: на основании описания смыслового значения предикатных и предметных констант, содержащегося в базе знаний, строит простые конструкции на языке высокого уровня, соответствующие смыслу формулы заключения или базы знаний, и выдает внешней программе.

Блоки подсистемы хранения данных и знаний

Базы данных и знаний хранят данные и знания в определенной форме: для уровня 1 в виде произвольных логических формул, для уровня 2 в виде дизъюнктов (так как методы вывода делением дизъюнктов требуют представления исходных посылок в виде множества дизъюнктов). Могут использоваться базы данных и знаний внешней программы. В этом случае необходима предварительная настройка с указанием их местоположения.

Блок преобразования формул выполняет преобразование произвольных выражений логики предикатов первого порядка или логики высказываний во множества дизъюнктов, используя законы логики и сколемовское преобразование.

Блок преобразования дизъюнктов выполняет обратное преобразование: преобразует дизъюнкт в секвенцию. В простейшем случае преобразование заключается в переносе литералов с инверсией через знак секвенции в левую ее часть. В более сложном случае может потребоваться анализ и объединение нескольких дизъюнктов.

Блок управления синхронизацией отслеживает изменения в базах обоих уровней. При изменениях в базах уровня 1 выполняет повторные преобразования формул и заменяет соответствующие дизъюнкты в базах уровня 2. При изменении в базах уровня 2 корректирует состояние баз уровня 1.

Блоки подсистемы заключений

Исходное заключение 1: содержит формулу (формулы) исходного заключения, полученного от внешней программы.

Исходное заключение 2: содержит множество дизъюнктов, в которое с использованием блока преобразования формул из подсистемы хранения данных и знаний преобразуется исходное заключение 1.

Модифицированное заключение 1: содержит множество вариантов модифицированного заключения, представленное в виде набора множеств дизъюнктов.

Модифицированное заключение 2: содержит множество вариантов модифицированного заключения, представленное в виде набора секвенций, получаемых преобразованием дизъюнктов модифицированного заключения 1 с помощью блока преобразования дизъюнктов из подсистемы хранения данных и знаний.

Блоки МЛВ

Блок общих операций включает в свой состав процедуры, используемые другими блоками. К ним относятся процедуры: частичного деления дизъюнктов, полного деления дизъюнктов, построения матриц «производных», унификации литералов.

Блок расширения реализует метод специального параллельного абдуктивного вывода делением дизъюнктов, в результате которого формируются множества дополнительных литералов для невыводимых дизъюнктов заключения.

Блок минимизации выполняет минимизацию полученных вариантов модифицированных дизъюнктов, исключая часть литералов.

Блок дедуктивного вывода необходим для выполнения проверочного дедуктивного вывода при минимизации заключения, а также содержит процедуры, используемые блоком расширения. Представляет собой реализацию метода обобщенного параллельного дедуктивного вывода делением дизъюнктов.

Блок согласования решений содержит функции согласования значений общих переменных и решений и используется блоками расширения и дедуктивного вывода.

Блок фильтрации: в соответствии с выбранным критерием оптимальности отсекает часть вариантов модифицированного заключения. Для определения класса дизъюнкта использует функции блока оценки.

Блок оценки содержит набор функций оценки для формирования множества оценок вариантов модификации заключения.

Блок управления процессами МЛВ управляет временем и способом запуска отдельных функций МЛВ. Объединяет функции в процессы, управляет запуском процессов и передачей параметров и результатов.

Общие блоки

Блок управления обеспечивает прием команд от внешней программы через интерфейс и управление работой подсистем.

Блок состояния и статистики хранит состояние выполнения операций ЛВ и отдельных подсистем, а также статистические сведения, позволяющие оценить эффективность вывода. По требованию внешней программы выдает необходимую информацию через интерфейс.

Работа системы

Для выполнения ЛВ модифицируемых заключений систему ЛВ следует подготовить: должно быть настроено расположение баз знаний, при необходимости должно быть выполнено преобразование исходных формул во множество дизъюнктов, а также должна быть указана функция оценки для блока фильтрации.

Для начала работы системе передается сформированное внешней программой исходное заключение. Это заключение подвергается преобразованию во множество дизъюнктов, после чего поступает в МЛВ. Там производится ЛВ делением дизъюнктов с расширением формулы заключения. Если в процессе вывода устанавливается, что исходное заключение выводимо из исходных посылок, вывод завершается, так как модификации заключения не требуется. В противном случае полученные варианты расширенного заключения подвергаются минимизации. Сформированные в результате минимизации дизъюнкты поступают в блок фильтрации, где производится оценка и отбор вариантов модификации заключения. Варианты модифицированного заключения передаются из МЛВ в блок заключений, при необходимости подвергаются преобразованию и выдаются внешней программе.

В качестве областей применения системы ЛВ модифицируемых заключений можно выделить следующие.

Системы автоматического регулирования. Состояние объекта управления в такой системе описывается логической формулой заключения, а допустимый диапазон состояний задается в виде формул исходных посылок. Если состояние объекта выходит за допустимые пределы, производится модификация заключения для возвращения объекта в допустимое состояние.

Системы корректирующего обучения. База исходных посылок содержит знания из некоторой предметной области. Обучаемый вводит утверждение, которое проверяется на истинность (выводимость из исходных посылок), и, если оно неверно, производится его коррекция.

Грамматический разбор предложений. Система ЛВ модифицируемых заключений может быть использована для восстановления предложения и построения новых предложений.

Вычислительные комплексы с динамической архитектурой. Система ЛВ модифицируемых заключений может применяться для диспетчеризации вычислительных процессов в системах с динамически изменяющимися составом и связями вычислительных средств.

Экспертные системы. Если начальное заключение пользователя неполно или неверно, ЛВ модифицируемых заключений позволяет уточнить (откорректировать) заключение, а в некоторых случаях указать на необходимость исследования дополнительных признаков.