Формально-грамматическая модель логического вывода в системах искусственного интеллекта

• Автор: Анисимова, Ирина Николаевна
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Санкт-Петербург
• Количество страниц: 143 с.

ОГЛАВЛЕНИЕ
ВВЕДЕНИЕ
ЛОГИЧЕСКИЙ ВЫВОД И МЕТОДЫ ПОВЫШЕНИЯ ЕГО ЭФФЕКТИВНОСТИ В
СИСТЕМАХ ИИ (ОБЗОР)
Глава 1. МЕТОД ПОСТРОЕНИЯ ЛОГИЧЕСКОГО ВЫВОДА В ИВ, ОПИРАЮЩИЙСЯ НА ФОРМАЛЬНО-ГРАММАТИЧЕСКУЮ МОДЕЛЬ
1.1. Хорновские дизъюнкты ИВ и КС-грамматики
1.2. Моделирование множества гипотез ИВ КС-грамматикой
1.3. Построение логической шкалы и проверка выводимости целей
1.4. Алгоритм предварительной настройки для построения логических выводов
1.5. Построение опровержений в множествах дизъюнктов
ИВ методом с предварительной настройкой
1.6. Особенности построения опровержений в рекурсивном случае
1.7. Основные результаты и выводы главы
Глава 2. МЕТОД ПОСТРОЕНИЯ ЛОГИЧЕСКОГО ВЫВОДА В ИП, ИСПОЛЬЗУЮЩИЙ ПРОПОЗИЦИОНАЛЬНУЮ М-АБСТРАКЦИЮ
2.1. Пропозициональные абстракция и m-абстракция
2.2. Использование пропозициональной m-абстракции для обобщения метода логического вывода на ИП
2.3. Процедура параллельного построения схем и выводов
в исходном множестве гипотез
2.4. Свойства метода логического вывода в ИП
2.5. Основные результаты и выводы главы

Глава 3. МЕТОД С ПРЕДВАРИТЕЛЬНОЙ НАСТРОЙКОЙ ДЛЯ ИП, ИСПОЛЬЗУЮЩИЙ АБСТРАКЦИОННОЕ ОТОБРАЖЕНИЕ С РАСШИРЕННЫМИ ВЫСКАЗЫВАНИЯМИ
3.1. Абстракционное отображение и множества дизъюнктов
с расширенными высказываниями
3.2. Формально-грамматическая модель логического вывода в множествах дизъюнктов с расширенными высказываниями
3.3. Процедура параллельного построения схем в множестве дизъюнктов с расширенными высказываниями и выводов в ИП
3. 4. Использование комбинации абстракционных отображений
3. 5. Выбор ведущих аргументов для абстракции с удалением аргументов
3.6. Основные результаты и выводы главы
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
ПРИЛОЖЕНИЕ

ВВЕДЕНИЕ

В последнее время наблюдается тенденция к интеллектуализации инструментальных программных средств научных исследований, использованию экспертных систем, систем, основанных на знаниях, применению механизмов и методов искусственного интеллекта (ИИ). Одним из фундаментальных направлений в этой области является автоматическое доказательство теорем [34,51,54,80,87,128], опирающееся на логическую форму представления знаний и революционные методы в качестве механизма логического вывода. Эти методы имеют практическую реализацию в логическом программировании, в частности, в декларативном языке Пролог.
Бойером с соавторами [893 предложено дизъюнктивное представление для всех аксиом теории множеств вместе с основными определениями, относящимися к этой теории. Полученные дизъюнкты непосредственно применимы в методах доказательства теорем, основанных на резолюции. Многочисленные работы [93-96,141] посвящены переформулировке на логический язык элементарных геометрий и, в частности, представлению евклидовой геометрии языком хор-новских дизъюнктов. Это делает возможным применение логического программирования для автоматического доказательства теорем геометрии.
Несмотря на определенное разочарование, связанное с выдвинутым в восьмидесятых годах японским проектом создания ЭВМ пятого поколения, архитектура которой должна была базироваться на применении механизмов Пролога в качестве внутреннего машинного языка [49,65, 66,86], и критику универсальности Пролога как инструментального средства (ИС) доказательства теорем, для решения целого ряда задач логические методы сохраняют свое важное зна-

дальнейшего рассмотрения. Если соответствующий нетерминал Aq не был до этого включен в множество укорачивающих символов, то он туда включается. Логическая переменная flag обеспечивает окончание работы алгоритма, когда ни один новый символ не был признан укорачивающим, то есть на шаге t+1, удовлетворяющем условию Wt+1=Wt. На этом же шаге заканчивается и формирование списков S(Aq). Покажем, что уже на следующем t+2-м шаге не произойдет пополнения СПИСКОВ S(Aq), ТО есть St + 2(A)=St+1 (А) для любого символа A€Vn.
Лемма 1.1. Пусть на t+1-м шаге алгоритма предварительной настройки получено Wt+1=Wt. Тогда St+2(A)=St+1 (А) для любого AEVn.
Доказывая лемму от противного, предположим, что найдется такое правило Р-, =(А -» А-.АеР, что P-St + iA) и Р3 GSt+ 2 (А). При просмотре правил вывода на t+1-м шаге Pi не попало в список St+1(А). Следовательно, найдется такой нетерминал Аг, 1<г<п, из правой части Р3, что Ar£Wt. В то же время на основании сделанного предположения можно утверждать, что Ar£Wt+i. Следовательно, что противоречит нашему утверждению.
Оценим сложность предложенного алгоритма предварительной настройки. Рассмотрим крайний случай, когда все символы грамматики являются укорачивающими, и на каждом шаге в множество укорачивающих нетерминалов заносится лишь один символ. В этом случае число шагов t равно К - числу различных нетерминальных символов грамматики. А поскольку, как было показано, формирование списков правил закончится на t+1 шаге, необходимом также для проверки условия выхода Wt+i=Wt, общее число шагов алгоритма не превысит К+1, K