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

• Новосельцев, Виталий Борисович
• доктор физико-математических наук
• 2006

Оглавление диссертации доктор физико-математических наук Новосельцев, Виталий Борисович

Реферат Введение

Глава 1. Логические подходы к управлению знаниями.

1.1. Подход на базе классических и интуиционистских теорий.

1.2. Модальные логики.

1.3. Дескриптивные логики.

1.4. Выводы.

Глава 2. Структурные функциональные модели.

2.1. Язык теории. Основные определения.

2.2. Нерекурсивные детерминированные С-модели.

2.3. Рекурсивные детерминированные С-модели.

2.4. Интерпретация С-модели.

2.5. Выводы.

Глава 3. Установление выводимости в РДС-модели.

3.1. Формальное исчисление. Правила вывода.

3.1.1. Исчисление SR.

3.1.2. Корректность и полнота исчисления SR.

3.2. Стратегия и алгоритм вывода в классе РДС.

3.2.1. Описание алгоритма.

3.2.2. Корректность алгоритма построения вывода.

3.2.3. Особенности введения рекурсии.

3.3. Проблемы реализации систем построения вывода.

3.4. Выводы.

Глава 4. Модальная логика и обратный метод.

4.1. Базовые понятия и соглашения.

4.1.1. Синтаксис и семантика логики КТ.

4.1.2. Мультимножества и секвенции.

4.1.3. Прямое и обратное исчисление секвенций для логики знания

4.2. Исчисление путей для логики КТ.

4.2.1. Прямое исчисление путей.

4.2.2. Обратное исчисление путей.

4.3. Анализ избыточностей и полнота КТ^*^.

4.4. Выводы.

Глава 5. Ф-упорядочение.

5.1. Определения и соглашения.

5.2. Полнота KT^w без секвенций, относящихся к >-.

5.3. Предпосылка как критерий избыточности.

5.4. Выводы.

Введение диссертации (часть автореферата) на тему «Формальная теория структурных моделей описания информационных систем и методы установления выводимости»

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

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

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

Актуальность исследования. В последние годы класс систем, позиционируемых разработчиками в качестве интеллектуальных (когнитивных), постоянно расширяется. Востребованность человека в получении интеллектуальных услуг становится все более значимой в связи с вовлечением в практику управления и анализа новых составляющих окружающего мира и необходимостью адекватного восприятия/использования этого окружения. - Для достижения указанной цели (интеллектуальной помощи), естественно, необходимо уметь моделировать и/или прогнозировать комплексное поведение компонентов анализируемой предметной области -будь то социология, климатология, медицина, органическая химия или нечто подобное. Упомянутые предметные области (ПО) обладают рядом общих свойств, среди которых важно отметить следующие: > обилие вовлеченных в модель базовых понятий; тотальное взаимовлияние этих понятий, приводящее, как правило, к NP (P-SPACE) полноте соответствующих алгоритмов; отсутствие единой (общей) теории для прикладной области, т.е. существенная необъективность при формировании модели.

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

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

Одной из важнейших проблем современных компьютерных наук (computer science) является построение инструментальных средств, максимально сокращающих объем специальных навыков, необходимых при использовании информационно-вычислительных технологий. Отметим три наиболее значимых, на наш взгляд, области, для которых «интеллектуализация» является чрезвычайно важной. По степени вовлеченности пользователей на первое место, несомненно, следует поставить «Всемирную паутину» (World wide web или WWW) с ее гигантскими информационными ресурсами и сопутствующими проблемами менеджмента данных, с быстрорастущим количеством сетевых сервисов и недостатками механизмов реализации этих служб, с необходимостью управления сложной структурой Паутины и т.д.

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

Наконец, третья из приводимых здесь областей практической деятельности относится, главным образом, к науке или инженерии. Речь идет о возможном) желании прикладного специалиста самостоятельно и за 8 короткий срок создать необходимый ему программный продукт. - Здесь одним из наиболее перспективных подходов является разработка систем с возможностями автоматического синтеза программ.

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

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

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

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

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

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

Научная новизна полученных результатов определяется следующими положениями: построена формальная теория структурных рекурсивных импликативных моделей SR, для нее показаны свойства эффективной распознаваемости и эффективной разрешимости, а также приведены варианты прикладного использования; для исчисления SR сформулирован базовый обратный алгоритм установления выводимости формул, показана корректность алгоритма и определены его сложностные характеристики; предложена бесповторная стратегия вывода, учитывающая структуру модели и естественный порядок на атрибутах; сформулирован и обоснован подход к установлению выводимости формул для систем классов КТ и КТ45 (55) (модальных логик знания и автоэпистемической логики); исследованы алгоритмические аспекты проблемы установления выводимости для предложенного подхода, на основании чего предложены строго обоснованные стратегии сокращения пространства поиска вывода, использующие Ф-упорядочение.

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

12 обоснованы и опираются на новейшие результаты в области автоматического доказательства теорем. Полученные результаты частично использовались в реальных разработках (см. [Новосельцев 1985в], [Новосельцев и Калайда 1986] и [Новосельцев, Калайда и Шагисултанов 1991]) и применяются в настоящее время в ряде аспирантских исследований, которые ведутся под руководством автора. Они также могут быть использованы для реализации и исследования экономических моделей с конкурентным взаимодействием субъектов, децентрализованных комплексов управления сложными прикладными структурами, распределенных информационных систем различного назначения.

Апробации работы. Результаты работы докладывались в профильных семинарах ВМиК МГУ, ММФ СПбГУ, ФПМиК и ММФ ТГУ, АВТФ ТПУ, а также на ряде научных форумов различного уровня, среди которых можно отметить следующие:

II Всероссийская конференция по прикладной логике - Новосибирск, ИМ СО РАН, 1988,

IX Международная школа ПП-91 «Программное обеспечение управления и ИИ» - Иркутск, ИрВЦ СО РАН, 1991,

Международная конференция «Параллельные вычисления - 91» - Киев, ИК АН Украины, 1991,

Международная конференция «Логика и семантическое программирование» - Новосибирск, ИМ СО РАН, 1992,

5th International Symp. on Applied Logic - Tallinn, 1996,

Международная конференция «Всесибирские чтения по математике и механике. Томск 1997» - Томск, ТГУ, 1997,

8th Korean-Russian International Symposium on Science and Technology -KORUS 2004, Томск, ТПУ,

8th WSEAS International Conference on APPLIED MATHEMATICS Puerto De La Cruz, Tenerife, Canary Islands, Spain, 2005,

9th Korean-Russian International Symposium on Science and Technology -KORUS 2005, Новосибирск, НГТУ.

Результаты, выносимые на защиту:

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

Эффективные обратные стратегии и алгоритмы установления выводимости формулы в теории SR.

Формальный подход к установлению выводимости формул для модальных систем классов КТ и КТ45 (SS) с использованием обратного метода. г- Строго обоснованные стратегии сокращения пространства поиска вывода в модальных системах на базе Ф-упорядочения, обеспечивающие реализацию надежных и эффективных интеллектуальных программных комплексов.

Объем и структура диссертации. Диссертация включает введение, пять глав, заключение и список литературы; общий объем составляет 207 страниц, включая иллюстрации.

Заключение диссертации по теме «Системный анализ, управление и обработка информации (по отраслям)», Новосельцев, Виталий Борисович

5.4. Выводы

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

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

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

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

Аспирантское исследование Д.СЛарионова [Ларионов 2006] по применению разработанного подхода к автоэпистемической логике S5, начатое под руководством автора настоящей диссертации, успешно завершено с практической реализацией, что также подтверждает перспективность, мощь и универсальность рассмотренной методологии.

Заключение

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

Выделенный в работе класс РДС-моделей обладает рядом привлекательных свойств:

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

2. Естественный порядок, определяемый структурой описания, позволяет осуществлять поиск решения задачи T=(A^X(,,S) локально на подсхемах, причём на каждом этапе - работе с одной подсхемой - используется информация, касающаяся только данной подсхемы. Это позволяет формировать пространство вывода только из прикладных аксиом (ФС), которые принадлежат вовлекаемым в вывод подсхемам.

3. Информация о работе на каждой подсхеме фиксируется и может использоваться в дальнейшем - обеспечивается бесповторность поиска решения («запроцедуривание»).

4. Ограничения на использование рекурсивных конструкций позволяют синтезировать алгоритмы, в которых на синтаксическом уровне предусмотрен выход из рекурсии. Завершаемость таких программ зависит только от задания семантики прикладной составляющей РДС-модели.

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

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

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

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

Диссертационное исследование определяет достаточное количество «точек роста» - новых направлений работы, которые могут оказаться полезными в областях распределенного управления, нейроинформатике, семантическом лингвистическом анализе, CASE-технологиях и так далее.

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Новосельцев В.Б. Синтез рекурсивных программ в системе СПОРА Препринт - 43. Ленинград: ИТА АН СССР «Алгоритмы небесной механики», 1985.-45 с.

2. Новосельцев В.Б. Структурные вычислительные модели // Синтез программ. - 1985. - С. 17-23.

3. Новосельцев В.Б., Калайда В.Т. Концепции построения программного окружения для решения задач оптики атмосферы // Журнал оптики атмосферы. - 1986. - №6. - С. 43-51.

4. Новосельцев В.Б. Синтез рекурсивных программ без развертки модели // Программное обеспечение ЭВМ. - 1987. - С. 54-59.

5. Zurenapel F., Novoseltsev V. Toward the automatic deductive proof of the recursive formula in special intuitional theories // Communications on Discrete Applied Systems. - 1990. - №3. - pp. 356-364.

6. Новосельцев В.Б. Некоторая формализация недетерминированных процессов // Параллельные вычисления. - 1991. - С. 37-41.

7. Новосельцев В.Б, Калайда В.Т., Шагисултанов В.Г. Разработка программного обеспечения для представления управляемых объектов в системах связи. Научно-технический отчет // ИОА СО РАН. - № К5-14/91-Гб.- Томск, 1991.-84 с.

8. Novoseltsev V. Automatic inference engine for structured model theory // Applicationes de Logique. - 1991. - № 2. - 25 c.

9. Новосельцев В.Б., Бойцов С.Н. Иерархическая модель сложной динамической системы // Рукопись деп. ВИНИТИ. - 1996. - 28 с. -№1206-В1996.

10. Novoseltsev V. Computational models and recursive program synthesis // 5th International Symposium on Applied Logic. - Tallinn, 1996. - pp. 76-82.

11. Новосельцев В.Б., Нам Ю.Б. Формализм для представления и анализа сложных информационных комплексов // III Сибирский Конгресс по прикладной и индустриальной математике. - Томск, 1998. - С. 25-30.

12. Новосельцев В.Б., Бурлуцкий В.В. Логический вывод в дедуктивных системах // Вторая сибирская школа молодого ученого: т. 3, - 2001. - С. 27-41.

13. Новосельцев В.Б., Бурлуцкий В.В. Подход к реализации вывода в различных льюисовских системах // Логика и приложения. - 2001. - С. 61-65.

14. Новосельцев В.Б., Бурлуцкий В.В. Реализация обратного метода для модальной логики КТ II Исследования по анализу и алгебре. - 2001. - С. 54-60.

15. Новосельцев В.Б., Тютерев В.В. Метод динамического наращивания узлов как способ построения нейронных сетей эффективного размера // Нейрокомпьютеры: разработка и применение. - 2001. - №2. - С. 82-88.

16. Новосельцев В.Б., Тютерев В.В. Автоматическое построение нейронных сетей методом эволюционного наращивания // Рукопись деп. ВИНИТИ, ТГУ. - 2001, № 1944-В2001.-26 с.

17. Новосельцев В.Б., Ларионов Д.С. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование, ИММ РАН: т. 14 - 2002. - №9 - С. 48-52.

18. Новосельцев В.Б., Романчук Е.А. Нечеткие множества в когнитивных системах // Труды ИСП РАН: т. 7. - 2004. - С. 55-60.

19. Новосельцев В.Б., Соколова В.В. Расширение алгебры Кодда операциями с рекурсивными объектами // Вестник ТГУ. - 2004. -№284. - С. 54-59.

20. Новосельцев В.Б., Колтун П.Н., Романчук Е.А. Возможность использования дескрипторных логик в системе управления знаниями // Вестник ТГУ. - 2004. - №284 - С. 17-22.

21. Novoseltsev V., Sokolova V. Expansion of Codd algebra by recursive definitions // Korea-Russia International Symposium on Science & Technology "KORUS 2004". - Tomsk, 2004. - pp. 54-57.

22. Новосельцев В.Б., Малахов А.В. К вопросу о синтезе параллельных алгоритмов // Вестник ТГУ. - 2004. - №284. - С. 35-39.

23. Новосельцев В.Б., Романчук Е.А. О манипулировании знаниями с использованием нечетких множеств // Оптика атмосферы и океана. -2005.-№4.-С. 867-871.

24. Novoseltsev V. Theorem proving in normal modal system of K-family // 8th International Conference on Mathematics. - Spain, 2005. - pp. 82-88.

25. Новосельцев В.Б., Аксенов C.B. Организация и использование нейронных сетей. - Томск: НТЛ, 2006. - 160 с.

26. Новосельцев В.Б. Теория структурных функциональных моделей // Сибирский математический журнал.-2006.-№5. Т. 47.-С. 1014-1030.

27. Новосельцев В.Б., Аксенов С.В. Повышение качества распознавания сцен нейронной сетью определенного вида // Известия Томского политехнического университета. - 2006. - №6. Т. 309. - С. 150-160.

28. Новосельцев В.Б., Коваленко Д.А. Стратегия установления выводимости формул в структурных функциональных моделях // Известия Томского политехнического университета. - 2006. - №6. Т. 309. - С. 112-118.

29. Новосельцев В.Б., Копаница Г.Д. Нецелеориентированная стратегия вывода формул в модальных исчислениях // Известия Томского политехнического университета. - 2006. - №6. Т. 309. - С. 11-20.

30. Новосельцев В.Б., Соколова В.В. Обработка рекурсивных данных конечными автоматами // Известия Томского политехнического университета. - 2006. - №6. Т. 309. - С. 54-58.

Список литературы диссертационного исследования доктор физико-математических наук Новосельцев, Виталий Борисович, 2006 год

1. Бабаев, Новиков и Петрушина (Бабаев И.О., Новиков Ф.А., Петрушина Т.И.)1 ! 1981. Язык Декарт входной язык системы СПОРА // Прикладнаяинформатика, вып.1. М.:«Финансы и статистика». - 1981.-С.35-73.

2. Мелихов, Бернштейн и Коровин (Мелихов А.С., Бернштейн J1.C., Коровин СЛ.)2< i 1990. Ситуационные советующие системы с нечеткой логикой. М.: Наука.-1990.-271 с.

3. Новосельцев и Бурлуцкий (Новосельцев В.Б., Бурлуцкий В.В.)i 2001. Реализация обратного метода для модальной логики КТ П Исследования по анализу и алгебре. Томск. - 2001. - С.57-66.

4. Новосельцев, Колтун и Романчук (Новосельцев В.Б., Колтун П.Н., Романчук Е.А.)зч.| 2004. Возможность использования дескрипторных логик в системе управления знаниями // Вестник ТГУ (Математика. Кибернетика. Информатика). №284. - 2004. - с. 17-22

5. Новосельцев и Ларионов (Новосельцев В.Б., Ларионов Д.С.)к-1 2002. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование. Т. 14, №9. - 2002. - С.48-52.

6. Новосельцев и Малахов (Новосельцев В.Б., Малахов А.В.)г : 2004. К вопросу о синтезе параллельных алгоритмов // Вестник ТГУ (Математика, Кибернетика, Информатика), №284. 2004. -с.35-39

7. Bachmair and Gansinger (Bachmair L. Gansinger H.)i:-. i 2000. Resolution theorem proving. Handbook of Automated reasoning, (Robinson A. And Voronkov A. - Eds). - Elsevier science and MIT Press.-2000

8. Girard, Lafont and Taylor (Girard J.-Y., Lafont Y., Taylor P.)r, * 1989. Proofs and types 1989. - Cambridge University Press

9. Hi 2 P.J.Veerkamp. Berlin: Springer Verlag, 1991.-pp.3-19.

10. Mints. Orevkov and Tammet (Mints G., Orevkov V., Tammet T.): 1996. Transfer of sequent calculus strategies to resolution for S4// Proof Theory of Modal logic. Studies in Pure and Applied logic, Kluwer Academic Publishers. 1996

11. Nievvenhuis and Rubio (Niewenhuis R., Rubio A.)2000. Paramodulation-based theorem proving. // Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000