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

□□3489731

На правах рукописи

Пннжин Алексей' Евгеньевич

АЛГОРИТМЫ ИНТЕЛЛЕКТУАЛЬНОЙ ОБРАБОТКИ ИНФОРМАЦИИ И СТРУКТУРНОГО СИНТЕЗА ПРОГРАММ

Специальность 05.13.01 - Системный анализ, управление и обработка информации (отрасль: промышленность)

2 4 ДЕК 1

Автореферат диссертации на соискание ученой степени кандидата технических наук

Томск - 2009

003489731

Работа выполнена в Томском политехническом университете

Научный руководитель - доктор физико-математических наук,

доцент

Новосельцев Виталий Борисович

Официальные оппоненты: доктор технических наук, профессор

Матросова Анжела Юрьевна

Ведущая организация - Институт вычислительной математики и

математической геофизики СО РАН, г. Новосибирск

Защита состоится «21» января 2010 г. в 15 ч. 00 м.

на заседании совета по защите докторских и кандидатских диссертаций Д 212.269.06 в Томском политехническом университете по адресу: 634034, г. Томск, ул. Советская, 84/3, Институт «Кибернетический центр».

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

Автореферат разослан «//» декабря 2009 г. Ученый секретарь совета по защите

доктор технических наук, профессор Спицын Владимир Григорьевич

докторских и кандидатских диссертаций Д 212.269.06, кандидат технических наук, доцент

Сонькин М.А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

Диссертация посвящена исследованию алгоритмов логического вывода в специальных исчислениях и синтеза программ с условиями, подпрограммами и рекурсией. Область исследования ограничена дедуктивным подходом, где программа извлекается из доказательства соответствующей теоремы. Появление первых работ в области синтеза программ на основе дедуктивного подхода приходится на 60-е гг. прошлого столетия. В работах Р. Уолдингера, Ц. Ченя, Р. Ли, 3. Манны при доказательстве теоремы использовался метод резолюций Робинсона и различные вариации, направленные на повышение его эффективности. В 70-ее годы появился язык логического программирования Пролог, который в последующие десятилетия получил широкое распространение и был использован при решении множества практических задач, в частности при построении экспертных систем. На базе Пролога появилось множество реализаций, решающих задачу синтеза программ (AutoBayes, NuPrl, Oyster и др.). Однако применяемый в Прологе метод вывода от целей к посылкам приводит к издержкам, связанным с необходимостью возврата при

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

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

Важный вклад в развитие данного направления внесли работы отечественных исследователей. В частности, идея альтернативного метода вывода от аксиом к целям, впервые высказанная Г. Генценым, получила развитие в исследованиях С. Ю. Маслова и Г. Е. Минца, где приобрела название «обратного метода». В работах А. Я. Диковского, Н. Н. Непейводы, Э. X. Тыугу предлагаются вычислительные модели, ориентированные на описание конструкций структурного программирования, и исследуются теоретические аспекты синтеза рекурсивных программ. Теория структурных функциональных моделей (С-моделей) В. Б. Новосельцева является развитием теории вычислительных моделей и содержит теоретическое доказательство возможности построения алгоритмов, обладающих свойством полноты и решающих задачу вывода за полиномиальное время.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Практическая ценность и реализация результатов работы.

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

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

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

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

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

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

а) линейная зависимость для программ с условиями и подпрограммами;

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

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

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

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

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

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

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

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

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

а также докладов на ряде научных форумов:

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

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

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

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

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

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

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

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

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

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

СОДЕРЖАНИЕ РАБОТЫ

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

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

Модель предметной области £ рассматривается как совокупность множеств (А, Р, О), представляющих собой наборы атрибутов, функциональных связей, селекторов и схем соответственно. Выделено непустое подмножество примитивных схем ЕсО.

Атрибут - характеристика объекта предметной области, связанная с некоторой схемой Т из множества /3. Если 7'е П\Е, то связь атрибута а со схемой Твыражается записью о:Ти атрибут называется непервичным. Если ТеЕ, то атрибут является примитивным (например, целое число).

Функциональная связь (ФС) - отображение множества исходных атрибутов в целевой атрибут:/ а\,..., а, —> аа.

Селектор (предикат) - условие, при котором определенное подмножество атрибутов и ФС имеет смысл.

Схема - совокупность атрибутов, ФС и селекторов. Схема Татрибута / определяется выражением вида:

1:Т=(а0:8т, а\:Бо,..., ап:Яо„

//>,(...) з «ш^ю, я, ^ц...

/><(•••) => ако'£ко< ак 1:5л• • • \f_seh епсИ/

\f_sef),

где ТеО\Е - имя схемы, 5,/еО - собственные подсхемы, а а:)еА -атрибуты схемы Г. Обозначение скрывает список ФС схемы Т. Часть определения между обозначениями ¡/...епсП/ определяет вариантную часть схемы, которая состоит из условных ветвей, разделенных символом □, и соответствует программной конструкции ¡/...еке1/...еке. Символы Р1&Р называются выбирающими селекторами и представляют собой логическую функцию вида р,(а„о,...), где а„0,... - атрибуты заголовка схемы. Следом за описанием селектора указываются условные атрибуты

<а,1|..., а следующее за ними выражениескрывает множество условных ФС. Условная ФС может включать в себя атрибуты заголовка и условные атрибуты соответствующей ей ветви. Условие р, определяет допустимость атрибутов и ФС, входящих в / ветвь. Иными словами, условные атрибуты и ФС имеют смысл только в соответствующей им ветви вариантной части схемы.

Непервичные атрибуты порождают следующие имена. Пусть t - имя

непервичного атрибута и /:Т. Пусть ай.....а„ - имена собственных

атрибутов, определенных в схеме Т. Тогда, !.ай, ..., {.а„ - также являются именами атрибутов. Атрибуты а0,...,а„ называются су б-атрибутам и по отношению к атрибуту /.

Описание предметной области поставляется в виде структурной функциональной модели (С-модель), которая представляет собой конечную совокупность схем М= (ГЬ...,Г„).

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

Кроме того, указываются некоторые дополнительные ограничения для ФС схем С-модели:

ФС содержит по крайней мере один собственный атрибут схемы; ^ в нет ФС, в которые вовлечены атрибуты из разных

вариантных ветвей схемы или из вариантных частей ее подсхемы; ^ длина любого атрибута, связанного ФС, не превышает двух. Далее, в главе рассматриваются понятия НДС- и РДС-моделей, представляющие основной предмет исследования в предлагаемой работе.

С-модель является нерекурсивной детерминированной

(НД-) С-моделью, если она удовлетворяет следующим условиям:

модель М является синтаксически замкнутой, т.е. подсхемы, встречающиеся в определении каждой схемы Т,еМ, являются элементарными либо входят в состав модели М\ ^ схемы Т\,...,Т8 являются детерминированными, т.е. не содержат вариантной части, либо вариантная часть содержит две взаимоисключающие условные ветви; ^ любая схема Т, модели М определяется через элементарные

атрибуты, либо через схемы, предшествующие Г/ в модели М. Введение рекурсивных вхождений порождает конструкции, когда атрибут, связанный с некоторой схемой, явно или посредством ряда непервичных атрибутов входит в описание этой же схемы. Вводится следующее ограничение: для каждой схемы Г/еМ рекурсивные вхождения подсхем вида С.Т1 могут появляться только в одной из альтернативных ветвей схемы Г,. С-модели, удовлетворяющие этому ограничению, а также

первым двум ограничениям НДС-моделей, называются рекурсивными детерминированными (РД-) С-модепями.

Задача планирования и синтеза 5 определяется тройкой (А0гХо,Т), где А0 и Ло - наборы имен исходных и искомых атрибутов, а Т — схема, в которой определены эти имена. Задача планирования состоит в поиске решения 5=(Л0ДоД) на базе С-модели М, а задача синтеза - в генерации программы, принимающей на вход набор А0 и возвращающей Х0.

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

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

Излагается общая логика работы и состав основных модулей программной реализации машины вывода (рис. 1).

Генерация С-модели 1для тестарования)^

Чтение файла - описания С_модели (ХМ1)_

Внутреннее представление С-модели

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

Проверка и подготовка структур данных _(компиляция)_

Выгрузка/загрузка результатов компиляции

«с

гх

Результаты компиляции

Формулировка логической теоремы

Логический вывод

Извлечение программы

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

Далее, предлагаются четыре формальных правила вывода:

1) /х>Л ^ уТверЖдаеТ) Что при выявлении достижимости

аргументов А, утверждается достижимость результата х ФС/ „х 1\Т - (Л,л : Г. | /: Л (,.х),1.А

2) -—73—:—-- - расширяет первое правило для

/,: /, — (х |...),/, -X

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

.. ] \ А-* х*] I р,А1 р

3 )-----определяет условие допустимости р атрибута

х/р

х при наличии условия допустимости р у функциональной связи/.

/,:А-*х/р,/г:А->х/~р

4) —'----- утверждает, что достижимость

х

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

Далее рассматриваются модели преобразования (компиляции) НДС-модели в структуры данных, оптимизированные для реализации перечисленных правил. Особо отмечается, что результаты компиляции не зависят от постановки задачи и нотации описания исходных данных, что позволяет использовать эти результаты повторно для различных задач планирования.

Предложенная модель данных показана на рис. 2.

Рис. 2. Модель структур данных компиляции С-модели

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

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

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

Хранение информации об условиях реализуется ассоциациями исходноеУсловие и условие объектов Атрибут и ФункциональнаяСвязь. Благодаря этим ассоциациям в совокупности со связью атрибутРезультат, перенос условия на атрибут выполняется с помощью элементарной операции копирования ссылки условие в список условияДопустимости. Проверка достижимости согласно правилу вывода (4) обеспечивается методом являетсяДопустимым класса Атрибут, определяющего наличие прямого и обратного условия с помощью простой логической операции.

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

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

Рис. 3. Модель данных подпрограммы

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

Вызов подпрограммы. ^ Вариантная часть (в виде пары ветвей условия).

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

Рис. 4. Модель данных результатов вывода

Алгоритм планирования принимает на вход описанные выше структуры данных и постановку задачи. При осуществлении доказательства используются счетчики - если при обработке очередного атрибута счетчик аргументов ФС равен нулю (т.е. достижим атрибут -результат ФС), то формируется очередной шаг доказательства. Если на ФС наложено условие, то шаг помещается в список шагов доказательства текущей подпрограммы и соответствующей ветви условия. Условие ФС добавляется в список условияДопустимости и с помощью метода являетсяДопустимым, проверяется достижимость атрибута на всех ветвях условия. При получении утвердительного ответа он помещается в список достижимыеАтрибуты шага доказательства, содержащего ветви условия.

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

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

Далее, алгоритмы расширяются возможностями планирования и синтеза программ с явной и неявной рекурсией. Представлена формальная модель доказательства в классе РДС-моделей (рис. 5).

Рис. 5. Структура РДС-модели

На диаграмме прямоугольниками изображены схемы РДС-модели. В левом верхнем углу каждой схемы отмечено ее имя и имя атрибута, порождающего рекурсивный вызов. Эллипсами отображены исходные (А0) и целевые (Х0) атрибуты согласно постановке задачи на схеме. Жирными линиями отображается последовательность ФС схемы (/\ус?)> дуга в левой части отображает условные ФС альтернативной ветви р, в правой - ФС ветви ~р. В ветви ~р содержится ряд вызывающих друг друга промежуточных подсхем (Т2...Тк-1) и, наконец, схема Тк, содержащая

обращение гх:Т\ к головной схеме Тх. Стрелками (1), (2), (3) обозначена предлагаемая последовательность этапов доказательства.

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

Второй и третий этапы вывода осуществляются на рекурсивной подсхеме и выполняются согласно принципу структурной индукции -устанавливается выводимость А0, Хо/р) (база индукции), затем, исходя из предположения, что (4:7*, /¡.у10', 11.Х0') доказуемо (гипотеза индукции), выполняется доказательство теоремы (/ьТ\, 1\-Х<>', ЛУ~р). Предлагаемый метод позволяет синтезировать программы, в которых предусмотрен выход из рекурсии по одной из ветвей условия.

Компиляция РДС-модели не требует каких-либо дополнительных действий, т.к. выявление и обработка рекурсивных вхождений выполняется на стадии вывода. Для этих целей в структуры данных доказательства добавляются новые элементы (рис. 6):

^ ссылка внешнийВызовПодпрограммы - указывает на вызов

подпрограммы, который инициирует текущий вызов; ^ свойство логического типа содержитРекурсивныйВызов объекта Условие - используется для выделения рекурсивной ветви вариантной части.

+БНеиШШВы30БПоДпр0гр£ШЫ

ВыювЛодпрогршиы

Рис. 6. Модификация модели данных для вывода на РДС-модели

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

Условие

+насвание: Строка +знак Воо1еап

+содержкгРеку|1сиБнь/йВьисв: Еоо1еаг

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

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

Алгоритмы вывода и синтеза программ в работе представлены в виде блок-схем, псевдокода и описания программной реализации на языке Java. Приведены примеры исходной спецификации в формате RDF/XML и результаты синтеза.

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

Целью расчетов, приведенных в первом параграфе главы, является математическое обоснование показателей скорости работы алгоритма относительно объема НДС-модели. Для выявления зависимости принимаются некоторые допущения:

S пусть г обозначает количество схем в модели; ^ количество ФС каждой схемы одинаково и равно s; S количество аргументов каждой ФС одинаково и равно а; S количество непервичных атрибутов в каждой схеме равно и\ S количество доставляющих ФС каждой подсхемы равно Ь; Для предельного случая, когда все ФС являются условными и в результатах планирования участвуют все подсхемы, общее время планирования определяется следующей формулой:

j>_ ¡-(J""4 s{afP'"'C + fdb + ^лФС + fl"",do" + ¡усгвстт^ + u{bfP'.nn + fmem/ny^ ^

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

fpz.<t>c_ Время получения ФС, в которую атрибут входит в качестве аргумента и уменьшение счетчика аргументов ФС;

/>и/д - время создание шага доказательства и помещение его в список; ^сл.фс _ Время Пр0верКИ наличия условия у ФС; fpoe don _ Время Пр0верКИ допустимости ФС;

получение ветви условия, соответствующей условию ФС; fp-» "_ Время добавления аргумента вызова подпрограммы; f"KK"'"- время добавления/получения вызова подпрограммы из стека.

Таким образом, в случае вывода на НДС-моделях, время работы алгоритма сохраняет линейную зависимость ог количества ПВ и выражается полиномом первой степени Г=0(г, 5, а, и, Ь)

Целью расчетов приведенных во втором параграфе является получение вида зависимости вычислительных затрат от объема данных РДС-модели. За исключением дополнительных затрат на поиск рекурсивных вхождений и построение замыканий, введение рекурсивных конструкций не ухудшает общей оценки скорости работы алгоритма, т. к. вывод на подзадачах (/:7*ь М, ЛУр) и 1\.Х0', Х0/~р) (2 и 3 этапы на рис. 5)

полностью включается в основной алгоритм поиска решения.

В параграфе рассматривается предельно сложный случай РДС-модели. Пусть п обозначает общее количество атрибутов схемы. Предположим, что п для всех схем одинаково. Так как примем л-и. Предположим, что каждая схема включает в себя вызовы всех подсхем модели. Тогда и=г и г<п. Примем г=п, следовательно и=п. С учетом принятых допущений оценка сложности алгоритма поиска рекурсивного вхождения определяется Т,южкрекугс1Ш< О (/г3).

Далее рассматривается случай, когда рекурсивное вхождение встречается в каждой схеме, опосредовано всеми подсхемами и затрагивает все ФС этих схем. При допущении, что построение замыкания требует максимального количества итераций, равного количеству доставляющих ФС каждой подсхемы (т.е. равного Ь), ), сложность алгоритма построения всех замыканий определяется Тзамыкание < О (6-и3).

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

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

На вход машины вывода подавались сгенерированные схемы с возрастающим числом ФС, связанных таким образом, чтобы обеспечить необходимость обработки всех ПВ. Генерация и вывод проводились многократно для сглаживания побочных эффектов. При создании схем с условиями, из п ФС схемы в каждую условную ветвь помещалось (п-6)/2 ФС, чтобы обеспечить затраты, близкие к максимальным согласно (*). Оценка для программ с рекурсией выполнялась на моделях, содержащих один рекурсивный вызов, опосредованный всеми подсхемами модели и требующий их двукратного прохождения для построения замыкания.

Рис. 7. Результаты экспериментальной оценки эффективности алгоритма

Из представленных результатов следует, что затраты на обработку условных ФС замедлили скорость примерно на % относительно линейного случая. Затраты на обработку подсхем увеличили время работы примерно в два раза. Для случаев планирования программ с рекурсией и построением замыкания было выполнено сглаживание побочных эффектов (выбросов) и выполнена полиномиальная и экспоненциальная аппроксимация. Анализ полученных трендов подтвердил соответствие экспериментальных результатов заявленным полиномиальным оценкам.

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

Предлагается следующий метод трансформации:

1. Множество предикатов Р представляется в виде совокупности схем С-модели:

М = (7'0)...,Т„), где Г,еМ Р,еР. (символ 'ЧУ' здесь и далее интерпретируется как «взаимно-однозначное соответствие»)

2. Переменные, входящие в предикат преобразуются в собственные элементарные атрибуты заголовка схемы:

P,{r0,...,rj) оГг(.. .,r0,.. .,rß...), t,eE, /=1.. j

3. Создается набор ФС f_set, реализующих логику предиката - поиск значений переменных и вычисление истинностных значений путем подстановки индивидных символов:

P,(r0,...,rj) <-> Т, = (...,г0.....,/>... \f_set), f_set = (...,f'nm:rn,...,rm-> rb ...)

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

4. Предикаты-факты отражают множество кортежей, удовлетворяющих соответствующей схеме, и определяют реализацию ФС, объявленных в предыдущем пункте.

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

Ро Р\,...,Р„ <-> Г0 = (..., t\.T\,..., t„:T„,...)

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

Р0 :-..., Р,(го,.. .,о)„.. Го = (..., г0„.., /•„..., t,\T, I Ую- Го->(,.Го,...,/!г/. гу-Н./>,...,/"V Г,.г0-> Го,...,/1,,-. Urj-^rj,...)

7. Функции, входящие в исходную спецификацию (если таковые допускаются) преобразуются в ФС соответствующих схем.

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

Далее, на основе предложенной методики предлагается метод адаптации разработанной машины вывода для решения ряда задач на Хорновских выражениях в традиционных логических исчислениях. Рассматривается случай С-модели без подсхем и вариантной части, состоящей из одной простой схемы М=(Т), представляющей собой множество ФС, вовлекающих только примитивные атрибуты. Переход к примитивным типам позволил задать следующие интерпретации конструкций С-моделей:

Логика высказываний (ЛВ). Каждой величине а,, ставится в соответствие высказывание А у, а функциональный символ интерпретируется как знак логического следствия. Тогда множество ФС схемы может быть представлено в виде набора Хорновских правил:

Ao<r-Ao\A...AAün_,^Ak<r-AkiA...AAhl. (1)

Задача планирования 5={А0гХо,Т), при А0 = {аь ..., а,}, Х0 = {я,+ь ..., аД, для постановки задачи проверки выполнимости набора высказываний интерпретируется как Хо<—Ао и соответствует:

Ах... А-Л/+1 (2)

Логика первого порядка (ЛПП). Используя метод обратной пропозиционализации, высказывания (1,2) приводятся к выражениям ЛПП: У2(А0(2)<-А<я(г)л...лА0п(г)1 . _ А1(2)<-Ак,(г)л....лАк„(~) (3)

Дескриптивная логика (ДЛ). Известно, что выражения ДЛ могут быть приведены к высказываниям ЛПП, если они не вовлекают в предикаты более двух переменных. Согласно правилам трансформации Хорновские правила в ДЛ записываются в виде аксиом вида: А0 с40] п ... пА0„.

Задача категоризации в ДЛ: Ац с А:1 - ? аналогичным образом трансформируется в выражение ЛПП. Все это в совокупности позволило сформулировать следующую постановку проблемы (3) в виде правил ДЛ:

Л0сЛ01П...П/40л.....АксАк, п...г\4ь,

А^) = г... А{£) ^ т Ат(г) е1... А/г) = 1.

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

Табл. 1 Форматы данных и соответствующее логическое исчисление

Машина вывода Логическое исчисление Формат данных

miniSat (sat4j) JIB Cnf

Darwin 1.4.1 ЛПП Tme

paradox2.2, iProver0.2 ЛПП Tptp-fof

Pellet ДЛ Owl-rdf

Выбор реализаций машин вывода объясняется следущими соображениями. Пакет Sat4j содержит реализацию алгоритма miniSat, показавшего максимальную скорость по итогам конкурса решения SAT-проблемы в 2006 г. Darwin, Paradox, ¡Prover - номинанты конкурса CADE ATP System Competition (CASC) 2007, проводимого в рамках ежегодной конференции по автоматизированному логическому выводу. Пакет Pellet считается одной из наиболее высокопроизводительных реализаций среди свободно распространяемых машин вывода на ДЛ.

Результаты испытаний приведены на рис. 8. Отметим, что при измерении времени работы алгоритмов на ЛПП и ДЛ учитывается время загрузки исходных данных (согласно требованиям CASC 2007), поэтому на графике (а) результаты работы предложенного алгоритма отличаются от аналогичных результатов (б) и (в).

а) б)

Рис. 8. Результаты сравнения производительности машин вывода (а - на ЛВ, б - на ЛПП, в - на ДЛ)

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

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

' В ходе исследования получены следующие результаты:

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

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

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Новосельцев В. Б., Пинжин А. Е. Реализация эффективного алгоритма синтеза линейных функциональных программ // Известия Томского политехнического университета. - Томск : изд-во ТПУ, 2008. -Т. 312.-№ 5.-С. 32-35.

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

3. Пинжин А. Е. Алгоритм синтеза программ с явной и неявной рекурсией // Известия Томского политехнического университета. - Томск : изд-во ТПУ, 2008. —Т. 313. 5. - С. 84-88.

4. Пинжин А. Е. Реализация системы логического вывода для логики первого порядка на базе структурных функциональных моделей // Материалы 9-й Всероссийской конференции молодых ученых по математическому моделированию и информационным технологиям (УМ-2008). - Кемерово, 2008. - С. 60-61;

5. Пинжин А. Е. Реализация системы логического вывода на основе структурных функциональных моделей для ряда логических исчислений // Материалы международной конференции «Программные системы: теория и приложения (Р8ТА-2009)». - Переславль-Залесский, 2009. - С. 38-44;

6. Пинжин А. Е. Построение эффективной машины логического вывода для ряда логических исчислений на основе предварительной подготовки исходных данных // Материалы международной конференции «Теоретические и прикладные вопросы современных информационных технологий (ТиПВСИТ'2009)». - Улан-Удэ, 2009. С. 363-368;

Подписано к печати 08.12.2009. Тираж 100 экз. Кол-во стр. 22. Заказ № 71-09 Бумага офсетная. Формат А-5. Печать RISO/ Отпечатано в типографии ООО «PayLIJ мбх» Лицензия Серия ПД № 12-0092 от 03,05.2001г. 634034, г. Томск, ул. Усова 7, ком. 046 тел. (3822) 56-44-54

ВВЕДЕНИЕ.

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. Согласно предложенному методу интерпретации реализованы модули конвертации исходных спецификаций, выполнено экспериментальное сравнение скорости вычислений и показана высокая эффективность разработанной машины вывода по сравнению с аналогами.

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.