- •Введение
- •Глава 1. Ведение в системы искусственного интеллекта
- •1.1. Архитектура систем искусственного интеллекта
- •1.2. База знаний и данных
- •1.1.1 Понятие модели
- •1.1.2. Логические модели
- •1.1.3 Модели знаний на основе продукций
- •1.1.4 Фреймовая модель знаний
- •1.1.5 Семантические сети
- •1.3. Машина вывода
- •1.3.1. Понятие формальной системы
- •Примеры стратегии вывода
- •Как функционирует машина вывода
- •1.4. Извлечение знаний и обучение
- •1.4.1. Извлечение знаний от многих экспертов
- •1.4.2 Проблема непротиворечивости формализованной базы знаний
- •1.5. Обучение системы
- •1.6. Интерфейс с пользователем
- •1.7. Организация работы
- •1.8. Инструментальные средства создания систем искусственного интеллекта
- •Языки программирования
- •1.8.2. Языки продукционного программирования
- •1. 8. 3. Языки инженерии знаний и инструментальные системы
- •1.8.3.1. Система vpExpert
- •1.8.3.2. Система kas
- •1.8.3.3. Система Expert-Ease
- •Глава 2. База знаний
- •2.1. Методы извлечения знаний
- •2.1.1. Классификация методов извлечения знаний
- •2.1.2. Пассивные методы
- •2.1.2.1. Наблюдения
- •2.1.2.2. Анализ протоколов «мыслей вслух»
- •2.1.2.3. Лекции
- •2.1.3. Активные индивидуальные методы
- •2.1.3.1. Анкетирование
- •2.1.3.2. Интервью
- •2.1.3.3. Свободный диалог
- •2.1.4. Активные групповые методы
- •2.1.4.1. «Круглый стол»
- •2.1.4.2. «Мозговой штурм»
- •2.1.4.3. Экспертные игры
- •2.1.4.3.1. Игры с экспертом
- •2.1.4.3.2. Ролевые игры в группе
- •2.1.4.4. Игры с тренажерами
- •2.1.4.4.1. Компьютерные экспертные игры
- •2.1.5. Текстологические методы
- •2.2.Формальное описание понятий предметной области (по)
- •2.2.1. Методы абстрагирования понятий
- •2.2.1.1.Агрегация и декомпозиция понятий
- •2.2.1.2.Обобщение и специализация понятий
- •2.2.1.3.Типизация и конкретизация понятий
- •2.2.1.4.Ассоциация и индивидуализация понятий
- •2.3.Методы классификации
- •2.3.1. Экстенсиональный и интенсиональный аспекты классификации
- •2.3.2. Таксономия и мерономия
- •2.3.3. Типы классификаций
- •2.3.4. Древовидные классификации
- •2.3.5. Булевы классификации
- •2.3.6. Комбинативные классификации
- •2.4.События и процессы
- •2.4.1. Состояния предметной области
- •2.4.2. Событие
- •2.4.3. Последовательные процессы
- •2.4.4. Рекурсивные процессы
- •2.4.5. Ветвящиеся процессы
- •2.5. Системы продукций: структура, технология, применение
- •2.5.1. Неформальное введение в системы продукций
- •2.5.1.1 Алгоритмические модели
- •2.5.2 Логический вывод
- •2.5.3 Прикладные модели
- •2.5.4. Метамодель систем продукций
- •2.5.4.1. Основные подсистемы
- •2.5.5.2. Метаструктура базы данных и операций
- •2.5.5.2.1. Характер организации данных
- •2.5.5.2.2 Операции над базой данных
- •2.5.5.2.3 Контроль несовместимости
- •2.5.5.2.4 Ассоциативная надстройка
- •2.5.6. Метаструктура модуля правил
- •2.5.6.1 Аппарат активации
- •2.5.6.2 Структура правил
- •2.5.7. Метаструктура модуля управления
- •2.5.8. Технология поддержки разработок продукционных систем
- •2.5.9. Формальные модели систем продукций
- •2.5.9.1. Алгебраическая модель
- •2.5.9.1.1. Основные определения
- •2.5.9.1.2. Операции преобразования ситуации
- •2.5.9.1.3. Условия корректности вычислений над конъюнктивной базой данных
- •2.5.9.1.4. Однозначность вычислений над дизъюнктивной базой
- •2.5.9.2. Управление выводом в системах продукций
- •2.5.9.3. Язык управления применением продукций
- •2.5.9.4. Язык управления выбором данных
- •2.5.9.5. Обзор формальных моделей вычислений
- •2.5.10. Экспериментальные системы продукций
- •2.5.10.1. Система скип
- •2.5.10.2. Система анализа топологических чертежей интегральных схем
- •P(слой) x0, y0 : Dx1, Dy2, .., Dxn-1, Dyn;
- •2.6. Выводы к второй главе
- •3. Машина логического вывода
- •3.1. Формальное определение задачи
- •3.2. Специфика решения задач в сии
- •3.3. Управление процессом решения задачи
- •3.4. Модели эвристического поиска решений
- •3.4.1 Стратегия поиска в глубину
- •3.4.2. Стратегии перебора с отсечениями
- •3.4.2.1. Метод ветвей и границ
- •3.4.2.2. Стратегии поиска на основе эвристической функции оценки
- •3.5. Методы вывода и доказательства теорем
- •3.5.1 Механизм резолюции Робинсона
- •3.5.2. Резолюция в логике высказываний
- •3.5.2.1 Линейная резолюция вL
- •Метод линейного вывода в lЛавленда, Ковальского и Кюнера
- •Эффективная реализация
- •3.5.2.3. Метод поиска в глубину
- •3.5.2.4 Эвристики поиска в дереве
- •3.5.2.5. Семантическая резолюция
- •3.5.3 Резолюция в pl
- •3.6. Методы индуктивного вывода
- •3.6.1. Виды индукции
- •3.6.2. Индукция как вывод и индукция как метод
- •3.6.3. Правила, необходимые для систем автоматического формирования знаний
- •3.7. Дедуктивный вывод на семантических сетях
- •3.7.1. Нерезолютивные методы вывода на семантических сетях
1.3. Машина вывода
1.3.1. Понятие формальной системы
Прежде чем мы сформулируем понятие машины вывода, нам необходимо дать определение формальной (аксиоматической) системы и правил вывода. Под формальной системой понимается четверка:
М = <Т, Р, А, П>, (1.10)
где Т - множество базовых элементов;
Р - множество правил построения правильных (сложных) объектов из базовых элементов;
А - множество изначально заданных объектов формальной системы (множество аксиом );
П - множество правил построения новых объектов из других правильных объектов системы.
Для того, чтобы выяснить смысл этих формализмов, рассмотрим введенную ранее логическую модель как пример аксиоматической системы.
В качестве множества базовых элементов Т здесь используются элементы языка логики предикатов: переменные, константы, функциональные и предикатные символы и вспомогательные знаки.
В качестве множества правил Р построения правильных (сложных) объектов логики предикатов выступают правила построения формул логики предикатов.
Например, следующая формула является правильно построенной
(x(y( z( P(x, y) (z))))),
в то время как объект ниже
(x P(x, y)) (z((z)))
не является правильно построенной формулой.
Множество аксиом - это множество формул, истинность которых постулируется без доказательства.
Постулаты логики предикатов имеют вид схем аксиом. Схема аксиомы - это математическое выражение, которое дает конкретную аксиому каждый раз при подстановке вместо какой-то буквы одной и той же формулы.
Схемы аксиом логики предикатов таковы:
A (B A)
(A B) ((A (B C)) (A C))
A (B A & B)
A & B A
A & B B
A A B
B A B
(A C) ((B C) (A B C))
(A B) ((A )A)
A
x A(x) A(t)
A(t) xA(x)
Постулаты арифметики:
1. A(o) & x (A(x) A(x’)) A(x) (аксиома индукции)
2. a = b a = b
3. a = b (a = c b = c)
4. A + 0 = a
5. a 0 = 0
6.
7. a = b a = b
8. а + b = (а + b)
9. a b = a b + a
Здесь A,B,C- формулы; х - переменная;t- терм;a,b,c- целые числа; операция (’) (штрих) соответствует добавлению к числу единицы: а’ = а + 1.
Рассмотрим, например, схему аксиом (7). Заменим формулу А В наВ и подставим (7)
Далее по правилам де Моргана: =получаем:
Нетрудно видеть, что схема аксиом (7) является тождественно истинной, если истинна формула A .
Мы, однако, не в состоянии доказать последнюю формулу, т.е. считаем ее истинной по определению.
Воспользуемся примером, иллюстрирующим это положение.
Рассмотрим высказывание "последовательность 0123456789 встречается в разложении числа ". Обозначим это высказывание через А. Тогда обратное высказываниеозначает, что "последовательность 0123456789 не встречается в разложении числа". Для того, чтобы доказать формулу А (или) в принципе нужно строить бесконечное представление для числа. Поскольку ни один шаг такого "доказательства", если он не приводит к отысканию требуемой последовательности, не является законченным, мы не вправе считать, что доказана формула А (). Итак, мы в принципе не в состоянии укачать финитное (конечное) доказательство ни для формулы А, ни для формулы.
Будем записывать десятичное разложение числа , а под ним десятичную дробь= 0,333.... При записи каждой очередной цифры в разложениидобавляем "3" в. Если окажется, что высказывание А истинно, то стираем записанное представление дляи полагаем
где k- число троек, полученных в представлении к данному моменту.
Допустим, что справедлива формула В, где В - это высказывание "число рационально", и- обратное высказывание, т.е. число не рационально.
Спросим себя, рационально ли или нет? Еслине рационально (верно), то должно быть верно(иначе, если бы была получена последовательность 0123456789), то
где х, у - целые, т.е. было бы рационально. Однако, если справедливо , то= 1/3 = 0.333... (бесконечная последовательность). Здесьрационально, что противоречит предположению о его нерациональности. Итак,не может быть не рациональным. Но значитрационально. Для этого однако, нужно иметь доказательство А или, чего у нас нет.
Действительно, если рационально либо мы построили бесконечную последовательность 0,333... (что невозможно), либо доказали формулу А.
Приведенный пример характеризует так называемое интуиционистское направление в математике. Так интуиционисты отрицают правило tertiumnondatyr(третьего не дано). Ими также подвергается критике само понятие отрицания: ложность любой формулытрактуется ими так, что допущениеведет к противоречию.
Еще один философский пример того же рода демонстрирует так называемый парадокс лжеца: "если некто говорит, что он лжет, то говорит ли он на самом деле правду или лжет?"
Обозначим высказывание "Я лгу " через А. Если А истинно, то "некто в действительности лжет", т.е. должно быть и наоборот. А это означает, что формулаA ни истинна, ни ложна (противоречива).
Вернемся, однако, к истине (1.10). Нам осталось определить правила вывода П. Каждое правило вывода имеет структуру вида:
(1.13)
означающую, что если выведены формулы 1,2, ...,n, называемые посылками, то выводима также формуланазываемая заключением.
Под выводимостью формулы из формул1,2, ...,n, понимается такое отношение между этими формулами, что всякий раз, когда истинна каждая из формул1,2, ...,n, истинна также формула.
По определению, аксиома имеет структуру
,(1.14)
т.е. невыводима из других формул (множество посылок пусто).
Отметим следующие основные свойства для отношения выводимости.
1. Рефлективность:
(1.15)
2. Транзитивность:
(1.16)
(если выводима изи извыводима, то извыводима формула).
3. Монотонность:
(1.17)
(если из выводима формула, то присоединение кформулыне отменяет выводимость). Отметим, что свойство монотонности в общем случае не имеет места в некоторых неклассических логиках, рассматриваемых в главе 3.
4. Теорема дедукции:
Если из ивыводима формула, то извыводима формула(- импликация).
(1.18)
Верна также обратная теорема:
(1.19)
Теорема дедукции имеет весьма важное значение в логике. Действительно, чтобы доказать выводимость
(1.20)
заменим формулу эквивалентной формулой, где- символ пустой формулы (лжи). Используя эквивалентную замену, получим
Т
В качестве основных правил вывода в логике предикатов используются правила modusponensиgeneralization.
Правило modusponens:
(1.22)
утверждает, что если истинны формулы А и А В, то истинна формулаB.
Правило generalization:
.(1.23)
Справедлива и обратное
(1.24)
при условии, что С не содержит переменной. х. Это последнее правило существенно важно при реализации наиболее широко применяемого резолютивного вывода, с содержанием которого мы познакомимся позднее.
В частности, если С пустая формула, то имеет место
(1.25)
Пример правила generalization:
Отметим, что правила вывода в логике предикатов не исчерпывают множества всех известных правил вывода. Однако, правила вывода имеют иное семантическое содержание. Об этом следующий параграф.