Алгоритмы интеллектуальной обработки информации и структурного синтеза программ тема диссертации и автореферата по ВАК РФ 05.13.01, кандидат технических наук Пинжин, Алексей Евгеньевич

• Пинжин, Алексей Евгеньевич
• кандидат технических наук
• 2009

Оглавление диссертации кандидат технических наук Пинжин, Алексей Евгеньевич

ВВЕДЕНИЕ.

1. ФОРМАЛЬНАЯ ТЕОРИЯ.

1.1. Основные определения.

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

1.3. Постановка задачи.

Выводы к главе 1.

2. АЛГОРИТМЫ ПЛАНИРОВАНИЯ И СИНТЕЗА ПРОГРАММ.

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

2.2. Планирование и синтез в классе НДС-моделей.

2.2.1. Правила вывода.

2.2.2. Трансформация вариантной части.

2.2.3. Компиляция НДС-модели.

2.2.4. Постановка задачи и схемы алгоритмов вывода.

2.2.5. Извлечение программы из доказательства.

2.3. Планирование и синтез в классе РДС-моделей.

2.3.1. Формальная модель доказательства.

2.3.2. Подготовка данных и алгоритм вывода на РДС-модели.

2.4. Программная реализация.

Выводы к главе 2.

3. ОЦЕНКА ЭФФЕКТИВНОСТИ.

3.1. Расчет вычислительных затрат на осуществление вывода в классе С-моделей.

3.2. Получение вида зависимости вычислительных затрат от объема спецификации РДС-модели

3.3. Экспериментальные результаты.

Выводы к главе 3.

4. ИНТЕРПРЕТАЦИЯ С-МОДЕЛИ ДЛЯ РЯДА ЛОГИЧЕСКИХ ИСЧИСЛЕНИЙ.

4.1. Трансформация спецификаций языка Пролог в конструкции теории С-моделей.

4.2. Упрощенный метод интерпретации для ряда логических исчислений.

4.3. Реализация методов преобразования и экспериментальные результаты.

Выводы к главе 4.

Введение диссертации (часть автореферата) на тему «Алгоритмы интеллектуальной обработки информации и структурного синтеза программ»

В современном мире информационных технологий наблюдается постоянный рост интереса к методам интеллектуальной обработки информации. Эти тенденции определяются, с одной стороны, растущими объемами и интеграцией хранилищ данных, а с другой - постоянным ростом спроса на информационные услуги, связанные с обработкой этих данных. Указанные факторы проявляются как на уровне корпоративных информационных систем в области медицины, экономики, прогнозирования и др., так и на глобальном уровне, где одним из следствий возросших потребностей в «интеллектуализации» всемирной сети стало возникновение парадигмы Semantic Web. Основой многих современных систем интеллектуального поиска и обработки информации являются машины логического вывода, реализующие те или иные методы доказательства логических теорем. Примерами таких систем являются экспертные системы, системы поддержки принятия^ решений, интеллектуального поиска и др. Одной * из основных проблем построения машин вывода является скорость получения доказательства, которая обычно определяется как количество вычислительных операций, требуемых для обработки базы знаний заданного объема. Следует отметить, что эффективность генерации вывода также зависит от степени выразительности языка описания предметной области. Некоторые современные реализации машин вывода для логики высказываний (построенные, например, на базе табличного (tableaux) метода) в ряде случаев позволяют добиться линейных вычислительных затрат на осуществление вывода относительно объема базы знаний [33]. В то же время вывод на более выразительных моделях, описанных на языке логики предикатов, зачастую приводит к полиномиальному или даже экспоненциальному росту вычислительных затрат.

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

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

Появление первых работ в области автоматического синтеза программ на основе дедуктивного подхода приходится на 60-е гг. прошлого столетия. В работах Р. Уолдингера, Ц. Ченя, Р. Ли, 3. Манны [46^8, 62] при доказательстве теоремы использовался метод резолюций Робинсона и различные его вариации, направленные на повышение вычислительной эффективности [27, 31].

В 70-ее годы появился язык логического программирования Пролог, который в последующие два десятилетия получил широкое распространение и был использован при решении множества практических задач, в частности при построении экспертных систем. На базе Пролога появилось множество реализаций, решающих задачу синтеза программ, например AutoBayes, NuPrl, Oyster и др. [6, 39, 41]. Однако, несмотря на большие функциональные возможности, использование в Прологе стратегии вывода от целей к посылкам приводит к издержкам, связанным с необходимостью возврата при установлении недостижимости очередной подцели (так называемый «бэктрекинг») [26, 28, 40, 44]. В результате, решение сложных задач вывода и синтеза может привести к экспоненциальному росту вычислительных затрат, что значительно ограничивает использование Пролога для построения эффективных систем интеллектуальной обработки данных.

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

Важный теоретический и практический вклад в развитие данного1 направления и преодоление перечисленных проблем- внесли работы отечественных исследователей. В частности, идея альтернативного метода вывода от аксиом к целям, впервые высказанная Г. Генценым [40], получила развитие в исследованиях С. Ю. Маслова и Г. Е. Минца [7-9], где приобрела название «обратного метода». В конце 70-х гг. прошлого столетия Н. Н. Непейвода предложил формальную теорию, устанавливающую соответствие между предложениями доказательства теорем и терминами структурного программирования [12-14]. Э. X. Тыугу предложил аппарат вычислительных моделей, использование которого для синтеза ветвящихся программ и программ с подпрограммами обосновано в публикациях [10, 11, 30]. В работах А. Я. Диковского на основе теории вычислительных моделей исследованы возможности синтеза программ с рекурсией [1, 2]. Теория структурных функциональных моделей (С-моделей) В. Б. Новосельцева [17] является развитием теории вычислительных моделей и обладает теоретически доказанным свойством полноты вывода и возможностью построения алгоритмов решающих задачу вывода за полиномиальное время за счет использования внешней памяти.

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

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

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

Для достижения указанной цели в работе решаются следующие задачи:

1. Формальное определение элементов модели исходных данных и формулировка задачи логического вывода и синтеза программ на базе теории структурных функциональных моделей.

2. Определение общих принципов, требований и архитектуры машины вывода.

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

4. Разработка и программная реализация алгоритмов планирования и синтеза. программ.

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

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

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

8. Экспериментальное сравнение производительности разработанной машины вывода с существующими аналогами.

Объектом исследования является область теории искусственного интеллекта, связанная с проблемами автоматического доказательства логических теорем и синтеза программ.

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

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

Научная новизна работы заключается в следующем:

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

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

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

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

Предложенные модели данных компиляции и алгоритмы вывода были внедрены в ООО «ФлексСофт» при разработке медицинской информационной системы для обработки экспертной базы знаний Ехрег1Бос. Применение предлагаемых подходов позволило многократно повысить скорость поиска противопоказаний лекарственных препаратов и реализовать дополнительные возможности трассировки найденного решения.

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

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

Основные положения, выносимые на защиту:

1. Разработанный алгоритм вывода и синтеза программ, использующий метод динамической развертки и стратегию предварительной подготовки данных, характеризуется следующими показателями количества затрачиваемых операций относительно длины описания модели предметной области: а) линейная зависимость для программ с условиями и подпрограммами; б) полиномиальная зависимость не выше третьей степени для программ с рекурсией.

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

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

4. Результаты экспериментов подтверждают высокие показатели производительности разработанной машины вывода по сравнению с существующими аналогами.

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

Апробация работы.

Основные результаты работы представлены в виде:

3-х статей в журнале «Известия ТПУ» Томский политехнический университет, г.Томск, а также докладов на ряде научных форумов, среди которых можно отметить следующие:

IX Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (УМ-2008)» (г. Кемерово, 2830 октября 2008 г.);

Международная конференция «Программные системы: теория и приложения (Р8ТА-2009)» (г. Переславль-Залесский, ИПС РАН, 13-15 мая 2009 г.);

Международная конференция «Теоретические и прикладные вопросы современных информационных технологий (ТиПВСИТ'2009)» (г. Улан-Удэ, 20-26 июля 2009 г.)

Всего по теме диссертации опубликовано 6 работ, из них 3 статьи в журнале, входящем в перечень ВАК, 2 статьи опубликованы по материалам конференций и 1 работа опубликована в качестве тезисов доклада на конференции.

Личный вклад:

1. Формальное описание модели данных и постановки задачи построены автором на основе теории структурных функциональных моделей В. Б. Новосельцева.

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

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

4. Реализация машины вывода и экспериментальные оценки производительности выполнены лично автором.

Объём и структура работы. Диссертация состоит из введения, четырёх глав, заключения, списка источников из 62 наименований и 9 приложений. Содержит 21 рисунок и 1 таблицу.

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

Выводы к главе 4

Предложенный метод сведения конструкций теории С-моделей к выражениям языка Пролог и ряда логических исчислений обладает следующими возможностями и ограничениями:

1. Позволяет использовать разработанные алгоритмы вывода на С-моделях на Хорновских выражениях (клаузах) логики первого порядка.

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

3. Ограничивает выразительность логики первого порядка, однако обеспечивает полноту вывода.

Реализация методов трансформации позволяет использовать разработанную машину вывода для:

1. Решения задач вывода на Хорновских выражениях логики высказываний и логики первого порядка, не вовлекающих индивидные значения.

2. Решения задачи категоризации в дескриптивной логике

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

ЗАКЛЮЧЕНИЕ

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

В основу разрабатываемых методов были положены следующие базовые принципы:

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

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

3. Учитывая объем современных баз знаний, машина вывода должна использовать динамический механизм «загрузки-обработки-выгрузки» данных для снижения потребления внешней памяти.

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

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

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

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

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

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

Список литературы диссертационного исследования кандидат технических наук Пинжин, Алексей Евгеньевич, 2009 год

1. Диковский А. Я. Детерминированные вычислительные модели // Техническая кибернетика. 1984. - Т. 84. - № 5. - С. 84—105.

2. Диковский А. Я. Анализ и синтез алгоритмов над базисом функциональных зависимостей. // Оптимизация и преобразование программ, 4.1. ВЦ СОАН СССР. Новосибирск. - 1983. - С. 140-152.

3. Клини С. К. Математическая логика. М.: Мир. - 1973.

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

5. Лавров С. С. Синтез программ // Кибернетика. 1982. - № 6. - С. 11-16.

6. Ломп А. А. Структурный синтез программ с помощью системы ПРОЛОГ // Изв. АН ЭССР. Сер: Физика и математика. 1985. - № 34. - С. 125-132.

7. Маслов С. Ю. Обратный метод установления выводимости в классическом • -исчислении предикатов. // ДАН СССР. 1964. - вып.159, №1. - С. 17-20.

8. Маслов С. Ю. Стратегии в резолютивном и обратном методе // Математическая логика и автоматическое доказательство теорем. М.: Наука. - 1983. - С. 327-332.

9. Маслов С. Ю., Минц Г. Е. Теория поиска доказательств и обратный метод // Математическая логика и автоматическое доказательство теорем. М.: Наука. - 1983. - С. 291-314.

10. Ю.Минц Г. Е., Тыугу Э. X. Полнота правил структурного синтеза // Докл. АН СССР.-№4.-1982.

11. П.Минц Г. Е., Тыугу Э. X. Структурный синтез и неклассические логики. Применение методов математической логики. Таллин: 1983. - С. 52-60.

12. НепейводаН. Н. О построении правильных программ // Вопросы кибернетики. 1978. -№ 46. - С. 88-122.

13. Непейвода Н. Н. Прикладная логика. Новосибирск: НГУ. - 2000.

14. Непейвода Н. Н. Соотношение между правилами естественного вывода и операторами алгоритмических языков высокого уровня // Докл. АН СССР. — 1978, № 3-С. 526-529.

15. Новосельцев В. Б. Нерезолютивный логический вывод для пролого-подобных систем программирования. // Программирование. 2009. - № 3.

16. Новосельцев В. Б. Синтез рекурсивных программ в системах управления пакетами прикладных программ: Дис. . канд. техн. наук. Институт теоретической астрономии академии наук СССР. - Л., 1985. - 50 с.

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

18. Новосельцев В.Б. Эффективный нерезолютивный вывод для ограниченного исчисления хорновских дизъюнктов // Известия Томского политехнического университета. 2008. - Т. 312. - № 5. - С. 94-97.

19. Пинжин А. Е., Новосельцев В. Б. Эффективный алгоритм синтеза программ с условиями и подпрограммами // Известия Томского политехнического университета. 2008. - Т. 313. - № 5. - С. 77-84.

20. Рассел С., Норвиг П. Искусственный интеллект: современный подход (AIMA). 2-е изд. Вильяме. - 2007. - С. 381-384.

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

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

23. Тыугу Э. X. Концептуальное программирование. М.: Наука. - 1984.

24. Тыугу Э. X. Структурный синтез программ // Алгоритмы в современной математике и ее приложениях: Мат. Междунар. симпоз. Ургенч (Узб. ССР), 1979. - Новосибирск. - 1982. - Ч. 2. - С. 64-78;

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

26. Baader F., Calvaneze D., McGuiness D.L., Nardi D., Patel-Schneider P.F. The Description Logic Handbook: Theory, Implementation, and Applications. -Cambridge University Press, 2003. P. 154-156.

27. Baader F., Sattler U. An overview of tableau algorithms for description logics // Studia Lógica. 2000. - V. 69. - № 1. - P. 5^0.

28. Bemers-Lee Т., Hendler J., Lassila O. The Semantic Web // Scientific American Magazine. -2001. Y. 284. - № 5. - P. 34-43.

29. Borgida A. On the Relative Expressiveness of Description Logics and Predicate Logics // Artificial Intelligence. 1996. - V. 82. - P. 353-367.

30. Calvanese D., Lembo D., Lenzerini M., Rosati R. Data complexity of query answering in description logics // In Proc. of KR 2006. AAAI Press, 2006. -P. 260-270.

31. Davis M., Logemann G., Loveland D. A machine program for theorem proving // Communications of the ACM. 1962. - V. 5. - № 7. - P. 394-397.

32. Een N., Sorensson N. An extensible SAT solver // Proc. of the VI Intern. Conf. on Theory and Applications of Satisfiability Testing. S. Margherita Ligure, Italy, 2003.-P. 502-518.

33. Fischer В., Yisser E. Adding concrete syntax to a Prolog-based program synthesis system // Prelim, proc. of the International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'03), Sweden. 2003. - P. 56-58.

34. Gentzen G. Uhtersuchuagen uber das logische Schliessen // Mathematishe Zeitschrift. 1934. - V. 39. - № 2. - P. 176-210.

35. Horn C., Smaill A. Theorem proving and program synthesis with Oyster // The unified computation laboratory: Modelling, specifications, and tools. Oxford Institute Of Mathematics. - 1992.- P. 425-436.

36. Horrocks I. Description Logic: Axioms and Rules // Dagstuhl "Rule Markup Technique" workshop. February, 2002. - PP. 51.

37. ISO/IEC 13211-1:1995. Approved international standard for Prolog Part 1: General core Электронный ресурс. - 1995. - Режим доступа: http://www.iso.org/iso/isocatalogue/cataloguetc/cataloguedetail.htm7csnumber =21413.

38. Kowalski R. Predicate Logic as Programming Language // In Proceedings IFIP Congress, Stockholm, North Holland Publishing Co. 1974. - P. 569-574.

39. Reprinted in Computers for Artificial Intelligence Applications. IEEE Computer Society Press, Los Angeles. - 1986. - P. 68-73.

40. Kreitz C., Neugebauer G., Fronhofer B. Logic Oriented Program Synthesis (LOPS) goals and realization // Technical Report, TU Munchen. - 1988.

41. LeeR. С. Т., Chang C. L. Structured programming and automatic program synthesis // ACM SIGPLAN Notices. 1974. - V. 9. - № 4. - P. 60-70.

42. Lee R. С. Т., Waldinger R. J., Chang C. L. An improved program-synthesizing algorithm and its correctness // Communications of the ACM. 1974. - V. 17. -№4.-P. 211-217.

43. Manna Z., Waldinger R. The automatic synthesis of recursive programs // SIGPLAN Notice. 1977. - V. 12. - № 8. - P. 29-36.

44. RDF/XML Syntax Specification (Revised) Электронный ресурс. . W3C Recommendation 10 Feb 2004. - Режим доступа: http://www.w3.org/TR/rdf-syntax-grammar.

45. Rumbaugh J., Jacobson I., Booch G. The Unified Modeling Language Reference Manual, Second Edition. Addison-Wesley Professional. - 2004.

46. Sat4j official site Электронный ресурс. 2008. - Режим доступа: http://www.sat4j .org/

47. SAT DIMACS Challenge Satisfiability: Suggested Format Электронный ресурс. — 1993. — Режим доступа:ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/ satformat.tex.

48. SAT-Race 2006: Runtime comparison of all SAT-Race solvers Электронный ресурс. 2006. - Режим доступа: http://finv.jku.at/sat-race-2006/analysis.html

49. Sirin E., Parsia В., Grau B.C., Kalyanpur A., Katz Y. Pellet: A Practical OWL-DL Reasoner. Tech. Rep. CS 4766. - University of Maryland, College Park. - 2005.

50. The CADE ATP System Competition, part of the The 21st International Conference on Automated Deduction Электронный ресурс. -Bremen, Germany. 17-20th July 2007. - Режим доступа: http://www.cs.miami.edu/~tptp/CASC/21/.

51. The Source for Java Developers Электронный ресурс. Режим доступа: http ://j ava. sun. com.

52. TME input specification Электронный ресурс. Режим доступа: http://www.uni-koblenz.de/ag-ki/Systems/Protein/tme-syntax.txt.

53. ТРТР syntax v3.5.0 Электронный ресурс. Режим доступа: http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html.

54. Tyugu Е. Н. Towards practical synthesis of programs // In: Information Processing-80, Amsterdam: North- Holland Publ. Co. 1980. - P. 207-220.

55. Waldinger R. J., Lee R. С. T. PROW: A step toward automatic program writing // Proc. of the I Intern. Joint Conf. on Artificial Intelligence, Bedford, UK. 1969. -P. 241-253.