Формально-грамматическая модель логического вывода в системах искусственного интеллекта тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

ВВЕДЕНИЕ.

ЛОГИЧЕСКИЙ ВЫВОД И МЕТОДЫ ПОВЫШЕНИЯ ЕГО ЭФФЕКТИВНОСТИ В

СИСТЕМАХ ИИ (ОБЗОР).

Глава 1. МЕТОД ПОСТРОЕНИЯ ЛОГИЧЕСКОГО ВЫВОДА В ИВ, ОПИРАЮЩИЙСЯ НА ФОРМАЛЬНО-ГРАММАТИЧЕСКУЮ МОДЕЛЬ.

1.1. Хорновские дизъюнкты ИВ и КС-грамматики.

1.2. Моделирование множества гипотез ИВ КС-грамматикой.

1.3. Построение логической шкапы и проверка выводимости целей.

1.4. Алгоритм предварительной настройки для построения логических выводов.

1.5. Построение опровержений в множествах дизъюнктов

ИВ методом с предварительной настройкой.

1.6. Особенности построения опровержений в рекурсивном случае.

В последнее время наблюдается тенденция к интеллектуализации инструментальных программных средств научных исследований, использованию экспертных систем, систем, основанных на знаниях, применению механизмов и методов искусственного интеллекта (ИИ). Одним из фундаментальных направлений в этой области является автоматическое доказательство теорем [34,51,54,80,87,1283, опирающееся на логическую форму представления знаний и революционные методы в качестве механизма логического вывода. Эти методы имеют практическую реализацию в логическом программировании, в частности, в декларативном языке Пролог.

Бойером с соавторами [893 предложено дизъюнктивное представление для всех аксиом теории множеств вместе с основными определениями, относящимися к этой теории. Полученные дизъюнкты непосредственно применимы в методах доказательства теорем, основанных на резолюции. Многочисленные работы [93-96,1413 посвящены переформулировке на логический язык элементарных геометрий и, в частности, представлению евклидовой геометрии языком хор-новских дизъюнктов. Это делает возможным применение логического программирования для автоматического доказательства теорем геометрии.

Несмотря на определенное разочарование, связанное с выдвинутым в восьмидесятых годах японским проектом создания ЭВМ пятого поколения, архитектура которой должна была базироваться на применении механизмов Пролога в качестве внутреннего машинного языка [49,65,66,863, и критику универсальности Пролога как инструментального средства (ИС) доказательства теорем, для решения целого ряда задач логические методы сохраняют свое важное значение. Привлекательность методов заключается прежде всего в их мощности и хорошей теоретической разработанности.

Пролог остается распространенным ИС искусственного интеллекта [15,21, 32,48,56, 64,74,84]. [20,35,38,85,117,135,144] содержат описания некоторых из последних реализаций интеллектуальных систем важного прикладного значения, основанных на логических принципах и методах автоматического доказательства теорем. Системы [11,46,60,76,82,83,90] могут быть непосредственно применены при решении научно-исследовательских задач. На основе развития логических методов и Пролог-идей создаются новые инструментальные системы ИИ [7,8,118].

Наблюдается тенденция к объединению средств логического и функционального, объектно-ориентированного или процедурного программирования, что значительно расширяет их выразительные возможности. Конструкции и механизмы логических языков инкорпорируются в синтаксическую среду таких традиционных языков программирования, как Паскаль [41]. С другой стороны, современные реализации декларативных языков предполагают наличие интерфейса для подключения программных модулей на языке Си и т. п. [78, 79]. В области прикладных программ большое внимание уделяется созданию экспертных систем, основное управление в которых осуществляется обычными алгоритмическими средствами, а обработка знаний производится с помощью логических методов [5,33, 38,46,85]. Создаются гибридные интеллектуальные системы [21,27,28,77,106, 116], в которых обладающие высокой выразительной способностью сетевые, продукционные или фреймовые модели знаний сочетаются с хорошо разработанными для логики механизмами вывода.

Бурно развивающейся областью являются дедуктивные базы данных, основанные на логике предикатов первого порядка [24,52,

81,104,108,125,130], для которых был создан язык типа Пролога -Datai og [136].

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

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

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

2. Учет специфики предметной области и характеристик БЗ для каждой конкретной задачи.

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

В рамках второго из указанных направлений представляет интерес идея предварительной, полной или частичной, подготовки ответов на возможные запросы для стационарных, то есть постоянных или редко меняющихся, БЗ. Из литературы известны следующие реализации этой идеи. Предварительная подготовка ответов на возможные запросы с помощью построения таблиц параметров использована для реляционных баз данных [73], предварительная реорганизация БЗ за счет компиляции специальных знаний осуществлена в системе с абдуктивным выводом [97], в экспертных системах на основе декларативных продукций предварительно проведен частичный индуктивный вывод [40]. К сожалению, в настоящее время не существует эффективной реализации этой идеи для логических БЗ: подход на основе индуктивного вывода (полного или частичного) неэффективен.

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

Перспективным в этом направлении представляется использование формально-грамматической модели, опирающейся на КС-грамматику [51,100].

В настоящей работе были поставлены и решены следующие задачи:

1. Исследовать возможность применения формально-грамматической модели для стационарных БЗ, представленных множеством хорновских дизъюнктов исчисления высказываний (ИВ).

2. Исследовать возможность применения алгоритма выделения укорачивающих символов в КС-грамматике в качестве средства предварительной настройки для дальнейшей проверки выводимости целей. Разработать на основании этого алгоритма процедуру предварительной настройки, приспособленную для построения в дальнейшем логических выводов.

Ограниченная выразительная способность ИВ требует использования исчисления предикатов первого порядка (ИП) для описания большинства задач искусственного интеллекта. В связи с этим были поставлены следующие задачи:

3. Обобщить на ИП метод логического вывода с предварительной настройкой, опирающейся на формально-грамматическую модель.

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

В работе были получены следующие основные результаты.

1. В главе 1 предложено описание множества гипотез ИВ с помощью КС-грамматики с невыделенным начальным символом, что позволяет проводить обработку БЗ до задания запросов к ней.

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

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

Показана полнота метода логического вывода с предварительной настройкой для ИВ. Даны оценки сложности алгоритмов предварительной настройки (квадратичная относительно множества гипотез) и проверки выводимости целей с помощью логической шкалы (линейная относительно длины целевого утверждения).

2. В главе 2 предложен подход к обобщению метода с предварительной настройкой на ИП на основе комбинации формально-грамматической модели и метода резолюционного доказательства с пропозициональной абстракцией.

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

Показана полнота метода для ИП.

3. В главе 3 сконструировано новое абстракционное отображение с расширенными высказываниями. Описаны соответствующие дизъюнктивная и формально-грамматическая модели.

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

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

Практическая значимость исследования определяется тем значением, которое имеют для развития информатики методы ИИ. Методы с предварительной настройкой могут быть реализованы в качестве внутренних универсальных механизмов логического вывода в системах ИИ различных областей применения для стационарных баз знаний.

- 10

ЛОГИЧЕСКИЙ ВЫВОД И МЕТОДЫ ПОВЫШЕНИЯ ЕГО ЭФФЕКТИВНОСТИ В

СИСТЕМАХ ИИ (ОБЗОР)

Логические основы искусственного интеллекта изложены в [4,22, 34,43, 51,54,61, 62,67, 80,113,128 и др. ]. Знания представляются в виде стандартизированных формул (конъюнктивных нормальных форм) ИВ или ИП. Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов. Дизъюнктом называется дизъюнкция конечного числа литер, то есть lj \ДгУ- • • Vln- При этом для ИП рассматриваются только клаузальные формы, то есть предваренные КНФ, все переменные в которых V-квантифицированы. Существенным является то, что любое выражение логики высказываний и логики предикатов может быть преобразовано в КНФ.

Решение задач логического характера базируется на доказательстве теоремы о существовании решения. Идея использования техники доказательства теорем для решения задач принадлежит Р.Ковальскому [433. Теорема существования решения утверждает, что если S есть модель задачи, то существует выходной набор Sol, являющийся результатом применения к S решающей процедуры. Иначе говоря, теорема существования связывает входные данные, выходные результаты и процедуру решения. Если задача сформулирована на языке математической логики, то техника решения задачи через доказательство теоремы существования заключается в выполнении следующей схемы:

1) для задачи формируется теорема существования решения;

2) строится доказательство теоремы существования решения;

3) из доказательства теоремы существования извлекается процедура решения задачи.

- И

Основная проблема в приведенной выше схеме - это построение доказательства, или логического вывода.

Классическим механизмом логического вывода является метод резолюций, предложенный Дж.Робинсоном в 1965 году [70] и опирающийся на принцип дедукции. Общая идея метода состоит в следующем: чтобы получить некоторое заключение С, исходя из гипотез Н^Нг,., Нп, то есть проверить, является ли С логическим следствием гипотез Н!, Н2Нп, достаточно проверить, является ли противоречивой формула ^ДН^Л. ЛНПЛ1С, в которой отрицание заключения добавлено к исходным гипотезам. При этом рассматриваются лишь формулы стандартного вида - КНФ. Тогда полученная формула может быть интерпретирована как множество дизъюнктов 8={Н1,Н2, .,Нп,1С), доказательство невыполнимости которого эквивалентно построению в нем логического вывода пустого дизъюнкта Л.

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

А\/Х,ВУШ Н А\/В, где А, В, X - формулы.

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

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

Метод резолюции является недетерминированным, и в общем случае неэффективен. Его наиболее существенный недостаток заключается в формировании всевозможных резольвент, большинство из которых оказывается ненужными. Существуют различные модификации метода резолюций, направленные на уменьшение длины вывода и, в конечном итоге, на сокращение числа лишних порожденных резольвент, не влияющих на выводимость пустого дизъюнкта. Эти модификации, известные в литературе как стратегии метода резолюций или суживающие стратегии, рассмотрены в [22,34,51,54,61,62,80, 124]. Общим правилом является исключение из рассмотрения порождаемых дизъюнктов типа тавтологий и поглощенных дизъюнктов, которое не меняет выполнимости множества дизъюнктов.

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

Семантическая резолюция была предложена в [134]. В ней используется интерпретация для разделения множества дизъюнктов Б на два класса: Б! - непустое множество дизъюнктов, которое выполняется (т.е. принимает значение "истина") некоторой интерпретацией, £>2 - непустое множество дизъюнктов, которое не выполняется (т.е. принимает значение "ложь") этой интерпретацией; 81и$г=8. Разрешается резольвирование дизъюнктов, принадлежащих только разным множествам, и запрещается образование резольвент от дизъюнктов, входящих в одно и то же множество. Тем самым сокращается образование ненужных дизъюнктов, так как только ре-зольвированием из разных множеств можно получить пустой дизъюнкт.

Другим способом ограничения количества порождаемых дизъюнктов является упорядочение предикатных букв. Если имеется упорядочение предикатных букв типа Р1>Р2>. то разрешается резервирование литеры, обладающей наибольшим порядком, то есть

Pi

В семантической резолюции допускается любая интерпретация и любое упорядочение предикатных букв. Семантическая резолюция полна. Специальными случаями семантической резолюции являются положительная и отрицательная гиперрезолюция [131] и стратегия множества поддержки [1433.

Идея лок-резолюции состоит в использовании индексов для упорядочения литер в дизъюнктах из множества дизъюнктов S. Иными словами, она включает индексацию произвольным образом каждого вхождения литеры в S некоторым целым числом; разные вхождения одной и той же литеры в S могут быть индексированы по-разному. После этого резольвировать разрешается только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставится в соответствие наименьший из этих индексов.

Лок-резолюция полна и является весьма эффективным методом логического вывода. Основным недостатком лок-резолюции является то, что она несовместима с большинством других стратегий, даже таких естественных, как, например, со стратегией избегания противоречивых дизъюнктов [80]. Кроме того, совершенно неясно, как по данному множеству дизъюнктов a priori установить, какая из начальных индексаций литер дает более эффективную лок-резолюцию.

Линейная резолюция была независимо предложена в [120] и [123], а позднее усилена [115]. Линейным выводом из множества дизъюнктов S называется последовательность дизъюнктов С!,С2,.,СП, в которой верхний дизъюнкт CjES, а каждый член

С1 + 1, 1=\, 2,., п-1, является резольвентой дизъюнкта С^, называемого центральным, и дизъюнкта В^ называемого боковым. При этом В1 должен удовлетворять одному из следующих двух условий: 1) либо В^Б, 1=1,2,., п-1, 2) либо В4 является некоторым дизъюнктом Сд, предшествующим в выводе дизъюнкту , то есть Таким образом, линейный вывод начинается с некоторого дизъюнкта, применяет к нему правило резолюции для получения резольвенты, затем применяет резолюцию к этой резольвенте и некоторому дизъюнкту, и так далее, пока не будет получен пустой дизъюнкт.

Линейная резолюция может быть дополнительно усилена введением понятия упорядоченного дизъюнкта и использованием информации о резольвированных литерах [121,122]. В таком виде она называется ОЬ-выводом и является разновидностью линейной резолюции с функцией выбора (БЬ-вывод) [123]. Лавлендом, Ковальским и Кюнером установлены условия, при которых центральный дизъюнкт позднее может участвовать в роли бокового дизъюнкта. Это свойство позволяет сократить число лишних дизъюнктов, поскольку становится ясно, будет ли тот или иной центральный дизъюнкт использован для порождения пустого дизъюнкта, или нет.

Линейная резолюция и ОЬ-вывод полны. Линейная резолюция является одной из наиболее эффективных стратегий [54]. Особую привлекательность линейному выводу придает его простая структура. Кроме того, линейная резолюция совместима со стратегией множества поддержки, вместе с ней удобно применять эвристические методы.

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

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

Имеются уточнения линейной резолюции, которые эффективны (для ИВ), но не полны в общем случае. Речь идет о единичной [109,1423 и входной линейной [88, 113,1383 резолюциях. Несмотря на свою неполноту, эти стратегии гораздо легче реализовать на ЭВМ, чем общий случай линейной резолюции, они эффективнее линейной резолюции и достаточно мощны для того, чтобы доказать большой класс теорем. Единичная и входная резолюции эквивалентны [91], они полны для случая хорновских дизъюнктов.

Входная линейная резолюция (БУЗ-резолюция) - линейная резолюция, в которой одна из двух посылок - входной дизъюнкт, то есть член заданного исходного множества Б дизъюнктов. При реализации входной линейной резолюции, как правило, в качестве верхнего берется дизъюнкт цели, а в качестве боковых дизъюнктов - гипотезы (факты и правила базы знаний). Входная линейная резолюция легла в основу языка логического программирования Пролог. Теоретические основы Пролога рассмотрены в [2, б, 10,18,25, 31,42,45,753. Пролог обладает универсальными средствами управления поиском логического вывода - механизмами рекурсивного вызова процедур, обобщенного сопоставления с образцом (унификацией), поиска с возвратами (бектрекингом). Эти механизмы обеспечивают недетерминированный вывод и позволяют находить все возможные решения описанной логической программой задачи.

Единичная резолюция - это линейная резолюция, в которой по крайней мере одна из посылок - единичный дизъюнкт. Использование единичной резолюции приводит к тому, что на каждом этапе некая литера удаляется из одного дизъюнкта. Поэтому алгоритм проверки невыполнимости конечных множеств хорновских дизъюнктов ИВ с помощью линейной единичной резолюции имеет сложность Ы2 [51,111], где N - число литер, первоначально присутствующих в Б с учетом повторений. Поскольку единичная и входная линейная резолюции эквивалентны, для последней справедлива та же оценка. Сейчас существует линейный по времени алгоритм проверки невыполнимости множеств хорновских дизъюнктов ИВ [100].

Для ИП оценка эффективности этих революционных стратегий будет существенно хуже (в общем случае сложный алгоритм), так как дизъюнкт ИП может допускать бесконечно много конкретизации Кроме того, в логике предикатов затруднено нахождение контрарных пар, то есть литер, играющих роль X и IX в правиле резолюций. Это приводит к необходимости предварительного этапа согласования формул таким образом, чтобы аргументы отсекаемых контрарных литер совпадали. Согласующая процедура называется унификацией. Алгоритм унификации подробно рассмотрен в [22,47, 51,54, 80,102].

Для получения полиномиальной оценки по времени необходимо введение дополнительных ограничений на КНФ и хорновские формулы ИП. Так, для ИП предложен полиномиальный (квадратичный по времени) алгоритм для баз знаний, описываемых хорновскими формулами с одноместными предикатами. Существенные ограничения накладываются также на использование функций [37]. В работе [63] предлагается частный случай семантической резолюции, эффективный для сингулярных баз знаний, т. е. описываемых одноместными предикатами и функциями. Однако накладываемые в этих случаях ограничения на базы знаний на практике неприемлемы, поскольку, в то время как любой т-арный предикат может быть представлен в виде произведения бинарных [43,51], требование одноместности предикатов базы знаний существенно снижает выразительную способность логической модели.

Методом, альтернативным резолюции, является обратный дедуктивный метод Маслова [57]. Он сформулирован для аксиоматических систем, но может быть также применен и для логических исчислений. В этом методе поиск вывода идет от целевой формулы к аксиомам или постулатам, истинность которых априорно известна. Чтобы определить выводимость формулы С из посылок Н^ Н2,., Нп, необходимо найти формулы-предшественники, из которых С может быть выведена одним применением правила вывода. Затем по каждой из полученных формул-предшественников, не являющейся аксиомой исчисления, в свою очередь определяется множество непосредственных формул-предшественников и так далее, вплоть до построения окончательного вывода.

На основе обратного метода вывода были разработаны и реализованы машинный алгоритм вывода [23] и алгоритм машинного поиска логического вывода в ИВ [3], носившие экспериментальный характер, было показано что метод может быть также распространен на весьма широкие классы дедуктивных систем [59].

Для стандартизированных формул метода резолюций оба метода примерно эквивалентны [58]. Кроме того, идеи стратегий и доказательств их полноты обычно равноприемлемы для метода резолюций и обратного метода.

Обратный дедуктивный метод Маслова представляет большой интерес, однако его исследование выходит за рамки настоящей работы.

Существует целая серия методов, опирающихся на различные интерпретации логических формул и метода резолюций: матричную [30,34,50], в виде графов [43,61,62,100,101,105,114], в виде формальных грамматик [12,51,92,100,133], и использующих соответствующие формальные методы. На модификации метода резолюций основаны метод групповых резолюций [22] и метод для ИВ, использующий двунаправленный вывод [19].

Поскольку задача разрешимости логического выражения, приведенного к КНФ, для ИП является ИР-полной [98], общая оценка этих методов совпадает с оценкой для метода резолюций. Однако для некоторых частных случаев их применение может приводить к существенному ускорению вывода.

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

Учет контекста применения унификаций обеспечивается, как правило, внелогическими средствами. К ним относятся так называемые средства управления ходом вычислений, такие, как операторы отсечения и замораживания, имеющиеся практически во всех реализациях языка Пролог [2, 6,26,32, 39, 42,45,55, 68,71, 72, 99,112, 126], специальные мета-конструкции [5,68,103,139]. В языке 1С-Пролог к правилам могут добавляться специальные аннотации,

- 19 влияющие на порядок вычислений [2,9,13,68].

Реализации Пролога для йЕС-Ю, МПролога содержат средства индексирования процедур, позволяющие ускорять поиск подходящей альтернативы благодаря изучению значений определенных аргументов [26,31,39,42]. Таким образом, порядок исполнения вызовов процедуры делается зависимым от характера ее использования. Введение таких средств позволяет пропустить некоторые промежуточные вычисления, если их результаты уже известны [132]. В Ш-Прологе эффективность вычислений повышается за счет изменения порядка обработки литер цели. Обработка подцели откладывается в тех случаях, когда на данном этапе это может привести к большим затратам времени [2,127]. Оценка "выгодности" обработки той или иной литеры проводится путем сравнения количества имеющихся для нее в базе фактов, а также с помощью средств, позволяющих указывать, при каком наборе аргументов имеет смысл обрабатывать рекурсивную литеру. Обработка некоторых подцелей откладывается и в 1С-Прологе.

Следует, однако, отметить, что применение указанных средств возможно только на основании анализа предполагаемого решения задачи и требует от программиста четкого представления о поведении алгоритма решения, что лишает логическое программирование "прозрачности" и противоречит его основному принципу -декларативности [68, 69].

Проблема сохранения декларативности весьма важна. Реализация метода резолюций в Прологе просматривает дизъюнкты множества гипотез по очереди сверху вниз, что делает существенным порядок их следования, в то время как с точки зрения логики они все равноправны. Как следствие, алгоритм Пролога не является полным, хотя логическая система, на которой основан Пролог, адекватна и полна. Некоторые компиляторы (например, Турбо Пролог [1,32]), кроме того, предъявляют дополнительные требования к порядку записи утверждений базы знаний. Предоставляемые Прологом внелогические средства, такие, как отсечение и другие, изменяют ход вычислений логической программы, что также снижает декларативность Пролог-системы. Нарушение декларативности приводит к потере "прозрачности" средств логического программирования, что ограничивает их применение в качестве ИС для решения задач.

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

Создание в 1977 году Д.Уорреном компилятора языка Пролог доказало, что этот язык логического программирования может быть реализован так же эффективно, как и другие языки искусственного интеллекта [140]. Тем не менее, вычислительными машинами с традиционной "фон неймановской" архитектурой логические программы выполняются медленнее, чем соответствующие программы на традиционных процедурных языках. Что касается схемы управления памятью, то в современных реализациях Пролога она не уступает традиционным языкам программирования, по крайней мере для случая детерминированных процедур [14,26].

Таким образом, основной проблемой логического программирования является его относительная малоэффективность по времени по сравнению с обычными процедурными языками [12,13,26,69]. Поэтому основной задачей для систем логического программирования, использующих механизмы автоматического доказательства теорем, является ускорение логического вывода. Существует два направления решения этой задачи [12, 69]:

- 21

- Использование естественного параллелизма методов логического вывода, подразумевающее разработку параллельных реализаций Пролога и соответствующих аппаратных средств [18,863. Эта идея легла в основу проекта создания ЭВМ пятого поколения с принципиально новой, параллельной архитектурой;

- Разработка новых эффективных универсальных методов решения логических задач, поиск методов и средств ускорения логического вывода.

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

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

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

- 22

Методы предварительной обработки знаний с целью улучшения характеристик системы разработаны для абдуктивного вывода [97].

Аналогичная идея используется в [73] для реляционных баз данных. Предварительная подготовка ответов на возможные запросы осуществляется с помощью построения таблиц параметров с перечислением строк-записей, относящихся к каждому значению параметра, и введению перекрестных таблиц-связей параметров.

Отметим, что установление связей между согласующимися литерами в предложениях базы знаний проводится и в методе построения вывода с помощью графа соединений [43,114], хотя автор и не рассматривает в явном виде идею предварительной подготовки таких связей в БЗ.

Обработка БЗ на предварительном этапе проводится в семействе экспертных систем, разработанных в Институте автоматики и процессов управления с вычислительным центром ДВО АН СССР [40]. При этом до начала эксплуатации системы БЗ заменяются на синтезированные по ним программы, которые решают те же задачи, что и экспертные системы с исходными БЗ. В качестве методологического базиса синтеза программ используется принцип частичных вычислений А. П. Ершова [29]. Применение этого принципа состоит в том, что в программе - интерпретаторе базы знаний раскрываются все циклы, количество прохождений которых определяется состоянием базы, в тела этих циклов подставляется информация из правил и вычисляются или частично вычисляются условия и выражения, зависящие от состояния базы. Таким образом, до начала обработки запросов проводится, полностью или частично, индуктивный вывод из БЗ.

В некотором роде предварительную настройку на базу подразумевает и компиляция логических программ. Однако в этом случае оптимизация производится на уровне машинного кода и достигается в основном обработкой включенных в программу управляющих конструкций, рассмотренных ранее, то есть не затрагивает сути логических механизмов. Кроме того, существуют компиляторы логических программ, например, Турбо Пролог, требующие фиксации целевого утверждения до начала компиляции [1,78], что существенно снижает ценность этой процедуры.

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

- метод должен быть удобным для компьютерной реализации;

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

- метод должен быть универсальным в том смысле, что предварительная настройка должна осуществляться до задания конкретных целей и никак от них не зависеть;

- предварительная настройка на множество гипотез (БЗ) должна выполняться полностью автоматически и не требовать дополнительной "ручной" разработки;

- предварительная настройка должна быть эффективна и более компактна, чем обычный индуктивный вывод, хотя бы и частичный (это требование особенно актуально для ИП);

- метод должен по возможности не нарушать принципа декларативности, то есть обладать низкой чувствительностью к порядку записи утверждений БЗ.

В главе 1 предлагается метод логического вывода для множеств хорновских дизъюнктов ИВ, отвечающий всем вышеперечисленным требованиям. Настройка на БЗ реализована в виде процедуры, использующей представление множества гипотез в виде КС-грамматики. В главах 2 и 3 даны обобщения метода с предварительной настройкой на ИП на основе комбинации формально-грамматической модели и резолюционного доказательства с абстракциями.

Общий принцип абстракции, когда решение одной задачи сводится к решению другой [107], успешно применяется при организации различных процессов (поиск аналогий, самообучение) в интеллектуальных системах [110,119,137], позволяет добиться ускорения и улучшения качества функционирования системы в целом. Метод резолюционного доказательства с абстракциями описан в [1293.

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

В главе 3 исследуется возможность дальнейшего улучшения характеристик метода, для чего формируется новое абстракционное отображение и рассматривается комбинация абстракций.

- 25

3. 6. Основные результаты и выводы главы 3

Настоящая глава посвящена развитию метода с предварительной настройкой для ИП на основе подхода, изложенного в главе 2. Сконструировано новое отображение, частично сохраняющее информацию о значениях аргументов предикатов исходного множества гипотез. Получен результат, позволяющий использовать сконструированное отображение в качестве абстракционного.

Это отображение, названное отображением с расширенными высказываниями, вводит в абстракционное множество гипотез предикатные конкретизации, понимаемые как высказывания особого вида. В главе описана дизъюнктивная модель, позволяющая оперировать с высказываниями такого вида. По аналогии с главой 1 для нее предложена формально-грамматическая модель и алгоритм предварительной настройки.

Описан алгоритм параллельного построения выводов в абстрактном и исходном множествах гипотез.

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

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

ЗАКЛЮЧЕНИЕ

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

Разработано семейство методов с предварительной настройкой, ориентированных на представление баз знаний в виде множеств хорновских дизъюнктов и революционные механизмы вывода.

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

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

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

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

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

Компьютерная реализация метода с предварительной настройкой для ИВ и метода для ИП на основе пропозициональной абстракции осуществлена на языке Object Pascal в среде Borland Delphi в рамках дипломных работ на факультете прикладной математики и процессов управления Санкт-Петербургского государственного университета [17,36,53]. Компьютерное тестирование методов также подтвердило их эффективность.

Наиболее перспективным представляется метод, основанный на комбинации абстракционных отображений. Поэтому дальнейшие исс

1. Абилов В.Г., Зинченко Н.И. Turbo и Arity: два подхода к логическому программированию.// Мир ПК. -1990. -Ш. - С. 32-4 2.

2. Агафонов В. Н., Борщев В.Б., Воронков А. А. Логическое программирование в широком смысле (обзор). // Логическое программирование. Сб. ст. М. : Мир, 1988. - С. 298-366.

3. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. М.-Л.:Наука, 1965. - 39 с.

4. Александров В.В., Булкин Г.А., Поляков А. 0. Автоматизированная обработка информации на языке предикатов. М. : Наука, 1982. - 103 с.

5. Алиев Р.А., Абдикеев H. М., Шахназаров M. М. Производственные системы с искусственным интеллектом. М. : Радио и связь, 1990. - 264 с.

6. Антимиров В.Н., Воронков А.А., Дегтярев А. И., Захарьянцев М. В., Проценко В. С. Математическая логика в программировании. Обзор. // Математическая логика в программировании. Сб. ст. М. : Мир, 1991. - С. 331-407.

7. Атаян В.В., Мороховец Н. К. Сочетание формальных процедур поиска логического вывода и естественных приемов поиска доказательств теорем в системе автоматизации доказательств.// Кибернетический и системный анализ Кибернетика. 1996. -№3. - С. 151-182,191.

8. Батин Н.В., Герман 0. В. Обработка знаний в экспертных системах. Минск: МРТИ, 1993. - 63 с.

9. Белов В. Н. и др. Система для решения некоторых задач искусственного интеллекта. // Проблемы использования систем управления базами данных. Киев: ИК АН УССР, 1979. - С. 61-72.- 120

10. Белов В. Н., Брановицкий В. И., Вершинин К. П., Гецко Л. Н., Довгялло A.M., Ефименко С. П., Колос В. В. ПРОЛОГ язык логического программирования. // Прикладная информатика. Вып. 1. - 1986. - С. 24-58.

11. Борщев В. Б. Логическое программирование. // Известия АН СССР. Техническая кибернетика. 1986. - Ш. - С. 89-109.

12. Борщев В. Б. ПРОЛОГ основные идеи и конструкции. // Прикладная информатика. - М.: Финансы и статистика, 1986. -Вып. 2(11). - С. 49-76.

13. Бранохе М, Управление памятью в реализациях Пролога. // Логическое программирование. Сб. ст. М.: Мир, 1988. - С. 193-210.

14. Братко И. Программирование на языке Пролог для искусственного интеллекта. М.: Мир, 1990. - 560 с.

15. Братчиков И. Л. Синтаксис языков программирования. М.: Наука, 1975. - 232 с.

16. Буланов A.A., Калинина Т. В. Реализация метода поиска вывода в исчислении высказываний с предварительной настройкой. // Труды XXIX научной конференции факультета ПМ-ПУ СПбГУ "Процессы управления и устойчивость". СПб, 1998. - С.203-208.

17. Вишняков В.А., Буланже Д.Ю., Герман 0. В. Аппаратно-программные средства процессоров логического вывода. М.: Радио и связь, 1991. - 262 с.

18. Водяхо А. И., Мельцов В. Ю., Солдатов В. В., Страбыкин Д. А. Формальная система дедуктивного логического вывода в рамках- 123 логики высказываний. // Известия С.-Петербургского электротехнического университета. СПб, 1993. - №458. - С. 7-33.

19. Георгиев В.0. Модели представления знаний предметных областей диалоговых систем (обзор). // Известия АН СССР. Техническая кибернетика. 1993. - №5. - С.24-44.

20. Герман 0. В. Введение в теорию экспертных систем и обработку знаний. Минск: ДизайнПРО, 1995. - 255 с.

21. Дейт К.Дж. Введение в системы баз данных. Киев: Диалектика, 1998. - 784 с.

22. Дерансар П. Компиляция РИОЮС-программ по алгебраическим спецификациям. // Трансляция и оптимизация программ. Сб. -Новосибирск, 1983. С.137-153.

23. Домелкин Б., Середи П. Практическое использование Пролога. // Логическое программирование. Сб.ст. М.: Мир, 1988. -С. 167-192.

24. Донской В. И. Дуальные экспертные системы. // Известия АН. Техническая кибернетика (Россия). 1993. - №5. - С. 111-119.

25. Донской В. И. Логические продукционные системы: анализ и- 122 синтез. // Кибернетический и системный анализ. 1994. -№4. - С. 11-22,188.

26. Ершов А.П. О сущности трансляции. // Программирование. -1977. №5. - С. 21-39.

27. Закревский А. Д. Экспертная система логического распознавания как средство обучения методам логического вывода. // Логические исследования. Вып. 3. М.: Наука, 1995. -С.178-180.

28. Иванова Г.С., Тихонов Ю.В. Введение в МПролог: Практическое пособие для программистов.- М.: Изд-во МГТУ, 1990. 151 с.

29. Ин Ц., Соломон Д. Использование Турбо-Пролога. М.: Мир, 1993. - 608 с.

30. Искусственный интеллект: Применение в интегрированных производственных системах. М.: Машиностроение, 1991. - 544 с.

31. Искусственный интеллект. Справочник. Кн.2. Модели и методы, /ред. Д. А. Поспелов. - М.: Радио и сязь, 1990. - 303 с.

32. Калинина Т. В. Реализация двухэтапного метода поиска логического вывода в исчислении высказываний. Формапьно-грамма-тическая интерпретация: Дипл. работа ф-т ПМ-ПУ СПбГУ. СПб, 1998. - 83 с.

33. Канович М. И. Монадические хорновские базы знаний в экспертных системах. // Известия АН СССР. Техническая кибернетика. 1989. - №5. - С. 14-19.

34. Кларк К., Маккейб Ф., Грегори С. Средства языка IC-PR0L0G. // Логическое программирование. Сб. ст. М.: Мир, 1988. -С.245-260.

35. Клещев A.C. Реализация экспертных систем на основе декларативных моделей представления знаний: Препринт ДВО АН СССР. Владивосток, 1988. - 45 с.

36. Климов A.A. Разработка и экспериментальная реализация интеграции переборных средств языков Пролог и Рефал в синтаксическую среду языка Турбо Паскаль. Автореферат дисс. на соискание уч. степени к. ф.-м. н., СПб: СПбГУ, 1996. - 14 с.

37. Клоксин У., Меллиш К. Программирование на языке Пролог. -М.: Мир, 1987. 336 с.

38. Ковальски Р. Логика в решении проблем М.: Наука, 1990. -280 с.

39. Ковальский Р. Логическое программирование. // Логическое программирование. Сб. ст. М.: Мир, 1988. - С. 134-166.

40. Колмероэ А., Кануи А., ван Канегем М. Пролог теоретические основы и современное развитие. // Логическое программирование. Сб. ст. - М.: Мир, 1988. - С. 27-133.

41. Корухова Л.С., Любимский Э.3., Манжелей С.Г., Соловская Л.Б. Альтернативное немонотонное планирование при свободном взаимодействии процедурных и дедуктивных элементов. // Вопросы кибернетики (Москва). 1996. - №2. - С.238-258.

42. Коссей И.П. Четыре быстрых алгоритма в методе резолюций. //- 124

43. Известия АН СССР. Техническая кибернетика. 1982. - N5. -С.217-221.

44. Кузин Л.Т. Состояние и перспективы развития научно-технического направления "Искусственный интеллект". // Искусственный интеллект, итоги и перспективы. Материалы семинара. М.: Общество "Знание" РСФСР, 1985. - С. 4-9.

45. Кузин Л.Т., Баловнев 0. Т. Искусственный интеллект и вычислительные системы пятого поколения. // Искусственный интеллект, итоги и перспективы. Материалы семинара. М: Общество "Знание" РСФСР, 1985. - С. 24-32.

46. Левченко В.И., Савинова A.A. Управление диалогом и логический вывод в конечных предикатах. // Прикладные системы искусственного интеллекта. Вып.123. - Кишинев: "ШТИИНЦА", 1991. - С. 24-40.

47. Логический подход к искусственному интеллекту: от классической логики к логическому программированию. / Тейз А., Грибомон П. и др. М.: Мир, 1990. - 432 с.

48. Логический подход к искусственному интеллекту: от модальной логики к логике баз данных. / Тейз А., Грибомон П. и др. -М. :Мир, 1998. 494 с.

49. Ломкина Е.А. Применение метода абстракций для построения логических выводов: Дипл.работа ф-т ПМ-ПУ СПбГУ. СПб, 1999. - 92 с.

50. Лорьер Ж.-Л. Системы искусственного интеллекта. М.: Мир, 1991. - 568 с.

51. Макаплистер Дж. Искусственный интеллект и Пролог на микро ЭВМ. М.: Машиностроение, 1990. - 235 с.

52. Марселлус Д. Программирование экспертных систем на Турбо Прологе М.: Финансы и статистика, 1994. - 256 с.- 325

53. Маслов С. Ю. Обратный метод установления выводимости в классическом исчислении предикатов. // ДАН СССР. 3964. - 359, №3. - С.17-20.

54. Маслов С. Ю. Связь между тактиками обратного метода и метода резолюций. // Записки научных семинаров ЛОМИ АН СССР -3969. Т. 36. - С. 337-346.

55. Маслов С.Ю. Теория дедуктивных систем и ее применение. -М.: Радио и связь, 3985. 335 с.

56. Набебин А. А. Алгоритмы на графах и их Пролог-программы. -М. :МЭИ, 3992. 304 с.

57. Нильсон Н. Искусственный интеллект. Методы поиска решений.- М.: Мир, 3973. 270 с.

58. Нильсон Н. Принципы искусственного интеллекта. М.: Радио и связь, 3985. - 376 с.

59. Норгела С., Вайцекаускас Р. Семантическая резолюция с ограничением на переменных. // Логические аспекты информатики.- Вильнюс, 3987. С. 48-53.

60. Пантелеймонов А. Основные языки программирования искуствен-ного интеллекта. // Компьютер Пресс. Обозрение зарубежной прессы. 3993. - №9. - С. 33-38.

61. Попов Э.В. Инструментальные средства для создания экспертных систем. //Проблемы информатизации. 3993.- №3.- С. 36-42.

62. Попов 3. В. Экспертные системы состояние, проблемы, перс-пективы//Известия АН СССР. Техническая кибернетика. - 3989.- №5. С. 352-363.

63. Попов Э.В., Фридман Г. Р. Алгоритмические основы интеллектуальных роботов и искусственного интеллекта. М.: Наука, 3976. - 456 с.

64. Пхакадзе Т. М. Средства управления исполнением логических- 126 программ. Киев: Препринт АН УССР, 1987. - 20 с.

65. Робинсон Дж. Логическое программирование прошлое, настоящее и будущее. // Логическое программирование. Сб.ст. - М.: Мир, 1988. - С. 7-26.

66. Робинсон Дж. Машинно-ориентированная логика, основанная на принципе резолюции. // Кибернетический сборник. Новая серия. М.: Мир, 1970. - Вып. 7. - С. 194-218.

67. Стерлинг Л., Шапиро Э. Искусство программирования на языке Пролог. М.: Мир, 1990. - 333 с.

68. Стобо Дж. Язык программирования Пролог. М.: Радио и связь, 1993. - 368 с.

69. Стрыгин В.3. База данных с предварительной подготовкой ответов. // Известия АН. Техническая кибернетика (Россия). -1994. №. - С. 209-212.

70. Тарасов В.В., Соломатин Н.М. Развитие прикладных интеллектуальных систем: анализ основных этапов, концепций, проблем. // Системы искусственного интеллекта. Вестник МГТУ. Серия "Приборостроение". Спец.выпуск. 1994. - №1.- С. 5-14.

71. Тихонов Ю.В. Математические основы языка Пролог. // Компьютер Пресс. Обозрение зарубежной прессы. 1991. - №9. -С. 60-63.

72. Филиппович Ю.Н., Малыгин А. Г. Инструментальные средства поддержки интеллектуальных технологий и систем взаимодействия человека с ЭВМ. // Системы искусственного интеллекта.- 127

73. Вестник МГТУ. Серия "Приборостроение". Спец.выпуск. 1994.- №1. С. 105-110.

74. Храмов Ю. Е. Языки программирования искусственного интеллекта. // Журнал Д-ра Добба. 1991. - №1. - С.23-27.

75. Цуриков В. М. Состояние и перспективы развития работ по искусственному интеллекту. Зарубежный опыт. Минск: Бел НИИНТИ, 1989. - 47 с.

76. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем М. : Наука, 1983. - 360 с.

77. Чери С., Готлоб Г., Танка Л. Логическое программирование и базы данных. М.: Мир, 1992. - 352 с.

78. Чертовской В. Д. Интеллектуальные системы поддержки решений.- Минск, 1995. 93 с.

79. Чертовской В.Д., Скобликова 0. В. Пакет Пролог-программ для компьютерной поддержки решений систем управления с варьируемой структурой. / Белорус, гос. политехи, академ. Минск., 1994. - 57 с. - Деп. в ВИНИТИ N2629-B94.

80. Экспертные системы: Инструментальные средства разработки. -СПб. : Политехника, 1996. 220 с.

81. Ющенко А.С., Маслов И.В. Интеллектуальная программная система поддержки оператора манипуляционного робота. // Системы искусственного интеллекта. Вестник МГТУ. Серия "Приборостроение". Спец. выпуск. 1994. - №1. - С. 44-55.

82. Язык Пролог в пятом поколении ЭВМ: Сб.ст. М. : Мир, 1988.- 501 с.

83. Antonion Grigoris, Marray Neil V. Logical methods for computational intelligence. // Knowl.Eng.Rev. 1997. - V. 12, Ш. - P. 407-409.

84. Apt K.R., Van Emden M. H. Contribution to the theory of Lo- 128 gic Programming.//Journal ACM. V. 29, №3 - 1982.- P. 841-862.

85. Boyer R., Lusk E., McCune W., Overbeek R., Stickel M., Wos L. Set theory in first-order logic: clauses for Godel's axioms. // Journal on Automated Reasoning. V. 2, №3. -Sept. 1986. - P. 287-327.

86. Castillo 0., Mel in P. An intelligent system for research and education of non-linear dynamical systems. // 14th IMACS World Congr.Comput. and Appl.Math., Atlanta, Ga, July 11-15 1994. Atlanta (Ga), 1994. - P.82-85.

87. Chang C.L. The unit proof and the input proof in teorem proving. // Journal ACM. V.17. - 1970. - P. 698-707.

88. Chang C.L., Slagle J.R. Using Rewriting Rules for Connection Graphs to Prove Theorems. // Artificial Intelligence. -V. 2, №2. Amsterdam, 1979. - P. 159-178.

89. Chou S. A Method for the mecanical derivation of formulas in elementary geometry. // Journal on Automated Reasoning.- V. 3, №. Sept. 1987. - P. 291-300.

90. Chou S. An Introduction to Wu's method for mecanical theorem proving in geometry. //Journal on Automated Reasoning.- V. 4, №3. Sept. 1988. - P. 237-268.

91. Chou S., Schelter W. Proving geometry theorems with rewrite rules. // Journal on Automated Reasoning. V. 2, №3. -Sept. 1986. - P.253-274.

92. Coelho H., Pereira L. Automated reasoning in geometry theorem proving with Prolog. // Journal on Automated Reasoning.- V. 2, №4. Dec. 1986. - P. 329-390.

93. Console L., Portinale L., Dupre D.T. Using compiled knowledge to guide and focus abductive diagnosis. // IEEE Trans. Knowl. and Data Eng. N. Y., 1996. - 8, №5. - P. 690-706.- 129

94. Cook S.A. The complexity of theorem-proving procedures. // Proceedings Third ACM Symposium on Theory of Computing. -N. Y., 1971. P. 151-158.

95. Debray S. K., Warren D. S. Detection and optimisation of functional computation in Prolog: Proc. of the 3rd International Conf. on Logic Programming.// Lect. Notes Comp. Sci.- V. 225. 1986. - P. 490-504.

96. Dowling W., Gallier J.H. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. // Journal of Logic Programming. V. 1,№3. - 1984.- P. 267-284.

97. Eder E. Consolution and its Relation with Resolution. // Proceedings of the 12th IJCAI. 24-30 August 1991. V.1. -San Mateo (Calif), 1991. - P. 132-136.

98. FaBbender Heinz, Volger Heiko. A universal unification algorithm based on unification-driven leftmost norro-wing.//Acta cybern. 1994. - V. 11, №3. - P. 139-167.

99. Gallaire H., Lassere C. Metalevel Control for Logic Programs: Proceeding of the 3rd International Conference on Logic Programming. // Lecture Notes Comp. Sci. V.225 -1986. - P. 173-185.

100. Gallaire H., Minker J., Nicolas J. Logic and databases: A deductive approach.// ACM Computing Surveys. -1984. -16(2). P. 153-185.

101. Gallier J.H., Raatz S. H0RNL0G: a Graph-Based Interpreter for General Horn Clauses. // Journal of Logic Programming.- V.4. 1987. - P. 119-155.

102. Giordano A., SaittaL., Bergadano F., Broncadori F., De Marchi D. ENIGMA: A system that learns diagnostic knowledge.// IEEE Transactions on Knowledge and Data Engineering- 130

103. V. 5, №1. N.Y., 1993. - P. 15-28.

104. Ginchiglia F., Walsh T. Abstract Theorem Proving. // Proceeding of the llth IJCAI. 20-25 August 1989. V.l. - San Mateo (Calif), 1989. - P. 372-377.

105. HatonJ.-P., Haton M.-C. L'intelligence artificielle. -Paris: Presses universitaires de France, 1993. 127 p.

106. Henshen L., Wos L. Unit Refutation and Horn Sets. // Journal ACM. V. 21. - 1974. - P. 590-605.

107. Ishikawa Takashi, Terano Takao. Analogy by abstraction: Case retrieval and adaptation for inventive design expert systems.//Expert Syst. Appl.- 1996.- V. 10, №3-4.- P. 351-356.

108. Jones N.D., Laaser W.T. Complete Problems for Deterministic Polynomial Time. // Theor. Comp. Sei. V.3. - 1977. -P. 107-117.

109. Kahn K.M. A primitive for the control of logic programs. // International Symposium on Logic Programming. Atlantic City, 1984. - P. 242-251.

110. Kovalski R.A. Predicate logic as programming language. // Information Processing'74 (IFIP Congress 74). Amsterdam: North Holland Publishing Co., 1974. - P.569-574.

111. Kovalski R.A. A Proof Procedure Using Connection Graphs. // Journal ACM V. 22, №4. - 1975. - P. 572-595.

112. Kovalski R., Kuehner D. Linear resolution with selection function. // Artificial Intelligence. V.2 - Amsterdam, 1971. - P. 227-260.

113. Lang F.-M. PUNDIT apprend le Francais: The PRATTFALL machine-translation module. // 5th Annu. AI. Syst. Gov. Conf. Wachington, D.C., May 6-11, 1990: Proc. Los Alamitos (Calif.) etc., 1990. - P. 157-166.

114. Letz R., Schumann J., Bayeri S., Bibel W. SETHEO: A higth-performance theorem prover. // Journal on Automatic Reasoning. V.8, №2. - 1992. - P. 183-212.

115. Lopez-Suarez A., Kamel M. Reorganizing knowledge to improve performance. // IEEE Trans. Knowl. and Data Eng. N.Y., 1998. - V. 10, №1. - P. 190-191.

116. Loveland D.W. A linear format for resolution. // Proceeding of IRIA Symposium on Automatic Demonstration, Versailles, France, 1968. N. Y.: Springer, 1970. - P. 147-162.

117. Loveland D.W. A simplified format for the model elimination theorem proving procedure. // Journal ACM. V. 16. -1969. - P. 349-363.

118. Loveland D.W. Mechanical theorem proving by model elimination. // Journal ACM. V. 15. - 1968. - P. 236-251.

119. Luckham D. Refinement theorems in resolution theory. // Proceeding of IRIA Symposium on Automatic Demonstration, Versailles, France, 1968. N. Y.: Springer, 1970.1. P. 163-190.

120. Maslov S. Yu. Proof-search strategies for methods of the resolution. // Machine Intelligence. V.6. N.Y.: American Elsevier, 1971. - P. 77-90.

121. Minker I. Logic and databases. Past, present and future. //AI Mag. 1997. - 18, №3. - P. 21-47.- 132

122. Moss Ch. Cut ans paste defining the impure primitives of Prolog. // Lecture Notes Comp. Sci. - V. 225. - 1986. -P.686-694.

123. Naish L. Negation and quantifiers in NU-PROLOG: Proceeding of the 3rd International Conference on Logic Programming. // Lecture Notes Comp. Sci. V. 225. - 1986. - P. 624-636.

124. Plaisted D. A. Mecanical Theorem Proving. // Formal techniques in artificial intelligence. Studies in computer science and artificial intelligence. North Holland: Elsevier sci.publ., 1990. - P.269-320.

125. Plaisted D. A. Theorem proving with abstraction. // Artificial Intelligence. V. 16,№1. - Amsterdam, 1981. - P.47-108.

126. Przymusinska H., Przymusinski T. Semantic Issues in Deductive Databases and Logic Programs.//Formal techniques in artificial intelligence. Studies in computer science and artificial intelligence. North Holland: Elsevier sci.publ., 1990. - P.321-368.

127. Robinson J.A. Automatic deduction with hyper-resolution.// Internat. Journal of Computer Math.- VI.- 1965.- P.227-234.

128. Russel S.J. Execution architectures and compilation. // Proceeding of the 11th IJCAI. 20-25 August 1989. V.1. -San Mateo (Calif), 1989. - P. 15-20.

129. Sickel S. Formal Grammars as Models of Logic Derivations. // Proceedings IJCAI-77. 1977. - P. 544-551.

130. Slagle J.R. Automatic theorem proving with renamable and semantic resolution. //Journal ACM.- V.14.-1967.- P.687-697.

131. Tanyi E. B., Linkens D. A., Bennett S. The use of Prolog in the implementation of a Knowledge-based Environment for Modelling and Simulation (KEMS). // Trans. Inst. Meas. and- 133

132. Contr. V. 15, №. - 1993. - P. 248-259.

133. Ullman J. Implementation of logical query languages for databases. // ACM Transactions on Database Systems. V. 10, №3. - 1986. - P. 289-321.

134. Unruh A., Rosenbloom P.S. Abstraction in Problem Solving and Learning. // Proceeding of the 11th IJCAI. 20-25 August 1989. V. 1. - San Mateo (Calif), 1989. - P.681-687.

135. Van Emden M.H., Kovalski R. A. The Semantic of Predicate Logic as a Programming Language. // Journal ACM. V.23, №4. - 1976. - P. 733-742.

136. Vazak T., Potter J. Metalogical control for logic programs. // Journal on Logic Programming. V. 2, №3. - 1985. -P. 203-220.

137. Warren D., Pereira L. H., Pereira F. Prolog the language and its implementation compared with Lisp. // SIGPLAN Notices. - V. 12, №8. - 1977. - P. 109-115.

138. Wen-tsun Wu. Basic principles of mechanical theorem proving in elementary geometries. // Journal on Automated Reasoning. V. 2, №. - Sept. 1986. - P. 221-252.

139. Wos L., Carson D.F., Robinson G.A. The unit preference strategy in theorem proving. // Proc. AFIPS 1964 Fall Joint Computer Conf. V.26. - 1964. - P. 616-621.

140. Wos L., Robinson G.A., Carson D. F. Efficiencyand completeness of the set of support strategy in theorem proving. // Journal ACM. V. 12. - 1965. - P. 536-541.

141. Zhang Z. Z., Hope G. S., Malik 0. P. An expert systew for switching decisions in substations. // Autom. Contr.: Proc. 11th. Trienn. World Congr. Int. Fed. Autom. Contr., Tallin, 13-17 Aug. 1990. V.4. - Oxford etc., 1991. - P.223-228.- 134