Применение автоматического доказательства теорем в системах, основанных на знаниях




Скачать 25.54 Kb.
Дата02.08.2016
Размер25.54 Kb.
Я. О. ДУНАЕВА

Байкальский институт бизнеса и международного менеджмента ИГУ

ПРИМЕНЕНИЕ АВТОМАТИЧЕСКОГО ДОКАЗАТЕЛЬСТВА ТЕОРЕМ В СИСТЕМАХ, ОСНОВАННЫХ НА ЗНАНИЯХ

Автоматическое доказательство теорем (automatic theorem proving) представляет собой один из механизмов рассуж­дений в системах, основанных на знаниях. Программы ав­томатического доказательства теорем, так называемые пруверы (от англ. provers), используют обычно метод резолю­ции или другие полные процедуры вывода, ориентиро­ванные на опровержение (если получено опровержение ут­верждения, то его отрицание истинно). Первоначально этот механизм успешно использовался в чистом виде, т.е. для доказательства лемм и теорем в математике. Позже пруверы стали применять при решении разного рода проблем, связанных с верификацией и синтезом аппаратного и про­граммного обеспечения ЭВМ.

Идея использования прувера в качестве помощника человека-исследователя - для выполнения логических рас­суждений - значительно расширяет сферу применения ме­тодов автоматического доказательства теорем. Например, можно использовать пруверы для проверки правильности гипотез в обучающих системах при демонстрации приме­ров, требующих рассуждений, и при проверке ответов обу­чаемого, а также в диагностических системах (медицинс­ких, технических, экономических).

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

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

В предлагаемой схеме прувер "подключается" на вто­ром этапе, когда требуется проверить гипотезу, т.е. логи­чески вывести опровержение отрицания гипотезы, осно­вываясь на знаниях о предметной области. Таким образом, на вход пруверу подается совокупность KBН, где KB — описание предметной области, а Н — гипотеза (диагноз или ответ на вопрос).

При описываемом подходе для диагностической систе­мы возникают две интересные задачи — автоматическое порождение гипотезы Н и отсечение "лишних" знаний из KB, не нужных для проверки выдвинутой гипотезы (оценка релевантности знаний). Последняя задача актуальна и в случае, когда гипотезу выдвигает обучаемый в разделе те­стирования обучающей системы.

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

Предлагаемый подход к созданию основанных на знаниях систем вполне возможно применить при создании; электронных учебников или обучающих серверов. |
Литература

1. Russel S. J., Norvig P. Artificial Intelligence: A Modern Approach, 1995.

2. А. Тейз, П. Грибомон, Ж. Луи и др. Логический под­ход к искусственному интеллекту. Пер. с франц. М Мир, 1990.

3. С. Осута. Обработка знаний. Перс япон. М. Мир, 1989.



4. P. Lucas. Symbolic diagnosis and its formalization. The Knowledge Engineering Review, vol. 12:2, 1997, p. 109-146.


База данных защищена авторским правом ©uverenniy.ru 2016
обратиться к администрации

    Главная страница