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

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

НОВОСЕЛЬЦЕВ Виталий Борисович

ФОРМАЛЬНАЯ ТЕОРИЯ СТРУКТУРНЫХ МОДЕЛЕЙ ОПИСАНИЯ ИНФОРМАЦИОННЫХ СИСТЕМ И МЕТОДЫ УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ

Специальность 05,13.01 - «Системный анализ, управление и обработка информации (« отраслях информатики, вычислительной техники и автоматизации)»

АВТОРЕФЕРАТ

диссертации на соискание ученой степени доктора физико-математических наук

Томск-2006

Работа выполнена на кафедре политехнического университета

Официальные оппоненты:

оптимизации систем управления Томского

ЖДАНОВ Александр Аркадьевич, доктор физико-математических наук, профессор

МАТРОСОВ А Анжела Юрьевна. доктор технических наук, профессор

ТИМЧЕНКО Сергей Викторович,

доктор физико-математических наук, профессор

Ведущая ор!аннзация: Институт математики им.С./. Соболева

Сибирского отде чеиия Российской Академии Наук

'Защита состоится «21 » декабря 2006 г. в 10— часов на юседании диссертационного совета Д212.267.12 в Томском государственном университете по адресу:

634050. Точек, пр Ленина. 36

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

Автореферат разослан « г 4 » ^ 2006 г.

Ученый секрешрь диссертационно! о совета, д. г.н.. профессор

В.И.Смагчн

К Общая характеристика диссертации , .

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

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

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

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

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

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

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

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

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

Научная новизна полученных результатов определяется следующими положениями: 4

> построена формальная теория структурных рекурсивных, импликативных моделей для нее показаны свойства эффективной распознаваемости и эффективной разрешимости, а '1гакжс приведены варианты прикладного использования; ' ' '• > '

> для исчисления ЯЛ; сформулирован базовый обратный алгоритм установления выводимости предложения, показана корректность

. алгоритма и определены его сложностные характеристики;

> предложена беепо'вторная■ стратегия'вывода,' учитывающая структуру модели и естественный порядок на атрибутах; ■ •

> сформулирован, и обоснован,^подход к- установлению выводимости формул для систем классов ЛТ и КТ45 (Л'5) (модальных логик знания и автоэпистемической);

>• исследованы алгоритмические аспекты.' проблемы установления выводимости, для предложенного подхода, на основании чего предложены строго обоснованные стратегии сокращения пространства поиска вывода, - .... . . .

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

Апробация работы. Результаты работы докладывались в профильных семинарах• ВМиКМГУ, ММФ СП6ПУ, ФПМиЮи'ММФ ТГУ* НПП «Элеси»,' АВТФ ТПУ; а также на ряде научных' форумов ^различного уровня, среди которых можно отмстить следующие;

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

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

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

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

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

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

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

> 8th International Conference on APPLIED MATHEMATICS Puerto De La Cruz,Tenerife, Spain, 2005,

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

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

1. Формальная теория структурных рекурсивных имппикатианых моде ¡ей .57? Оля описания прикладных областей

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

3. Формальный подход к установлению выводимости формул для модальных систем классов КТ и КТ45($5) с использованием обратного метода

4. Строго обоснованные стратегии сокращения пространства поиска вывода в модальных системах класса КТ

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

2. СОДЕРЖАНИЕ ДИССЕРТАЦИИ

Во введении обоснована актуальность реализуемой тематики, определены предмет * и цели4 исследования,- приведены; содержательные формулировки сопутствующих задач, а также указаны возможные .'варианты • использования • полученных результатов: ' ' ' / : " '•" "'' !''' '"' " "

_ . • • ,. . , ' ■ •, . , ........ • ....•!.,;(

Глава 1 .,,,...'

Здесь систематизированы распространенные г. подходы и . методы; применяемые в области обработки знаний, Приведен аналитический; обзор работ из наиболее значимых (по мнению автора) разделов указан ной области, включающих, главным .образом, дедуктивные системы и' механизмы построения заключений в них. ! ' 1 ' '

. Большинство используемых в .настоящее, время-алгоритмов; поиска вывода основано,на теореме Эрбрана, которая формулирует, необходимые и, достаточные условия выводимости формулы.для.классической логики. При. использовании этой теоремы происходит, как правило, порождение большого числа избыточных дизъюнктов, 'Для< сокращения • количества этих избыточностей используются разнообразные'подходы,-Наиболее известным и' получившим широкое;; • распространение является ' метод- резолюций', предложенный Дж. Робинсоном,- Этот метод относят1 к*1 так' называемым прямым ши целеориептираванпым методам,1 используя1 его,- доказательство строятгпродвигаясь от цели к аксиомам. ' ""' '

Практически, одновременно ,с методом резолюций и независимо от Дж, Робинсона ленинградским математиком С.Ю.'Масловым был предложен обратный• метод поиска вывода - обратный- ' по • отношению V к целеориентированным. Метод Маслова дает возможность, направленно, опираясь, на внутренние, свойства доказываемой' формулы, ограничить! перебор, возникающий при непосредственном применении теоремы Эрбрана, и получить вывод цели, двигаясь «от аксиом».

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

1 Robinson J.A. On automatic deduction //Rice Univ. Studies:- '/964KS0.~Ml':'''

Глава 2

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

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

Фиксируется сигнатура. Определение 2.1. Четверку £ = (A,F,P,D), где Л, F, Р и D - не более чем счетные множества (элементарных) имен объектов, функциональных символов, селекторных символов и имен схем, соответственно, назовем сигиатурои. Считается, что выделено непустое конечное подмножество EcD имен примитивных или первичных схем".

Элементы множества Л называются именами объектов или объектами если это не приводит к двусмысленности Связь объекта а со схемой S отражается ¡аписью S(a) Если объект а связан со схемой Л и Sel., стандартная ¡анись S(aí заменяется записью а' либо просто а, когда ссылка на схему не важна или очевидна из контекста. - Истинностное значение синонимов а" и S(a) будем определять следующим образом: ci'- И, тогда и только тогда, когда «|ie.S'|r, где а 11 и Л* 11 обозначают реализации (на интерпретации I) величины и схемы соответственно.

Определение 2.2. Выражение вида

Ja i, ,«„->- с/о, (2.1)

где а„ i 0.....п - имена объектов, называется функциональной связью (ФС).

В(2.1) / »то имя ФС, а, - аргументы (г-1.....л), ап - результат ФС.

' Ты\>гу Э.Х. Решение задач на вычис.ште1ьпых моделях / ЖВМиМФ 1970 Т III

2 Фиксация множества НсгО для конкретной ПО не является статической При необходимости можно сделать доонредечение «вниз» и детачи шрокатн рассматриваемою ПО соответствующей модификацией множества Е Требование конечности множества I. при этом не нарушается

' Неформально ФС^ трактуется как возможность вычисления значения атрибута а0 по набору значений атрибутов ,..,(!„ применением реализации отображения f.

Имена объектов формируются из элементов множества А. .. .

Определение2.3; Пусть аеА, а - имя объекта, тогда я, а« и, а.а также являются г именами'--объектов, В записи вида а,и а называется' префиксом, Длина произвольного- имени' (v определяется числом! вхождений элементов множества А (с учетом повторений), из которых сформировано имя,.

Одним из базовых является понятие (непервйчной) схемы объекта: Определение 2.4., Схема 5 объекта г определяется вьфаженисм вида

. . :(fJ. pt • • (2.2)!

Pt=3Sîi(aH),..;&M(am)1JliVfllier у,--' • ■ " -где 5sD\E, re А. Для всех возможных значений* индексов 7, j, SyeD -собственные подсхемы, схемы S, ауе А - ее собственные, величины,, р,в В,'-(возможно, параметризованные) выбирающие, селекторы. В правой части (212) г называется».префиксом-схемы,- участок до. вертикальной .чертьп-заголовком,. фрагмент ,lf,..fi..- вариантной?, wo мастью*, а., остальная ■ часть -заголовка - ,постоянной • частью,- Символ- «II» заимствован, из> нотации« ; «охраняемых, команд», Дсйкстры и, • и некотором смысле;', соответствует' традиционному «elsejf».> Иероглиф////ег скрмваст'список собственных ФС схемы ÄV Считается, что > префикс ./'- может «проноситься» в. скобочный' фрагмент, так что r.(S(a),...)^,/e/r.S(a),,..)vuK/(.i>(r.a),,..), Аналогично префиксируются имена селекторов, отображений; и атрибутов ФС из набора filter. ■ ■ ' 1 ■ . " ,'Г ' ; / ......

Селекторы' на интерпретации I получают истинностные (шкальные)' значения и образуют полную систему, т.е. VIJ, Щ, 'р^&р^Л ' п Синтаксическая конструкция (2.2) на' интерпретации Ii определяет размеченное от1Юшеиие в смысле Дейкстры'; ' ' '

Определение 2,S. Пусть S(r)m(...Su(r.ay).„) — схема. Если^еЕ, то r.ii/j ~ имя величины схемы S. Если S)jsD\Б и а - имя величины;схемы Sy, то г.ац.а -, имя величины схемы S. Ниже имена величин называются атрибутами.

Определение 2.6. Пусть £ - охсма. ФС /;щ„.„а„-^ао: m filler называется , допустимой для схемы Я, если и только.если ao,qi„..,a„ - атрибуты схемы.'Я. . Схема называется синтаксически правильной, если fitter, содержит; только допустимые ФС,

В дальнейшем считается,, что ФС, содержащиеся в наборй filter схемы S, отвечают следующим требованиям:

♦ ФС содержит по крайней мере один собственный атрибут схемы; .

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

♦ длина любого атрибута, связанного ФС, не превышает двух.

Определение 2.7. Факт наличия условия р у атрибута а отмечается записью а/р, а соответствующее выражение называется y-ampu6vmoju.

Определим понятие структурной импликативной модели. Определение 2.8. Сгруктурной (С-) моделью называется конечная

совокупность схем М .....S',„), где каждая S„ t 1.....п. является

элементарной или задана в соответствие с определением 2 4.

Определение 2.9. С.-\юп.еяь М является (синтаксически) замкнутой, если и только если для каждого её элемента Л',е У схемы, встречающиеся в определении .V,, являются элементарными либо определены в описании \1.

Описывая С-модель для предметной области, мы строим специальную (прикладную) теорию, в которой можно решать различные алгоритмические проблемы. Моделируемые ПО не обязательно носят «расчетный» характер -необходимым требованием, как отмечалось выше, является реализуемость ФС. Постановка задачи в С-модели имеет непроцедурный характер, - в ней указываются лишь исходные и искомые атрибуты некоторой схемы. Определение 2.10. Задачей в С-модели М называется тройка Т (, I,;.X,„S), где An и .Vn - наборы имен, соответственно, исходных и искомых величин, a S -схема С-модели W, в которой определены эти имена.

При исследовании свойств С-моделей и алгоритмов синтеза программ в них исполыуется понятие развёртки схемы S. Оно определяется через развёртку схемы на атрибуте.

Определение 2. 11. Пусть S(r) г (...S„{a„),...\ftltet) - схема, и S„&L Разверткой схемы S на атрибуте а,, называется выражение, получающееся в результате (а) подстановки в заголовок S на место Л'„(а,,) заголовка схемы S,, и (б) присоединения к набору filter схемы S всех ФС схемы S„.

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

Определение 2.12. Под полной разверткой S С-модели понимается объект, полученный из схемы S, у которого в результате последовательности развёрток на атрибутах в заголовке остаются только атрибуты, связанные с »лементарными схемами.

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

нескольких^¿^-участков и потребовать,' чтобы единственным^видом^х пересечения было строгое вложение,

' ' При построений С-модели допускаются' возможность рекурсивных определений I схем. Ясно," что полная ' развйртка' ' рекурсивной' схемы ;Д1в определена процесс её построения не завершается.' Во. втором .параграфе показывается, что некоторые естественные ограничения позволяют выделить класс С-моделей„.допускающий: рекурсивные схемы, в котором проблема доказательства эффективно решается, т.е. полная развертка схемы' не требуется; Выделенный подкласс 'вкладывается':'»' 'канонический класс детерминированных 'моделей Дйковского1,'' но 'является существенно более привлекательным,, чем' родительский,' в • смысле 'алгоритмических, характеристик; • " ''■''•' • ' "'•''

Определение 2.13. Схему 5. вида (2.2) называют детерминированной, .если она не- содержит вариантной" части либо ей вариантная часть имеет двухальтернативную форму ¡/ р г>... ; .../I.

Здесь .и ниже,, если не оговаривается!.противное, полагают,, что совокупность схем, составляющих С-модель, является упорядоченной,,., . Определение 2И4. С-модель называется^ нерекурсивной

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

♦ " Л7-синтаксически замкнута;'- ' ' '' '' "'' __ ''''/'" '

Я,', детерминирршшыё схемы;'; ' ' "■, ',

♦ любая схема ^/ модели определяется только через элементарные схемы. либо через схемы, которые предшествуют % в модели Л/,''

Определение 2. ¡5. Детерминированная., схема,!, у > которой I для - любых. двух ФС, совпадающих, по правой части (результату), аргументы принадлежат разным альтернативным ветвям^называется строго детерминированной.

Теорема 2.1. подтверждает включение класса НДС в класс Дйковского. Теорема 2.1. Полная развёртка любой схемы ^'НДС-модели Л/ определяет модель Дйковского; если М составлена только, из строго детерминированных

схем.". л ■ I ... . .. . .■ . .•.,-.'

Замечание. А .Я. Диковским показано; что при выборе семантики, в которой не , используется, внешняя ' управляющая память для ;.задания условий , в детерминированных уравнениях, проблема, синтеза в Д-вычислнтельиых моделях является /У/'-полной. В НДС-моделях алгоритмы, решающие проблему синтеза, обладают полиномиальными, характеристиками. Теорема

1 Дикавский А.Я. Детерминированные вычислительные модели // Техническая кибернетика, - ¡984. - Т.ЗЗ.-М5,- С. 68-74.

2.1 выделяет в классе моделей Диковского «хороший» в алгоритмическом плане подкласс моделей.

В третьем параграфе вводится понятие рекурсивных детерминированных (РД) С-моделей и доказывается свойство эффективной распознаваемости. Определение 2.16. С-модель Л/ (Л',, ,Л'Ш) называется рекурсивной детерминированной (РДС) моделью, если выполнены следующие требования:

1) М — синтаксически замкнута;

2) Л',, ...V,,- детерминированные схемы;

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

Конструктивность определения 2.16 обеспечивается теоремой. Теорема 2.2. Принадлежность С-модели М ,Л',М) классу РДС устанавливается конструктивно ¡а конечное время, пропорциональное ()(\\1\*)~С > т4.

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

Определение 2.17. Если в развертке схемы имеется фрагмент

.. // а.р г> ...// а.р.с/ з....//.. Д то а.[3.<? и дополнительное условие а.р.-д называются более сильными условиями по сравнению с а.р. тгот факт отмечается ыписью и.[1 I/ [> а.р (символ «-» используется как шак принадлежности имени дополняющего селектора, а не обозначение операции). Если (ЗеЛ, го а.р.с/ и га.р.-(/ называются непосредственно более сильными условиями, чем а.р, записывается '»то в форме а.р с/ ► а.р.

Определение 2.18. Пусть имеется рекурсивная схема .9. Рассмотрим фрагмент ее развёртки: (....'V,,(«,,)...'/...а.У„(а,,)...//...). Атрибут аа,, будем называть следующим за а„ и обозначать его п'.Дс/,,), где А - длина префикса а.

Введённые, отношения существенно используются при построении и анализе алгоритмов установления выводимости! " ''

Наконец, в заключительном параграф "фиксируются щ обсуждаются понятия интерпретации С-модсли, принадлежности» кортежа' типу и предложения вычислимости, ' ' ' ■ • •

Определение 2.19,Интерпретация I С-модели М задаВт:

♦ . для каждой схемы Л'е С непустое множество (первичный тип) 51 г;

♦ ' для каждого/бЕ-отображение Л|:5,1||Х,.,х5я||-+-Soli j .

♦ для каждого /збР - булевское отображение /^It^'i|iX, . .xS,,)^ {//, J1),

Определение2.20. Рассмотрим M*(...S,..),. Пусть.. A**{aofpeo,...ta,/ptm} -

множество; , атрибутов», -развертки!! S, ■<?t!^f:bi/p/a„;.,bic/ptlil-*bi/ph(i" "'— функциональная связь этой же развЁртки ((У/?«бЛ, /"О;,,„А), а г — некоторый''

кортеж, определяемый заголовком,схемы S, Говорят, что ф|| .имеет смысл-для кортежа г, если ры\\°И, /»0,Кортеж./' принадлежит,-тип^ если на г выполнены • все.функциональные соотношения,1 которых'"ймеют;'смысл для' него. ■

Определение 2,21. Выражение вида.УГ :А->Х, где (программный) терм в. сигнатуре 2, построенный по правилам, приведенным, в третьей главе, А и Л* - непустые наборы ^-атрибутов, называется г предложением, вычислимости (ПВ), Наборы А. и X называются аргументами» и результатами ПВ ■ соответственно; .... ,

Для определенного-выше понятия, нарушается ¡классическая трактовка , функциональности, однако традиционные: приемы* («ПВ есть объединение ФС, таких что,..») позволяют не выходить за рамки классики.

Глава 3 ''■'.■ ' ' ■ ■ ^

В главе описывается . исчисление, в рамках...которого: осуществляется, построение программного терма-решения для задачи»Г'ЧЛо.ЛЪ,5), .когда 5 является схемой РДС:модели. Показывается полнота и непротиворечивость теории; .Предлагаются нецелеориентированные (обратные) стратегия и алгоритм решения задачиТ, для алгоритма исследуется вопрос корректности, и устанавливаются сложностные оценки',. •

В рамках построенного исчисления, исходя из описания задачи 7, формулируется и доказывается георема (существования) 5r-w(3/r) /•/0—>VU, после чего из доказательства извлекается программный терм-решение F.

Определение 3.1. Пусть M~(...S...) - РДС-модель, пусть также .....а„!р„.

X\íq\,...jcJqm - v-атрибуты развертки S, 4,J~F:iil/p¡,--;d„/p„-^x,/ql,...,xJc)m -предложение вычислимости, а /• - кортеж, определяемый заголовком развертки при некоторой интерпретации I. Говорят, что f |, имеет смысл для кортежа >. если р\у=И, i I.....п и - I____,т.

Определение 3.2. Говорят, что ПВ 4'^/oí—>,V удовлетворяет схеме S, если при любой интерпретации 1 тип .V]i не содержит двух кортежей, для которых " Р[i имеет смысл, таких что их компоненты совпадают для всех атрибутов множества .1, но не совпадают по крайней мере для одного атрибута множества .V. При этом для произвольного кортежа г, который принадлежит отношению 5]|, результатом применения /,_]| к компонентам г. именованным атрибутами множества 4, является набор компонент, именованных атрибутами множества .V. Все ФС схемы удовлетворяют ей по определению.

В теории имеется три сорта термов, которые строятся в сигнатуре S согласно следующему определению.

Определение 3.3. (1) Термы первого сорта («-термы) представляют собой упорядоченные списки атрибутов (атрибуты понимаются в смысле второй главы). Они порождаются элементами А. (2) Термы второго сорта (у-гермы) строятся из термов первого сорта и предикатных символов из Р согласно следующей рекурсивной процедуре. Пусть р - селектор, реализуемый п-местной булевской функцией, /?еР; -í - п- хлементныи терм первого сорта, такой, что его /-Й атрибут связан с той же схемой, что и /-й аргумент р: !' и О

- термы второго сорта; а - некоторый атрибут; «-» и «&» - символы операций дополнения и конкатенации (конъюнкции), соответственно. Тогда перечисленные выражения являются термами второго сорта: а.р(А). -Р, P&Q. Других термов второго copra нет. (3) Наконец, термы третьего сорта (программные) строятся из термов всех сортов по следующим правилам. Пусть Р - герм второго сорта; /, g, И - функциональные символы (элементы множества F); FF2, F¡ термы третьего сорта и имеется вхождение # в F,; а

- некоторый атрибут; F}[fvg} - обозначение замены вхождения g на h в терме F-\. Тогда а.Л:...—>... - терм третьего сорта; F¡;FZ - терм (оператор композиции): if Р then F¡ else F2Ji - терм (оператор ветвления); h if Р then /•', else Fi\h/'g\ fi - терм (оператор рекурсии). Других термов третьего сорта нет.

В исчисление входит одна схема аксиом и четыре правила вывода. •

(0) схема аксиому НV:A>r> 4 , (Nr тождественное отображение)

(1) \~F,:A->X\Z • (правило сужения) ■'■■'•• 4 . . • ■ •

\-F:A-yX , ... ....... . , . .. , .

(2У F;A~>X,Z/P.' \-f:Z^x/p (правило суперпозиции)'

ьЕфА,г/р-*хЛх/р&р ' ' .:::

здесь Л - конъюнкция условий достижимости атрибутов из Z, а р - условие допустимости х^тпомтм, что условие достижимости - это'условие,' при котором в процессе построения доказательства обеспечивается достижимость некоторого атрибута^ а условие допустимости — это' условие?» при> котором атрибут имеет смысл в РДС-модели),; t, . •■■•,: .*••• ..м- ! .

(3) ^~Fi:A->X,x/Q&p \-Fi:A->X,x/Q&~p i '-(правило ветвления)" ■

Hfpthen Fx else FtJl:A^X,x/Q' • ' •

(4) bFi.'A-^XtX/Q&P' ' (премило введенияr

h FvA->X,x/Q&-p / рекурсии)'

■ Itfl/pthen'F\elseFi\h/gi\,^h/gi]/l:A-*X/Q,.

здесь X/P^x\/f',...rxJP, nka - символ введённого выше отношения порядка.

Схемааксиом позволяет формировать «начальные»' 'для-'вывода ПВ предложения' вычислимости, отталкиваясь от- заданных атрибутов* из1 формулировки задачи -7YПравило сужения () )'применяется, если необходимо исключить из; рассмотрения часта атрибутов; 'достижимость' которьтх доказана,*например, при использовании правила (4).' v ' '

Правило суперпозиции (композиции) (2) ¡понимается'как обычно: ссли> показана достижимость Zи известно, что по Z вычислим х, то можно считан., что показана достижимость х с учётом условий, при которых достижимы атрибуты из--ZJ Правило; ветвления-(3) позволяет ослабить условие при атрибутах: если показана^ достижимость х при '> условии Q&p (терм /м)' и одновременно при условии Q&.-p (терм то ПВ,,у которого профаммный герм построен с'помощью оператора ветвления, [обеспечивает достижимость х, с элиминированием условий р и -р. . ' ... , . .

Правило введения рекурсии (4) применимо' только для-:случая' рекурсивной схемы. Установить рекурсивные, схемы модели,, позволяет процедура, описанная в теореме 2.1 Правило означает, что^есл!! (а)дюказана. достижимость X/Q&'p по,Ajпосредством терма К,' иДб);из предположения о,, достижимости V^'aiW,...,«* следует достижимость X/Q&-P, то

достижимо X/Q (при элиминированных р и -р) посредством применения рекурсивного программного терма

h ifp then F, ehe . A -> X/Q.

Построенную теорию назовем исчис лением SR (sti uctural recursive calculi)

Далее исследуются важные свойства исчисления SR. Показывается, что правила SR для некоторой схемы РДС-модели позволяют получить все ПВ, которые удовлетворяют этой схеме (полнота исчисления) и что, исполь !уя пранила SR. можно построить только ПВ, удовлетворяющие схеме (корректность SR).

Теорема 3.1. Исчисление SR является корректным относительно понятия ПВ. удовлетворяющего схеме S.

Доказательство. Утверждение теоремы означает следующее: если ПВ >Л" выведено с помощью правил SR на основании информации об исходной схеме Л' модели XI, то, независимо от интерпретации I, для любых двух кортежей типа Л|ь гаких что Ф|| имеет для них смысл, компоненты, соответствующие атрибутам Л и .V в этих кортежах, совпадают и связаны соотношением, задаваемым Ф||. Доказательство строится конструктивно -рассматривается (произвольная) схема и все правила поочередно и показывается, что правила позволяют выводить из ПВ, удовлетворяющих исходной схеме, только те ПВ, которые также ей удовлетворяют. ■

При исследовании полноты исчисления SR необходимо показать, что если некоторое ПВ не может быть выведено из информации о схеме .V по правилам SR. то ->то ПВ не удовлетворяет схеме S. Вводится понятие замыкания набора атрибутов относительно схемы S, которое необходимо для доказательства теоремы полноты исчисления.

Определение 3.4. Пусть S(r) - r.(.l,X, ... | filter) и пусть .1 - некоторый набор атрибутов схемы S. Замыканием Л*' для ,1 относительно функциональных связей схемы 5 называют объединение всех атрибутов V таких, что ПВ /■":.-(—>.V может быть построено с использованием правил SR.

Важное свойство замыкания .1' определяется следующей леммой Лемма". ПВ Fx. J—>.Y выводимо по правилам SR. если и только если.Vс: А*.

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

Теорема 3.2. Исчисление SR является полным относительно понятия ПВ, удовлетворяющего схеме.

Во втором параграфе предлагаются и исследуются стратегии и алгоритм установления выводимости в исчислении SR. Алгоритм использует некоторую ограниченную стратегию поиска решения задачи Т ( /п .Yn S)

Входной информацией для алгоритма является, описание модели М и формулировка задачи Т! Доказательство теоремы существования заключается в> управляемом. стратегаей последовательном применении ' правил SK к аксиомам и ранее полученным утверждениям. Аксиомами выступают ФС из описания схемы модели Л7.' Поиск доказательства ведется от данных к Целям'.

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

С/,множество ^-атрибутов- исходной'схемы; достижимость которых установлена в текущий момент; '

■ по-аксиома — проблемно-ориентированная.или • предметная ¡аксиома .— ФС из (развертки) исходной схемы; ,. , ,

■ вход в подсхему,,- наличие в,. С*, у-атрибутов, которые принадлежат подсхеме текущей схемы; . ,.. ..,, .

■ Ао и 5 берутся из формулировки .задачи Г,,, ..

. Описание алгоритма*: ,„ , ■ >• , t

, «установить/pO;,C()P/Ío>>; ■ ■ ■•. • . ... .. к, «поднять §цаг"продолжать,доказательство"»;, • •«• .<-. «текущей схемой объявить S»; .> .»• •.■• ■■ • while «поднят, флаг "продолжать доказательство"» do, ..... /^«имеется ио-аксиома схемы, аргументы.которой входят в С/» then, . «применить правило (2), и, если возможно, правило (3)»; . > «переопределить См: к С) добавить новые у-атрибуты либо, изменить условия достижимости определенных ранее»; ' •'■■' «установить i»/+l»j' ..........' •"* "

• : «если определился вход в подсхему, запомнить е6»

e/síí/^«имеется подсхема, в которую определен вход»/Лея 1 '

«объявить ев текущей схемой» '

else if атекущая -- рекурсивная схема» then • «применить правило (4); установить /«»/+1»;.

«переопределить Сщ; к С, добавить новые у-атрибуты либо изменить условия достижимости определённых ранее» е/л? «объявить текущей внешнюю схему»1' "■"■ -

• .flflflv- ■■•■: ■ ' "

//(<аекущая—исходная схема 5» ««</ ■ ■'

«нет ио-аксиом, аргументы которых входят в С,») then ■' ' "

«опустит!, флаг "продолжить доказательство"»/I ■ •' " '.

od'.

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

Теорема 3.3. Приведенный алгоритм' корректно вычисляет 1п .

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

В следующем параграфе приводятся соображения по практической реализации предложенного алгоритма вывода, и устанавливается, что полный алгоритм (с включением правила введения рекурсии) иаксииагыюй теоретической оценкой имеет 0(|Л/|3), а реально является не более, чем квадратичным по длине исходного описания модели .V/.

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

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

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

Глава 4

В этой и заключительной главах обсуждаются варианты обратного метода установления выводимости для модальных теорий'. Приведенные результаты относятся к логике шания КТ, хотя исполыуемый подход был с успехом использован автором и его учениками и для других модальных теорий (см., например, [20]).

1 Фебе Р. Мооаиьная югика \1 Нахка 1974

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

Логика КТ является более богатой системой по сравнению с минимальной модальной логикой А* (за счет добавления аксиомы Т: 1) и интересна тем. что аксиома Г отвечает свойству рефлексивности бинарного отношения R структуры модальной логики. Логика КТ имеет большое шачеиие при реализации систем обработки шании. когда модальный оператор принимает трактовку «известно» (схема Т как pat и требует, чтобы то. что и-¡честно являлось истинным).

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

Реализация плана осуществляется в четыре 'папа'

I. Построение базовых исчислении для КТ - прямого секвенциального исчисления A"/',,.,, и настроенного на аналишр\ем\'ю формулу Ф обратного исчисления A'7'"lnv (в последнем случае формулами А'7* ,rv являются все подформулы исходной Ф).

II. Введение исчислений пыпей Kï'bv_vh и Kï'bw, кодирующих вывод (связывающих подформулу с примененным к ней в процессе вывода правилом) в базовых исчислениях ЛТ«,, и Л'7*",„,. соответственно.

III. Замена вывода исходной Ф формулы в КТ на опровержение отрицания Ф в A'7*V (из соображений технического удобства) с применением стратегий сокращения пространства вывода.

IV. Отображение полученного в К'Г"\? вывода в исходную систему.

Пусть Ф - формула логики КТ. Для анализа Ф удобнее исполь ювать не саму систему КТ, а эквивалентное ей исчисление секвенций КТ<Щ. Справедлива теорема1 (полноты КТЧЩ): Ф невыполнима в КТ тогда и только тогда, когда существует опровержение Ф в A'7\eq. Из упомянутой работы

1 Fitting M. !'i oof methods for modnl and mmiliotiistic /т;1<л .Svni/iewv l.ihicirv Radel Pub Lump /О« Г169

■ заимствована, и! подходящая версия 'исчисления секвенций КТ%Щ (р -пропозициональная переменная): 1 • Аксиомы'. Г, pi ~р,- • • '

Правила вывода: '

■ Г, а\ // (Л); г;л г, я (у); г,уг' (0): ,:£^L(4)( | " Г, Ал!) Г,А</В' -Hr.'O/i.A ' ' Г, I Й •

В ! рамках, обратного, метода,. поиск : опровержения' переносится ; в инверсное,исчисление)JCTfinv (формулами ЛТ"1,™ являются все подформулы исходной Ф, что и определяет, настройку-на формулу), Исчисление ■ приводится ниже:

Аксиомы:р,-р' • ' " '

' Правша вывода: • ' 1 • ' '

Г. А л (С); Д.7? (у); ' Г. 4 (л,У, . '' (а,); ! /,''" г, л r;'A;viv^;- ' пиля"' , ,г,/4лй

11Г,0а т,0а. ■ Г-,: Л- ■ •••*•••

, ,, В«- общем s

случае! неясно, - кик в A"/'''lnv находить" опровержение. Произвольной секвенции,.Для!доказательства полноты-'/Г/'1','™ доказывается лемма подсеквенциальности',:которая позволяет переносить найденное в АТКЧ опровержение Ф в исчисление К1,\т (индукцией по длине вывода Г. в KTiel]).

Лемма -.(подсеквенциальносгт/).- ПустьФ — формула КГ, Г - секвенция, состоящая .из подформул Ф и имеющая опровержение,- в ЛТ,е<1, тогда, существует-секвенция А> такая, что Ас; Г, и А имеет опровержение ь KT"\„V.

■••Л ' . I ■

Теорема 4.1 (полноты\ :KTf,„v). "Формула Ф системы КТ является невыполнимой тогда и только тогда, когда она имеет опровержение в К1фт,

Во втором параграфе в стиле А.А.Воронкова! . для заданной-формулы Ф строится; исчисление путей ATT^path f 14], Поиск вывода в этом исчислении'технически прост, а дерево вывода пустого пути представляет каркас доказательства Ф в KTKV. ' ' ,

Определение 4/. Пусть С- формула KTKV С\ и С2-ее подформулы. Путем в Ф или . Ф-путем- будем ч называть ■ любуюконечную последовательность символов л/, д„ у/, v„.".;, 0, которая удовлетворяет следующим правилам:

♦ Пустой путь (элемент) е есть Ф-путь.. .■■>■■..:, ,

♦ Пусть я.< есть Ф-путь, тогда , " • ' '

1 Voronkov A. How to optimize proof-search In modal logics; new methods ,of proving . redundancy criteria for sequent 'calculi//ACM Transactions and Computational logic '. -2001,-K I.-pp. 1-35 '

• если С имеет вид С|лС;, то ял, и ял,, есть Ф-пути (л-путь),

• если С имеет вид С| vC:, тогда яу/ и яуг есть Ф-пути (v-путь).

• если С имеет вид С|, тогда л есть Ф-путь ( -путь).

• если С имеет вид 0Ch тогда яО есть Ф-путь (0-путь).

Подформула для Ф на пути тс, обощачаемая ф|., определяется традиционно. Исчисление путей A"7'1>1,;l.h имеет вид:

Аксиомы Г, TCi, ль

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

Г, ял,. .та, (л). Г. ¡ту, Г.яуЛу). П ,л0(0). П1 . я ( ).

Г. п. я П. я Г. я Г, -

Все пути, входящие в секвенции П я,.....я, и II я, .....я„

ятяются Ф-nvmsutu

Определение 4.2. Обрамт секвенции пути или дерева вывода в Л'7"'р, h называется дерево, полученное из первоначальных (формул заменой каждого пути я на ФI.

Для доказательства полноты К7фрЛь исполыуется соответствующая Лемма {бимодетрования dm KTl\,nh). (I) Пусть D - дерево вывода в тогда образом D является дерево вывода Ф в Л'7',с,,. (2) Пусть 1У дерево

вывода секвенции в ЛТ^, и я........ - такие, что Ф I г( .(, V/ I.....п.

Тогда существует дерево Г) для Я|.....я„ в h такое, что /У является

образом дерева D. (3) Пункты (1) и (2) справедливы, если везде «дерево вывода» заменить на «опровержение».

Теорема 4.2 (пототы <>ш KTx'r.lth). Формула Ф логики AT невыполнима тогда и только тогда, когда пустой путь в имеет опровержение в Л'7'",, ,h

В третьем параграфе собраны ре!ульгаты, свяшнные с анализом избыточностей и полноты КТЬ

Определим обратное исчисление путей КТПусть Я|.....я„

Ф-пути. П я......я„. П[ ~ Я] .....я„ и Г - последовательности путей Тогда

аксиомами Л^^ являются любые формулы вида: Я|, я;, где р Ф Ui, -р-Ф |. для некоторой пропозициональной переменной р.

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

Г. it а) (л;): Г. ял, (л,): Г, яу, А, яу^ (у); Г. я, я (С);

Г,я Г,я Г, А, я Г, я

Г (<Н): П , яО (0): П . я ( )

Г,я П, я П. я

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

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

Предлагаемый в . главе механизм вывода;, является достаточно естественным и наглядным для человека и допускает контроль со -стороны прикладного эксперта или .технического специалиста. Он (механизм) также хорошо приспособлен для практических реализаций, в частности, машин, вывода в различных системах принятия решения, экспертных и других когнитивных комплексах. Естественность и наглядность становятся весьма существенными, поскольку составной частью любой КВЗпо; сложившейся традиции должна быть / мощная' подсистема, объясняющая найденные решения. . . •• ••• ' ' ' "'' 1 1 ' " ■ '■ ' " . "

Глава 5,:'.'.' ' ■

В .пятой главе-, приведены! утверждения, -описывающие алгоритмически полезные свойства,, множества всех; возможных деревьев, вывода" в исчислениях путей., Подчеркнем, что главной-.целью является ограничение пространства , поиска! /.опровержения' некоторым (собственным)' подмножеством деревьев вывода, что . достигается1 за • счет- введения специального упорядочения на множестве Ф-путей,

Сначала,рассматриваются свойства, наиболее слабо ограничивающие-пространство поиска! с помощью упорядочения. ' Классический метод резолюций упорядочивает литеры в дизъюнктах и требует, чтобы правило резолюций применялось только тогда, когда наибольшие литералы в обоих' дизъюнктах разрешимы; Введем подобные ограничения на . построение деревьев, вывода для. логической системы КТ, Преобразуем классическое упорядочивание литер на-модальный случай.. В классическом,исчислении; возможно использовать' любое упорядочение на . подформулах ,Ф, которое принимает во внимание префиксное отношение. Непосредственный перенос подобного на модальные системы невозможен, поскольку не каждое упорядочение на путях сохраняет полнотуг- Рассмотрим вывод:

-¿Д-ЛсМ-

Ы Агл/-', ЛлЛгА/0 ;

Существенно то, что любой (у)-вывбд применяется выше правила (0), потому что правило (0): не > применимо к. верхним* секвенциям; Тем1 не менее, ■ если определено ¡упорядочение на путях, 'где л^л/^, является наименьшим в .. первой посылке, то возможность применения (V) первым будет исключена, и

доказательство не будет найдено. Очевидно, что понятие Ф-упоридочения в модальных логиках является более сложным - определим его. Определение 5.1. Пути назовем братьями, если один имеет вид ял, а другой - лл„ либо xv,. и ¡iv/

Обозначения. Beide ниже символом хк üvdeu обозначать л ти v. стшоюм * - г um I симчо /ни 0 - или 0 Запись гс'Ся означает «п' есть префикс я»

Определение 5.2. Для ладанной формулы Ф назовем Ф-упорядочением

любое отношение полного порядка на множестве всех Ф-путей, удовлетворяющее условиям:

1. л,всякий раз когда

a) модальная длина я, строго больше модальной длины к2 или

b) тг, и Я; имеют одинаковую модальную длину, последний символ -

а последний символ тг: - 0 , или

c) Ttj и л; имеют одинаковую модальную длину и или

d) и л2 имеют одинаковую модальную длину, последний символ л, -w . последний символ ть - и при тгом неверны оба утверждения

и iiiCit;. но к, имеет большую обычную длину, чем г:,.

2. Не существует пути между двумя братьями, го есть не существует Ф-путей я|, jb. ttj таких, что л|>-л:~-71) и я|, - братья.

Содержательно, отношение позволяет управлять порядком

применения правил - сначала правила применяются к формулам, большим относительно >-. Помимо этого отношение гребует, чтобы (включение любого правила было меньше, чем любая его предпосылка в мультимножественном упорядочении. Условие (1а) гарантирует, что заключение меньше посылки при применении правил (0) или (0-). Условие (lb) введено для того, чтобы применение (0) или (0~) к секвенции, содержащей путь тсх^ не дало неполное исчисление. Условия (lc-d) и (2)

являются не только техническими и служат для облегчения доказательств утверждений тгого параграфа, но и однозначно определяют любые два пути по отношению к порядку ■>-, что важно в плане реализации. Обозначение. Будем испочыовать запись п, eciu Л|>-Л;; или гь

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

исчисление .КТ"^, используя" соответствующий - вариант: леммы подсеквешримышсти, •

При доказательстве полноты появляются трудности, связанные с тем, что требование упорядочения формулируется в терминах предпосылок вывода, в то время как доказательство полноты для Л^ран, использует следствия. Это несколько'осложняет введение порядка на путях. Приведем» вариант алгоритма, который упорядочивает Ф-пути.

Алгоритм; работает с секвенциями из множества путей; эти секвенции обозначаются S„ySnA>~,, >Ла, Содержательно 'запись означает, что для любого neS/ H it'eS/,; выполнено п> тс'. Пути, принадлежащие одинаковым Sh еще не, упорядочены, но будут упорядочены позднее. На каждом , шаге выбирается некоторое множество -Si в секвенции;: содержащее два или более членов и заменяетсядвумя или. более множествами SJi>-..>Srt' такими, что S/|U...uS№=S/.г. Алгоритм заканчивает' работу, когда каждое множество

содержит только один элемент.. ............. . • .

Алгоритм4? упорядочения.

/. Устанавливаем S}v как множество путей а Ф модальной длины I, 2. Для всех Si, исключая последнее, выполняем: '

■3, выбираем все пути щ,,,,,п„ взаканчивающиеся 0;

4; -разбиваем S//ki S,\{jt,, .... Яя}>-{Я1}>«.> {nail .. , .

5, разбиваем Sa'ua S0\{c} ¡-' {с}; б,- Пока существуют Si с более чем 'одним членом, выполняем: ■ 7, выбираем пщи два брата в S/ такие, что

8,- выбираем L tt R ~ множества всех префиксов 'из пул/ и пух, соответственно',:.

9. разбиваелt SiHa'Si^iLUR^fo-L^iaxji-iimi),

Когда алгоритм?■; завершается, секвенция состоит из одноэлементных множеств, при этом говорят; куп', если имеет место ...{л} > ... у {л'}..... '

' Следующая лемма гарантирует, что алгоритмудовлетворяет определению Ф-уиорядочения; ;

Лемма?. Любое упорядочение, полученное алгоритмом" на формуле Ф

является Ф-упорядочением. .! • • •

Поскольку на любом шаге алгоритма?, мы получаем Ф-упорядочение, имеет место очевидное следствие: Ф-упорядочение существует.

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

опровержений. Для дальнейшего понадобится ряд дополнительных соглашений и определении.

Обозначение. П\сть п - тчпь, Г — секвенция ттей launch .т-Г ятяемеч сокращение.» Очя \чпвержОения. что х-я' t)/я uoöorn и' us Г"

Определение 5.3. (у)-вывод в KT'"p3Ih: Г. тту, Г. тту, (v)

Г. к

будем называть относящимся к Ф-упорядочению если - Г и 7гу,--Г. Аналогично, (л)-вывод в KT®pa,h: Г. ,тл>. ллс (л)

Г. 71

будем называть относящимся к Ф-упорядочению если лл,-Г и пл,,-Г

Определение 5.4. Дерево вывода в Л'7*"Р, „ будем нгымвать относящимся к если каждый (а) и каждый (v) вывод из чтого дерева относится к Лемма (о выпаде, относящемся к >). Если Ф - невыполнимая формула и Ф-упорядочение, то существует опровержение в Л'7^",, „i, относящееся к

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

гс;. Она может быть получена в результате применения правила (v)-7Zb К Л/1 Яь д.-v^ (v) Л1. ,1;

Фактически, этот вывод является единственным, и. тем не менее, он не относится к >-. Как отмечалось выше, условия, наложенные на вывод для того, чтобы он относился к сформулированы в терминах посылок, но в таком индуктивном доказательстве мы можем расширить шключение только новым выводом. Для разрешения что и проблемы следует избавиться от секвенций путей, которые приводят к описанном ситуации, ограничиваясь секвенциями специального вида. Это так называемые —компактные секвенции путей. Они определяются следующим обра «im.

Onpede-ieime 5.5. Пусть Л|.....гс„ — пути в формуле Фи.— Ф-упорядочение

Секвенция путей Г-л,,..называется '--компактом, если для каждого i I. .,,п выполняются следующие условия: (1) если л, - л-пугь, то л,л/-Г и я,ллГ: (2) если л, - v-путь. то и я,уг,~Г.

. Используя обозначения для дизъюнкции;* конъюнкции и модальностей, переформулируем определение >~компактности следующим образом: ' Определение 5.5*.' Пусть,тспути в формуле Ф и ¡- — Ф-упорядочение, Секвенция путей' Г»Л(,..,,пП( называется ¡—компактом, если для. каждого 1т\,.,„п и для каждого »-пути я/ в Гимеем.Л/ХХ^Г, , '-■•■.

Заметим, что Л/хх^П! гарантируется Ф-упорядочением, следовательно, требование 71,хх>Г можно заменить на я^хП^/}, Следующая лемма

утверждает, что компактная секвенция Г не может привести к безвыходной ситуации, ,• •, . . ... . .-.■•'.■ г ■

Лемма (о 1—компактах). Пусть -^Ф-упорядочение; тогда (I) посылка каждого * (ЭД-вывода«есть /--компакт; (2)' есл и ' Г ~ ^--компактная; секвенция, встречающая-^ дереве въгоода;ё, то каждый (&)-вывод,'имеющий.Г своим' заключением,, относится • к' >-;■ (3)* если ' Г - >•• компактная " секвенция, встречающая в дереве вывода с;1 и если Г'содержит по крайней мере один у-путьт или;.л-путь, то, существует (>«)-вывод, все, посылки• которого -Ьткомпакты,, , • • • . ■• '■ ■.■•:.■> . ■ .

Теперь',' опираясь на эту лемму, можно доказать сформулированную выше лемму о существовании'вывода, 'относящегося к У. Лемма.; Если' Ф — невыполнимая: формула и >• - Ф-упорядочение, то существует опровержение в КТ^^. относящееся к >-,

Во ¡-.втором, параграфе приводятся■ результаты по» дальнейшему сокращению ..пространства; поиска вывода,;, Продолжается, модификация инверсного исчисления, .путей ~ с учетом полученных ранее критериев избыточности,,, \ . ,. , „#. -'■ .... ..".. ; ,, • •• Определение 5.6, Обозначим через Л"/'1*.'* [. исчисление, полученное из 'К1ФЮ удалением::. . ..,.., . , • ' •• - . •

• всех секвенций путей, содержащих.пути различной модальной'длины; ■

• всех секвенций путей содержащих противоречивую пару путей;

• всех выводов;,не относящихся к• ;, . . ■

в . кг» 1р , справедливы леммы бимоделирования , н подсеквенциальности. •■• ''■ •' "

Лемма (бимоделирования для Л'7"'"к|р), ( 1) Пусть £> - дерево вывода вЛ7ф>]|.. Тогда образ О является деревом вывода Ф в ЛГУ*",,,,,!,. (2) Пусть В' ~ дерево вывода секвенции Л|,.,.,/(„ в и К|,...,тс„ - такие пути, что Ф | тсгА, , V/

-I,...,«, Тогда существует дерево вывода О для П|,...,л„ в АГТ^рач, такое,что О' является образом формул дерева вывода £>. (3) Пункты.' (1) и (2) справедливы, если везде «дерево вывода» заменить на «опровержение».

Заметим, что исчисление КТ"[Г имеет различные правила для обработки конъюнкции. Поэтому мы модифицируем определение дерева вывода, относящегося к Ф-упорядочению следующим образом. Определение 5.7. Дерево вывода в КТФ№ называется относящимся к Ф-упорядочению, если на вывод наложены следующие условия' а) для каждого (у)-вывода Г, Д, лу,. (v)

Г, Д. к

имеет место, только если и .туг>-Г:

Ь> для каждого (л,)-вывода (соответственно, (лг)-вывода)

Г. кл, (Л,) Г. ял, (Лг) Г,д Г.п имеет место, только если 71л;>Г (па,. -Г). Лемма {подсеквенциильности дчя КТФ'^1 Р). Пусть П - опровержение ь в К7"^р, относящееся к и / - вывод в О в виде _£л .

Г

и пусть даны секвенции путей Д|.....А„ такие, что каждая Д, есть

подсеквениия Г„ тогда существует дерево вывода /З'для Д в А"/'"'*-,,* из Д|.....Д„ такое, что Д - подсеквенция Г

Лемма подсеквенциальности обобщается для произвольного дерева вывода. При этом применяется индукция по длине дерева вывода. Лемма (подсеквенциальности дчя деревьев вывода в КГ1' *,Р). Пусть О -опровержение е. в КТ" V. которое относится к О" - поддерево вывода в Г>

секвенции Г из секвенций Г|____,Г„ и Д,.....Д„ подсеквенции Г.....,Г„

соответственно Тогда существует дерево вывода О' для секвенции Д в КТ" '¡р из Д[.....Д„ такое, что А является подсеквенииеи Г.

Теперь может быть доказана теорема полноты для КТф- ")Р. Теорема 5.1 (полноты К7Ф "|(>). Формула Ф системы КТ невыполнима тогда и только тогда, когда к имеет опровержение в исчислении КТ"

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

Введем строго понятие предпосылки для прямого и обратного исчислений путей КТърх11 и АГТ^^.

Определение 5.8. Пусть П и П' - секвенции путей и секвенция П является подсеквенцией П\ В чтом случае будем говорить, что П предпосылает 1Г.

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

Правила вывода строятся в стиле /„ Вас И та!г и П.СипхШ^ег1. Для исследуемых модольных. систем вводятся необходимые понятия, доказываются вспомогательные утверждения, и теоремы полноты. Теорема 5.2 (полноты для системы {/¡ГУ^'^р}), Пусть Ф - формула КТ и- >~ есть Ф-упорядочеиие, тогда (!)• если какое-либо дерево вывода, в системе {кг1'' >-1р} успешно, то формула Ф невыполнима и • (2) если формула Ф невыполнима, то .любое справедливое дерево вывода в {КТ4"'успешно.

Теорема 5.3 (полноты для { А"/'1"' "|р} с префиксной предпосылкой), (I) Если любое дерево вывода в. системе {А'^'^р} с префиксной; предпосылкой успешно, то формула Ф логики ЛТ-невыполнима. (2) Если формула Ф логики КТ невыполнима, то любое справедливое .дерево вывода- .V в {Л'71"'^.} с префиксной предпосылкой.успешно, -

Интересным свойством префиксной предпосылки является следующее. Предположим,' что во время поиска'опровержения мы ¡ получили секвенцию пути А" П;л,л' такую, что л£я'; Рассмотрим секвенцию путей Г -

Эта секвенция префиксно-предпосылается. секвенцией ;Л, следовательно ее . можно добавить: в пространство поиска без нарушения полноты, Однако, если мы добавляем Г к-пространству поиска,' то через сокращение мы можем вывести II,я',, которое предпосылает Д, Таким образом, П;л,я'' можно заменить на более.простую секвенцию.П,л', как только устанавливается, что л.является. преф'иксом<п<.'.

Полученные результаты суммируются 'и заключительном параграфе, Необходимость сокращения пространств вывода достаточно очевидна. В общем случае, даже для ■подклассов разрешимых предложений, процедуры установления выводимости1- (особенно,", в' первопорядковых системах)' являются. N1' (Р'.чрасе),■• полными. Применение, результатов • этой' и.

1 Bachmalr. L, Gnnslnger H, Resolution theorem proving // Handbook of Automated reasoning, - Elsevier science and MIT Press. - 2000,

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

3. ЗАКЛЮЧЕНИЕ

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

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

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

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

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

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

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

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

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

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

5. ZurenapeUF., Novoseltsev. V. Toward the automatic deductive proof of the recursive formula in speciab intuitional theories // Communications on Discrete

! Applied,Systems,-1990,-№3.-pp. 356-364. • • ' • "'

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

7, Новосельцев В.Б, Калайда В.Т., Шагисултанов < В.Г. Разработка '

•"■ программного обеспечения'для .представления управляемых/объектов в

системах связи.'Научно-технический отчет // ИОА СО РАН. - № К5-14/91-Гб,-Томск,.1991:-84 с; . ' ... '

8.-. Novoseltsev V,. Automatic "inference engine .for structured model theory // Applicationes de Logique! ~ 1991. - № 2, - 25 с.

9.1 Новосельцев- В.Б.,. Бойцов . С.Н, Иерархическая модель сложной динамической ¡системы // Рукопись деп; ВИНИТИ, - 1006: - 28 с. ~ №1206:В1996,. '.г..-- . ■ . • г . . ..< "

10. Novoseltsev,.V..Gomputational"modclsand:recursive program synthesis // 5th . International Symposium on Applied Logici —Tallinn, 1996; - pp. 76-82:

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

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

27-41, ' ", -

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

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

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

'. • ° ' •/ • " ' .' И.' ''•»'•. •'• • " • • ' ' ' '"•

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

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

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

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

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

21. N'ovoseltsev V., Sokolova V. Expansión of Codd algebra bv recursive definitions H Korea-Russia International Symposium on Science & rechnologv "KORUS 2004". - Tomsk. 2004. - pp. 54-57.

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

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

24. Novoseltsev V. Theorem proving in normal modal sybtem of Л-faniily // 8lb International Conferenceon Mathematics. Spain, 2005. - pp. 82-88.

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

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

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

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

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

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

Подписано к печати 12.08.06, Формат 60x84/16, Бумага "Классика", Печать RISO. Усл^печ.л, 1;86, Уч,'-изд.л; 1,68. Заказ 989, Тираж 100 экз,

иштеаитю^тпу, 634050, г, Томск, пр, Ленина, 30,

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

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

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

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

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

1.4. Выводы.

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

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

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

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

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

2.5. Выводы.

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

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

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

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

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

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

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

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

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

3.4. Выводы.

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

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

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

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

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

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

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

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

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

4.4. Выводы.

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

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

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

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

5.4. Выводы.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5.4. Выводы

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

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

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

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

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

Заключение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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