Страница 45 из 49
Глава третья
Исчисление высказываний. Эта формальная система описана во всех руководствах по математической логике, например в [45]. Цитаты из Д. Самойлова заимствованы из сборника [46].
«Логик-теоретик». Существует весьма много программ, с помощью которых демонстрировались возможности ЭВМ при доказательстве выводимости формул в исчислении высказываний. Например, одна из первых работ в данной области [47] и первая отечественная система такого рода [48]. Программа «Логик-теоретик» была первым шагом на пути создания А. Ньюэллом и Г. Саймоном общей концепции решения творческих задач на ЭВМ на основе организованного эвристически перебора по лабиринту возможных альтернатив. Эта идея была воплощена ими в виде программы, названной «Общий решатель задач». Работы по этому кругу вопросов печатались неоднократно, например [49, 50]. Как позже выяснилось, подход к решению задач, реализованный в «Общем решателе задач», оказался не столь плодотворным, как думали авторы. Но для организации вывода в исчислении высказываний он удобен, хотя программа не всегда без большого перебора могла находить нужные пути по множеству альтернатив. В работах [49, 50] по этому поводу имеется немало экспериментальных наблюдений как над людьми, ищущими вывод, так и над работой программы «Логик-теоретик»
Исчисление предикатов. Исчисление предикатов описано во всех учебниках. Сошлемся на [45]. Проблема соответствия логики предикатов и силлогистики Аристотеля до сих нор вызывает некоторую полемику [31, 51]. Еще во второй половине 40-х годов известный логик Я. Лукасевич построил специальную формальную систему для силлогистики [52]. Он оставил два квантора A и I, положив по определению, что Esp=Isp и Osp=Asp. Выражения Asp и Isp Лукасевич отнес к элементарным (неделимым далее) формулам. В качестве аксиом он выбрал следующие четыре формулы: Ass; Iss; (Amp&Asm)Asp; (Amp&Ims)Isp.
Я. Лукасевич ввел три правила вывода: 1) в выводимую формулу вместо любой переменной типа s, p или m можно одновременно по всей формуле подставить любую формулу исчисления; 2) в выводимой формуле вместо любой переменной можно по всей формуле поставить другую переменную; 3) модус поненс.
Изложение вопросов, связанных с процедурами автоматизации доказательств, можно найти в монографии [53].
Первым универсальным методом доказательства был предложенный в 1965 году американским логиком Дж. Робинсоном метод резолюций. Его появление совершило переворот в использовании ЭВМ для доказательства теорем в исчислении предикатов. Начиная с работы самого Робинсона [54], возник огромный поток исследований в этом направлении. В монографии [53] на зафиксированном в ней временном срезе дан аналитический обзор всего сделанного в этой области. Но и до сегодняшнего дня всевозможные модификации метода Робинсона продолжают оставаться предметом публикаций.
Появление языка программирования ПРОЛОГ вновь стимулировало интерес к методу резолюций. Язык ПРОЛОГ, считающийся весьма перспективным для ЭВМ новых поколений, позволяет эффективно описывать выполняемые в нем процедуры в виде вывода в исчислении предикатов (точнее, в некоторой части этого исчисления, связанной с дизъюнктами Хориовского типа, исключающими некоторые типы выражений). А так как метод резолюций есть универсальная процедура для Хорновских дизъюнктов, то понятен тот интерес, который специалисты по программированию, созданию ЭВМ новых поколений и пользователи, оперирующие ПРОЛОГом, проявляют к методам типа метода резолюций.
Общая схема вывода. Описанное в этом разделе представление имеет куда большее значение, чем то, о котором в нашей книге идет речь. В теории искусственного интеллекта И-ИЛИ деревья и И-ИЛИ сети встречаются не только при моделировании рассуждений. Они широко используются при представлении знаний о проблемных областях разного типа. Находят они применение и в лингвистических процессорах, предназначенных для анализа текстов на естественном языке. В монографиях [55–57] заинтересованные читатели могут найти описание областей применения таких моделей. Идея метода обратного вывода принадлежит С.Ю. Маслову. Впервые она сформулирована в работе [58]. В настоящее время в СССР имеются версии программной реализации этого метода, во многом не уступающего по своей эффективности методу резолюций Робинсона. Рассказ Э. По, из которого приведена цитата, помещен в [59].
Глава четвертая
Стебаков Сергей Александрович – советский математик, специалист в области топологии, качественной теории дифференциальных уравнений и теории управления.
От Аристотеля до Бэкона. Историю становления учения об индукции до начала XX века содержит монография [60]. Для ознакомления с более поздним пониманием этих вопросов можно рекомендовать статьи из сборника [61]. Специально логике формирования гипотез посвящена работа [62]. Высказывание Р. Грегори о небиологичности дедукции и о роли индукции для живых организмов заимствовано из [63, с. 187].
Индукция Джона Стюарта Милля. Взгляды Милля изложены в его сочинении, вышедшем в 1843 году. Позже эта книга была переведена на русский язык [64]. Цитата из В. Луговского взята из поэмы «Сказка о дедовой шубе», вошедшей в книгу [65]. Все формулировки принципов Милля сделаны в соответствии с текстами из [60].
Читатели, знакомые с методами распознавания образов, должны почувствовать почти дословное совпадение принципов Милля с приемами, используемыми в обучении распознаванию и классификации с помощью обучающих выборок из примеров и контрпримеров. Первое и наиболее полное описание подобных приемов содержится в [66]. Другие подходы к решению подобных же задач имеются в многочисленных публикациях по распознаванию образов. Укажем лишь наиболее близкие по духу методы, описанные в работах [67–69]. Такая близость между индуктивными методами рассуждений и распознаванием (вернее, узнаванием и классификацией) образов еще раз подчеркивает верность замечания Р. Грегори, процитированного в предыдущем разделе.
Рассуждения по аналогии. Первой программой, в которой были реализованы принципы работы с пропорцией Лейбница была, по-видимому, программа «Аналогия», разработанная Т. Эвансом в конце 60-х годов. Она с успехом решала задачи типа задач на аналогию из известной книги головоломок Г. Айзенка [70].
Программа, находящая аналогии для множества родственников, была создана Д. Румельхартом и А. Абрахамсоном в 1973 году. Именно в ней была использована идея семантического пространства Осгуда. Метод построения этого пространства основан на следующих экспериментах. Испытуемым предъявляют около 400 шкал, на концах которых стоят слова-антонимы, описывающие признаки (например, добрый – злой, острый – тупой, быстрый – медленный). В середине шкалы находится нейтральное деление (оно отмечено словосочетаниями типа не добрый – не злой; не острый – не тупой; не быстрый – не медленный). Кроме того, на шкале имеется еще по несколько делений слева и справа от нейтрального деления. Они никакими словами не маркируются. Испытуемым задается (всем одинаковый) список слов (например, отец, дерево, шило и т.п.), и их просят расположить каждое из слов списка на всех шкалах. Многие шкалы испытуемым кажутся весьма неподходящими для расположения заданных слов (например, как разместить слово «отец» на шкале острый – тупой?). В этих случаях экспериментатор предлагает размещать их «как хочется». После этого шкалы с нанесенными на них словами подвергаются статистической обработке по методу факторного анализа и выделяются основные факторы.