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

Полный текст автореферата диссертации по теме "Логический анализ интеллектуальных систем с метапроцедурами"

РОССИЙСКАЯ АКАДШШ НАУК ОРДЕНА ТРУДОВОГО КРАСНОГО ЗНАМЕНИ ИНСТИТУТ имосоиш

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

КАТРЕЧКО Сергея Леонядошч "ЙЯИЧВСЯСЙИ АЕШЗ 1ИТШЕКТУАЛШЯ СИСТЕМ О ИЗТАПРОЦВДУРАШ" :

Специальность 09.00.d7 - лэгнка

АВТОРЕФЕРАТ

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

МОСКВА - 1992

Работа выполнена в секторе логика Института фыософш Академии неук Россяи

Научный руководитель : доктор философских наук, профессор В.А.Смирвов.

Офвцальные оппоненты : ■ доктор философских наук В.А.Бочаров кандидат философских наук В.М.Юалак

Веддоя оргаяюацяя: - кафедра фшооофии Калининградского государственного университета.

Защите диссертации состоится » и^а^ЛхСе 1932 г. в " /У " часов на еаседаыга специализированного оовета Д.002.29-03 оо философским наукам в Институте фююоофи РАН ш адреоу:. Москва, ул.Волюнка, 14.

С диссертацией можно ознакомиться в бя&шотеке

Иаотитута филооофиш РАН.

Автореферат, разослан " 1992 г.

Ученый секретарь шацявливнроваяэого г^веге

Л.П.Кшщэнко

/

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

Актуальность тоги. Внедрение в широкую практику электрошю-пичислитолыых систем поставило перед наукой цэлцй комплекс новых гносеологических проблем. Применение ЭВМ измоплет ' хярактер информационного взаимодействия человека и природа. Видение мира человеком становится все более и более опосредованным машиной, и это нельзя но учитывать, как нельзя отбросить влилвие микроскопа, телескопа н налагаемых имя ограничений при ииучвнии' обгектов макромира, космического пространства. Применение ЭВМ налагает свои огршшчения» свою сетку видения мира. Например, при использовании прогргаашых ■ продуктов необходимо учитывать пр!цщиппал>нуп огрешгчштооть №нвткость) ресурсов SDM. Кроме тогос 'ыарокое распространение компьвтэров • я средств их программного обеспечения поровдает новые гносеологические проблему, насущность рэаэнля которых выступает кис своеобразная "прпхтяка" для осмысления в "тосрия" паучных исследований. Тпк, непримор, появление разработок в области "искусспвеююго imrjjusisiz'' (ИИ) заставило исследователей обратиться к изучении способов йзвлеченкя и переработки информации, что привело к бураояу разштт кошлэкса computer science, .который образовался на- стеке научных дисцшшш, издавна змгкмвщяхся проблески нналвяип, - фигософия, психологии, логики и эврястикп.

Тшсгеа образом, сосрэкушбо развитее ЭВМ делает актуальным анализ ттх гносеологических ■ проблем, встащи перед compute»« eolenoe, к рдэрвботку ковш: непргацювкй исследований для рененмн этих проблем. .

В то т врекяв следует отметить, что успеха в области програчжрования во мвогом связаны с укэ накопленным теоретически?! бвгвао» решения гносеологических проблем а ■ пауках комплекса uosputer зо1®пзо. Необходимость учета'этого влияния "опыта" computer eolenoe аа "практику" прогрвияфоввния ("иекусстярниого : интеллекта") выдвигеэт задачу осмысления достияэниО теоретических дисщшййй ш5шлокс0 <jor®utep eolenoe да? далькейвегт. разнятая инВормащюшшх "орудаа* человечества.

Цйяг и агдата йасладсоагегя. Даккья раббта посзяаэпз еналгзу одной из научных, дзсциплнн сотри tar ooiesoa кзарш, noumta

- г -

ОивсОа (ТПВ)р которая исследует возшкные способы решения задач в логических ясчгапвштх. Целью исследования является ответ не вопрос: как бозлохно использование л&юуравнввих средстд От решения задач 6 логических исчислениях? Достижение этой цели осуществляется в хода решения оладувдшс задач:

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

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

- выявление возмоеинх "точек" развития ТПВ в (данном направло1ши и обоснование перспэктивносга использования для отах целей аде а глобальной обработки информации (лет,ода

А&юпереяеюяа:).

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

Степень разреботашоста теш йсаяэдованш. С одной сторона, проблематика ТПВ таено связана' с проблематикой а&ъаахтыесхого Ъонаастельшва тгорел, -м существует целый ряд исследований, посЕйденши. анализу систш автоматического доказательства теорэя, в которых в той шш иной оЗгетни оатрапшаетоя круг пробдан ОТЗ. Достаточно полный, обаор втех доследования два в работе1.

; с другой отороны, теория поиска шаода является погреиачяоЗ дисциплиной ковдшкеа оошри:4ег» во1«п»а, на стнхэ югш, евристшаз, паахологвд, п воаштв анаш> ев проблекаиа® о топаз зрэтш раакш: "родатяьезшх" наук. Условно водло вддадагь слэдузсда иапрввлеиня коадедовашЗ:

I, Акалкз с фочкн зрения понхолога? о целью вшгалвшя в моделирования псйзютгсиаскшс зйханкзмоа реввння вадач ташвэкзд. Этот аспект йсследоЕауий (раввитая) теорш покска швода шаот

1 Вораяков Яогзжэза Д.Н. Автоматическое дгкадзг-эдьопго

ггорэм //Крберяетаасв. 1966. Ш 3; 1987. й А.

Сить выродок вопросом: каковы психологические мохандона ровюкия задач человеком и как вопмокно их модааирозатше в р;м<ах ТШ)? Этот подход прэдсташпж в работах психологов2 и философов3.

2. СлокностшЯ анализ достижений ТПВ, при котором гдавню^ вопросами яплявтся следукюие: каковы слоеноспшэ. оцешси офВзктивности разик слотом доказательства теорем к накопи какболеэ зффоктишшо сродства шв¡иония нощисти исчислений? Данный подход представлен в появившейся на схшм математики» тоорш алгоритмов я .топки новой дисциплины теории сложности, проблематика которой теано связано с проблематикой ТПВ. Это пагтрзрлонн-г исслэдоззша представлено в работа?: специалистов по теории сложности4 и математической логнко5.

3. "Качественный" подscд, при котором анализируются наиболее. Ентерорлыо вдеСлко подход, реализованные при рмзитпп ТПВ. Центральным вопросом ксслодовсяия при атом является следущий: с, кассам возможные "мохшшака" решения эодач я какие из шос поддайся моделировании в лопгееских системах? Это направленно исследований (развитая) теорий поиска вывода опирается на достижения философий (гкосэологли), логики и. эвристики п моют, быть незвано логико - эвристическим или авршшчесюи подходом. К базовым работам этого подхода, пояно отнести работы российских логиков и философов О.О.СероСрякншова6, В.Л.Смирнова7, а также топора есбствекяо теория пояс.ча вывода O.D.Mac лова9. Именно

я етому направлению ЕсслэдоканнЭ относится данная работа» ;; v

2 Пушкин В.II. Эвристика- паука о творческом кася-текип. М», 1957а

3 Бртиигага E.H. Логике, >4ыяловйв, шфзрмвция» Л.» 1988.'

л Cook S.A.. Heohow П.A. C'iiв relative efiioenoy Ы propoeitionai. proof eyetet.-is. //Joumai et sbtbollo logio. 1 97 Ъ Vol.44, N.1.

5 v **

Данцян В.Я. Алгош'-?'н*а_ задач . Bumwuoivoora //Berrp. . кавериелкм. 19в7. Вып. 13"..

в CepeOpiipitioscn О.®. зрвепгюскаэ прам-рши & логячоскиэ яочлздвшя. Л.",!9Т0. '

т Йетркоэ .'i.A. ©орм&яъныЯ вызол а дапгчвежмя' аочмеявкмя. !А., 19Т2. .

в Масло» С.С. Теория дедуятийныг систем ш е® irpewentmui М.. 1986. 4 •

Т^оретичаскал и и§то®могичеокая основ» дссле^ованмя. Мо то до ло гичо ской основой исследования • является. аппарат современной теории . познания, логики, эвристики и теории сложности. Б частности, значимыми для данной работы являются категории анализа и синтеза (Папп4 Александрийский), которые существенны при рассмотрении процесса решения, задач в'ТПВ.

Теоретической основой исследования являются труда логинов н пионеров теории поиска вывода К.Эрбрана,' Г.Генцена, С.К.Юшни, Х.В.Карри, Я.Хшг?икки, Э.Бета, Р.Смальяна, Д.Правитца, С.Кангера. Д.Иойв, О.Ф.Серобряшшкова, '• В.А.Смирнова, ленинградской (петербургской). школы . математической логики Н.А:Шашша (Г.В.Давыдов, Г.Е.Минц, Г.О.Цвйтин и др.). ОсоОб необходимо отмотать работы С.Ю.Ыаслова, которые заложили концептуальную основу теории поиска вывода. .

Автор опирался таю® на. работа специалистов в области программирования, "искусственного интеллекта" и психологии НЛ£ильсона, : А.Ньюэдла, Дх.Робинсона, Ван Хао", Р.Ковальского, Д.А.Поспелова^ В.К.Финна, В.Ы.Сергеева, О.К.Тихомирова.

Новизна етссерт&цаоикого исследования. В. диссертации колучеш слодующие результаты, которые выносятся на защиту:

- введенное игегодогагичаское понятие "интеллектуальной (ловино-эбристчооной) аиспет" позволило вадышть особый тип логических исчислений - исчисления поиска бивоба, и-предложить пврсивктивнае направление "штвлшктуализацтГ логических ' исчислений структурную спзциалчэацшо вывода, ■

- введение понятий окаидптеакого н отшашеского спрообаб построения выводов,. в также "стлштзсногп'' и ■ саш1£щчесно2о,> применений правил вывода позволило оборноватг Т832С об ограниченности (швффактавности) аяалтинеакого подходе к построении вывода а необходимости йспользовйшга (ды преодоления втих ограничений) : "не-Еш&яитйчеотщх". средст! йострооякя внвода, к глторша относятся, иапрйкэр, мяэ-»вяаяиягаеоко9" пршшгашгэ правил внвода.

- предложопвдя трактовка метода поиска швода- оарахла&1 лезсОа. С.О.Павлова позволяет суцустсенно модифицировав дзк5!Е,йэтод да есчкслоиея шсквзиваюй к расе?потрать ва Оезэ 05

исчисление поиска вывода - исчисление кисел о инВвксаеи, з . котором возмокко моделирование других.известии методов поиска.

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

- предложено исчисление поиска вывода! -для исчисления, Ьысказнвашй на основе использовании тернарной логическоП связки ¡/плавной !h¡3b¡0Hjaifiu, что позволяет наметить линию развития TIB, связанную с использованием трнарних логических сьязок.

Практическая вяачшость ясследозания паЯлг-чается в том, что предотавлегашо в ней результаты могут быть использовали для ¡ подготовки спецкурсов го логике, ориентированных на компъптерное приложение, и для подготовки спецкурсов го теория поиска вывода (автоматическому доказательству теорэм). Лредложвшше исчиаяошя покска . вывода могут быть использована для модификации; ¿даствувщих и разработки оригинальных программных, средств. :

• 'Anpofletsia работы» Диссертация обсуздеиа и рекомендовано к Защите на заседании сектора логики: Института Склософин.' РЛН. ^авличшв' аспекты исследования 'излагались в докладе . на - g Всесоюзной копфзранции по логики,; методологии и философии науки ' (Иинск, 1990), в сообщениях не ааушо- исслэдовдтельсжом семинвро rio логике Института философия РАН в теоретическом семинара • кафедры логаси философского факультета МГУ ем.М. В. Ломоносова. ,

Структура двссартагцз обусловлена'.- щщ,я и спецификой псслгздсвашп. ..Работа соот ч»т из введений,.; трех глав, ешшгсенйа, двух пршгевэниа а списке литературы. Первая глава кшзт боже Концептуат :шй характер а '. посвящена обоуэданта проблем йенользеватя ттщх>ии91;х.средств винтелл&кт/идьтгх системах. Она состой ? вв трех пэрвграфов.цослэдагй ш к<агорах; разбит на две чаот,: и «а; сличения. Здесь на основе анализа нсторзш развития теории исжю ршзода'; выделены. наиболеепарСпзэтишшв. нттравлэЕэд "штеялажтуализацки* - исчислений ¿поист^ бывоОа. Вторая/ т& яродт

главы посвящены более конкретным вопросам использования метауровневых средств при решении задач. Во второй главе обсуздается вопрос использования метасредсзтв для исчисления высказываний. Здесь предложено исчисление поиска вывода на базе обратного метода С.Ю.Маслова для классического исчисления высказываний. Она состоит из небольшого вступления, где' дается краткая историческая справка создания обратного метода, и двух параграфов. В третьей главе обсуждается Еопрос об использовании мотасредств в исчислении предикатов на примере рэиения проблемы "отход Она состоит из небольшого вступления, где дается краткая историческая справка проблемы "отхода", трех параграфов к заключения. Приложение I посвящено обсуждают» проблем создания исчислений поиска вывода на базе натуральных исчислений. В . приложении 2 предложено исчисление поиска вывода Для классической логики высказываний на базе тернарной связки условной дизьшадм.

ОСНОВНОЕ СОДЕРЖАНИЕ ДИССЕРТАЦИИ

Во • введении обосновывается актуальность избранной темы. Анализ истории развития систем "искусственного интеллекта", которую можно . представить как "борьбу" тенденций "универсальности" и "конкретизации" систем ИИ, - позволяет говорить о "возрождении" тенденции "универсальности" систем ИИ в середине 80-ых годов и о начале качественно нового Стала развития * систем ИИ, связанного с появлением обучающихся сшжл, дет которого характерно широкое использование метаурошшвых средств. Выделяются два различные области применения метасрэдств: помш логические систем, $ которых получить " таоэ" шаяна в силу их полноты невозможно, и неполные ^логические сшивал». Далее анализируется специфика использования мэтоурошевнх средств в каждой из отих областей. Уточняется цель исслодовшшя, которая заключается в шашзэ использования штасредств в полные логических сиаазтв. В е^оа случае штаурочневыв средства югу? быть использованы для:

- разр ;откзг стратегии и твктшш доказательств в ж>гичеешк • исчислениях;

- управления тхэцессш построения шводв при реванш ведан о помощью ЭВМ;

В первой глава {'От исчислений и гжизллашуалъшл схюпелал") ставятся задача шработоть методологический пгпарат исследования "эвристической" компоненты логических исчислетА и, на отой основе, выявить ка-лбодао перспективные подхода повышения "эврястичноети" исчислений.

в порво« параграфа С Понятие инг.рллсн7яуальнаа сисг.елы") на oc}iod8 анализа попятил логической с истлем/ обосноиурпется нзобходимость развития "зурист-яческой" компоненты логических систем для задачи поиска (построения) вывода и формулируется задача исследования: как возможно построение вывода б логических системах? Вводится базовое моаодологичоское понятно иитэллеюпуалънсй (логшщ-звристхеаной) сис-явли, и выделяется тал •интеллекту ояьшх систем, в которых предусмотрены особыз средства для организации процесса построения вывода. - исчисления почет вывода. Формулируется, что изучение этих исчислений и составляет "предает" новой научной дисциплины - теории, поиска QuHoöa. Введенное понятие логико-эвристической _систоми сравнивается с другими подходами • к определению интеллектуальных систем и показывается его совместимость с подходами И.С.Ладенко, В.М.Сергеева, В.К.Финна.

Во пврзгрефс ("Aituiw традиционно: логических ситол")

выделяются два, сущзствешшх для теории, поиска вывода, момэнта решения 'задач- ©«Uta и 'синтез (Пвпп Александрийский). Формулируются понятия аналитического способа (способ рошэпия "снизу, вверх": от_ Формулы к аксиомам) и синтетического способа (рои та задачи "сверху вниз": от аксиом к выводимой формуле) построения выводов в логических исчислениях, что позволяет предложить классификацию логических исчислений по степени актуализации в них возможностей аналитического и синтетического подходов. Согласно этой классификации все лс-нческие системы можно разделить на "аналитические", "синтетические" и "смешанные".. Эта классификация сравнивается с ияаостнш разделением всех логических cijctöm на аксиоматические системы (система гильбврт*. JCKoro гага), системы т. .уральлого вывода v секветщалыше исчисления и показывается . "условное"' ' совпадешь "синтетических" исчислений - о аксиоматическими системшсл.

- в -

■"аналитических" исчислений - с секвенциальными системами, а "сманенных" исчислений - с системами натурального вывода. Далее обосновывается утверадеше о том, что секвенциальные исчисления л 1 системы натурального вывода представляют собой два возможных . подхода к развитию "эвристической" когсюнопта исчислений. Для т втого более подробно анализируются "полок/тельные" особенности (для целой поиска вывода) натуральных и секвенциальных исчислений • и выделяется важное направление "интеллектуализации", реализованное в этих исчислениях, - структурная специализация вывода, которая^предполагает структурное представление выводов и наложение определенных ограничений на возможную форму (структуру) выводов, что связано с изменением понятия вывода. По сравнению с стандартным понятием вывода как линейной последовательности формул в "синтетических" исчислениях, в системах натурального 'вывода формулируется понятие "субординатного" вывода, а в секвенциях понятие "дорева вывода" ("дерева поиска вывода"). Анализ особенностей логических исчислений позволили выделить -другие "положительные" особенности исчислений для поиска вывода, средикоторых можно отметить использование мощного правила ¡■подстановки в гильбертовских системах, использование вопущекхй. в 'системах натурального вавода, а такке "потенциальные" возможности структурного представлзиия вывода, ааюшчешшэ в самой парной .-логической системе- Г.Фраге. Для более точной характеристики вффвктишости использования'; правил в работе вводятся понятия "аналитического" и "не-ансилтзтского" применения правила вывода, что позволяет уточнить классификацию логических пачкалакий и наделить среди шх'"чисто Фалишчвааш" исчисления (напрщар, секвенциальные исчисления без правая т.лга езчеиня).

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

! Трати^ параграф ("Могико-эврисяичбсгаи} исчисления) посш^н

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

в первой части параграфа ("Идея глобальней обрабяыа инхрор<ацух1 в ТПВ") проводится исследование использования идеи' глобальной обработки информации в ТПВ. Для этого выделяются дао возможных направления реализации идеи глобальной обработки информации. Од'о из них связано с дальнейшим анализом структура вывода, что уже было намечено в рам<ах логических исчислений типа, систем натурального вывода и секвенциальных исчислений. Например,; при "глобальной" обработке секвенциального дерева Еывода возможно', извлечение информации о "раскеплонии" некоторой формулы,! что': позволяет не производить "расщеплонио" такой ко формулы в других, вэтвях дерева поиска. Во- вторых, возможно и более радаюлыюо; использование идеи глобальной обработки информации в. виде, построения специальных логических исчислений, болзэ полта •. учитываются* информацию (структуру) испытуемых на выводтхгл» .•, фэрмул, - исчислений поиска бнвода. Далее анализируются! конкретные системы поиска вывода, в которых идея: глобальной,;' обработки информации нашла свои реализацию. Это в основном' работы, выполненные в ленинградской (петербургской) ¿utoxus'-, математической логики Н.А.к.лшт: Н.А.Шагаш а др.9, P.D.Давыдов-0,;' Г.С.Цейтин11, П.В.Суворов12, Е.Я.Данцин13. ■'.'■ '\" \

В сЬязл о анализом-подхода Г.С.Цейтапа, обсуадвется вще оди^

сшсо* повышения эвристичности исчислений- исполь50В£3№ ______ • .'

а • ■ ) ' 1. \

Шанин H.A. и др. Алгорифм машинного поиска ' еотвотшлагого.; логического вывода в исчислении высказываний. М.;

Давыдов Г.В. Синтез метода резоладив и о^рэтнвго ..метода.: //Звлиоки научных семинаров ЛОМИ АН СССР. 1971. >\\f»V',v&

«I - . ' ' -

Цвйтин Г.С. О сложности вывода а йочиодакда вйекь^щмажк //Записки научных семинаров ЛОМИ АН ССОР«. 4969.-ОД. ЛН«' ¿Vi» Н

12 ■ v- ч '• , ■'•'V -"''"

Суворов П.Ю. О I. явдзйввагии тавтологичное' ;,ироао8йциопЬаъйм* формул //Записки научных семинаров

«а - •• v

Данщт В. Я. Две системы ТЕВтолопгшооти. оокояаинныо каагатода расцеплений //Записке сешпаро» ЛОМИ АН- СССР.::!981 Ti.1D5V^■. •x-ü.v'

.■ • . - -

. сэвствето р'отЩсяшых правил выводе- (правил типа сочешя). Диализ результатов теории сложности J существенном повышении . "мощности" : исчислений при использовании собственно- допустимых правил вывода, и уотановлеиие связи меаду понятиями "собственно допус&юэ-правило вывода" и "аналитического" ("не-аналитическсго") применения правила вывода позволяет сформулировать и обосновать тозис о существенном повышении вф^ективности систем' поиска _прк использовании кв-аншшичесхих правил вывода.

Далее ожочаотся, что самой значительной попыткой реализация адеи : овальной" обработки инфор^ции в 60-е годы можно считать появление обратного лтоба С.О.Маслова, который сшлезировал оба выделенных > выше подхода использования идеи Глобальной-обработки информации. Анализ особенностей секвенциальных исчизлений,. используешх длй организации поиска вывода» позволил выделить . "генетические" идеи,' которые лвв^т в основе созд&шя ОУ и проясняют "суть"- его работы, среди которых наиболее сущартвевнши являются идеи переворачивания направления поиска и кспольэовашш структурной информации о "зацегоюетооти" литер формулы.'

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

' Во иоЬоЯ уеотн асрагра®» ("Яаяоб лоошюрохемоа б ШЗ") дазтсл краткоа' .концептуально® Е8."®эшэ ада® мвШа лтвтрэжэнюи. Определяемся конярогаэацЕя огого изгодв цяя теории поиска шЬода (лот®) -* лшвФ бреш&шх пврелехгйс. Видэляэтся союз идея этого ш?ода - "йтйладавшжэ в доягеЗ жди:" окончательного содбора згжзшЗ термов пра .вддетавошё до «эх вар, пока :ш будет ггояуяэна шдс&швдая 1и2ормгщ5Я о ъгшх яермов. Прк&реаз зг' здьЕсвагзш ето2 . олува?, шкфкизр, поаятиэ ушШоаэо ' сСирео ¿нифиишпора. а* .¿¡толе рэаоящаК

в )сралсзхвгхх 2 гмдв»еяео сокока шаоде е®.ооеса£

исчисления о ввриазмоа сзяээсоЭ рОлОвюй Омиякмдаы.

Дя.робунсона а понятие связт а обратном методе С.Ыаслоза. ' > .

• .13 заклотонии главы отмечается, что представляется перспективным для твбрзтнческого анализа ТГф ■ использовать катаматичоский аппарат 0&5уяпиЛнсй итрортцш исчислений, основу котарого были .разработаны С.¡0.Масловки. Обобщение результатов,, полученных при анализе истории развития. ТГО позволяот выделить яекболее штерасные направления ее дальнейшего развития, ,

50 вторсЗ Ш2Ш ("Обрам&Л летад С'.ОЛ'аслоба") атовкгсп задача • лостроотт на Соза обратного штодв .С-.П.Нзслопа15' юзчясягаия поиска шводз - исчисления чисел, с иНВекссии с цель», моделирования на ого основе разных тактик поиска ешзодп. ...

ПэрааЯ парчгрсф {"Сбщхч сяе&г обратного леяода") поопящея 'ао&троежт покотороЯ ксикрэтазсцка сбрзткого , метода для, зс-гислзжш шскозиваний. Пусть нам дака формула 'в даЬьпглтквнсЯ. нормальной ферт : 7 п а V -а & & V а & .V -а & -Ь и сакв«»-, давльиоа гтечпелонкз С без структурных ирввил. и с допус?.:.'..'.:: правилом сочетая: • . • •''"• ' ;v,\-f

ДХСИСОД&1 дашого исчисления 'являются соквоада" "V. вядп

X,» 12» ï3 t которые содержат кентрарнуа пару литер.,

ПРАВЯЛА ВЫВОДА исчисления следующие: ..." , v„V

д- крстяое . ? V V VУ, "Г

праэаш -> a1¿ *п» в.

г.

я -'.кратное' j ■ -s> 8tA-,» Ag» ' »'.'.»■ правило -> v

. ¿ЦУ A,v ..¿ v;

;, ■ ¡&ЕОДС65 формулы F иазнзевтея дзрвзс, получег-гоз -.-'.правил вывода, в кояцввнх>.вэрттах{чоторог^^^ э корна дерева - формула Р. г г У. "'

«Л ' ' 1 i •,♦«-• ,'.. ч 1 .

Мсслоз C.D. Обрэтлнй ; метод уотвиаддагшй : riurjo^iuoópl _ дли ■• логических . асчволвкяй. -У/Труда' .^катаматичеснйг^л'Ч^с^гугк'-©«.В.А.Ствклйва АН СССР. 1968. T.S8. Ч-Г '' ...

Построим дерево поиска вывода Р, в котором знак правилу -» V предварительно вменен на ):

"V" пс

•* а» ^а» a&ib» ->b

4

&

а» b» afc-to» ->b

5

a» -fc&b» ainb» -та 2

a. ^a&b. a&-&» ->b

з

а» а&^Ьг ->а4пЬ 1

Все концэецо секвенции дерева поиска ^замкнуты' ("задшнутость" секвенции будем обозначать знаком ы), т.е.содержа! контрарную пару литер: а и -«а - в секвенциях 2 я 4, Ь» ~ 1 секвенции Ь. Наличие одной кснтрар: эй пара литер достаточно да определения "замкнутости" какой- либо секвенции, поэтому вс< другие литеры и формулы "замкнутой" секвенции 'йогут быть уделены-"прополоты". Сфо. лулируем алгоритм. "прополки"16, на основанш которого преобразуем полученное дерево вывода фэраулы V "Избыточными" для г секвенции являются формулы а(. -ф и -1ё& Ь * да-' секвенции 4- формула а & ->Ь и литера -й. для секвенции 5- форму® а& -|Ь и литера а- На основанш произведенной "прополки" хоицевц: секвенций ветвей "прополем" нижележащие секвенции данной вотки из которых удалятся литеры и Соковые формулы секвенции, ю вот^ечащиеся в верхних секвенциях дайной ветви. Так как форда а 6 -ф не встречается в секвенциях 4- 5 и 2, то она ыоаат Сыт сначала удалена из секвенции 3, и затем, ) корневой секвенция 1 "Прополотое" дерево вывода Р выглядит так:

■* а. •> й.

а» ^а

•* а» -а&ь. -»a&ib

16 Шанин H.A. и р. Алгорифм ваянного поиока есгеотвэшюг логического выводе в начислении высказываний.

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

Формула ? будет шгляпеть ток: 10 ▼ 21& 22 г 32 V 4а

"Прополотое" дерево тавода будет выглядеть так:

(иначе л о квадратных июбок и знака 0 будет объяснено ниже)

-* 4,

-» □ , 10, г, А г2, 4, & лг ^

Кодировка формуя .пишете» суа;эствонной чертой исчислений на базе обратного матода а позволяет дать такое представление формул исчисления* виехвзнзшшй, в котором выразима' дополдательярч структурная информация о формуле, а гаюнио: "звцопленность" л^тер данной формулы (состав контрарных пар).

Вгедем исчисление чисел с индексами явгкм образом. Исходное понятие исчисления- понятие набора, который представляет собой ».«нотостоо чисел о индексами. Лксисиаих исчисления являются все такте пара чисел•с индексами, которые соотглтству а контрарным Нарва литер исходной формула- иагоОусш бла&трштсыз наборы. Концевые вершины "гфсиоштого" дереве енводэ, а таю» наборы: (2, 3,1, [Э1 (2„ образуй аксиомы пстартчэния пояска для формулы ж. Рдазсга&чдаоэ правзло клада ••сташэния позволяв? получать новые побори обьеданонием нескольких

благоприятных явбораз, щт котором возмоэто удаление тех чксэл о индексами, которое образуют кокную сооокугагооть литер некоторого дизькжта. В "г.рсаэлсточ* дерева вывода формулы У вновь полученные благоприятна«» нг:Сора г.рп дают га по дереву "сверху ешг" вэключеян п та^р этзна скобки. Например, при 'применении пропала вывода к чсхо»'та< благслгрялтвнм наборам ЦП я !

В результата получим новый благоприятна набор 80 так как числа 2, к 2г образуют полную совокупность литер & дизьшкта У» в кз благоприятного набора [10 получается благоприятный набор [4г1 исключением одаолитершго дизькшта 10. Т.е. правило шводэ исчисления является "механизмом" перехода по секвенциальному дереву "сверху шшз" от концевых секвенций к корневой секвзн'дол» который позволяет ксклтать 'кз состава наборов дизьюгштн исходной' формулы. .Именно с этик изменекием направления поиска по сравнения) ' с направлением пс>:сяа "снизу вверх" в секвенциальных исчислениях: й связано назвш1Г.о обратного яеяюда. Получете пустого благоприятного набора а означает построение вывода исчисления. ' Например, слэдуюдая последовательность наборов является выводом исчисления чисел, ностровкиоро для исходной формулы Р:

1-. Ио.г,) . 4. и0 V

2. [г2 Б. С1 01 кз 3, 4 . •

3. м04г] кз г^ г е. " с из б

Дкк того, чтоба показать корректное*'» полученного исчисления поиска, т.е. соответствие кшодв исчисления выводимости исходной формулы ? в секвенциальном • исчисяэшш, Доказывается. теорема р. полнота . сфо^улиртваннорз^ исчисления • чисел прбдгаьзпкему рэквенциальдаму исчисления. ДоказатвльотвЬ основано на том, что-любому "прополото^" секвенциальному, Еыйрду можно .поставить в ' соответствие вывод иочислдаяя .даезл»; и наоборот, либоа . вывод йсчкслэшя можно прёдсташть 'в шщ секвенциального вывода. . ' 'Анализ общей ехэин ОМ позволяет обосновать Яезкр о тоад, что" исчисленияна базе обратного ыотода'^представляет собой, по. ■существу» хамдечиедсния над формулами. логических исчислений, в которой выразжа допоижтельная информация о составе контрарных пар лнтер формул.;; Б^азктелыша Бошэяноста мэтансчислэний на ■ Опвэ обратного метода долада нх прквлэкагельным для использования как в практических системах автоматического доказательства тесней,'так я для решения некоторых теоретических проблзм лЗгкки, В частности,' с' помогай ОМ была ваявлэш ноше разрешимые классы дай;-, ода*чо. построение ; систем'

вэтоматачэского •докэатвльства теорем яа базе обратного штод® раязвно с проодолзкаем ряда трудностей кз-ва недэтеркаш^ ,веаног-о

фа^тера Ерсцзссв шроадэнал нэвых благопрв'ятшг наборов.

во второй параграфа ■ ("УоОифишцйи общей ох,агы обратного летода") деется ряд модификаций пр-тдлолэпного исчисления чисел, с целью построения практических алгоритмов поиска вывода. Для етого з параграфе сформулированы и даш "идеи" доказательств ряда лет, что соответствует моделировании а исчислении чисел ряда известных катодов поиска вывода, среди которых можно ввдэлить дав мощой «агода поиска вывода- сег.оО' революций и л&яоб раа^плекий. Основой моделирования зтих методов является структурное сходство правила исчисления и правила сечения:

■ гс .убило- сеченш правило еывода исчисления

' , ■» 1, С . В , -1 0 "'и» Л, X ( © ) 3, У ( Ф )

1| 3, О Ь ч 0 •> 1, В, X & I '( О )

Ае В " , -» А, В ( О .)

Здесь 0 & 0 (.такта этх-татать по Здесь 1С ъ У юяо ксклвчить по

правшу сечония, тан паи С?» -.0- правилу вывода исчислзкля, прч

противоречие, удаление которого' услошзн, что Л ь ^ образуют кэ нарушает выводимости А» ¿5. . дгаьгакт форда! б.

Моделирование прзЕяла реаолацкй (расаешшкй) связано о тем чго ого представляя? собой прз?:эяон::э пралилв сечения "сверху шиз" ("снизу ввэря) в секЕекцивльшх исчислениях.

Для шделароввшя! правила ргголгцпй" разрезается гз состава благоприятных нсборов зегетиать из только' числа с индексе;«, обрезуадяе некоторый -даомиаге звходаю® формула, по и пару чисел, ссотвэтствуетзв контраршм парэа хатвр. коходш. . формул;. Корректность этс$ ковфшцкя зечжмишяя ' оЗосноЕнэаатся дапуотнмостьв пр&гшла езчзкгя лет сзгшзцЕальшго'нечисленна б". ' Для моделирования мэтода' ■ расцеплений. , ярэдзвр-тедьло ' доказывается зеяггя леига о коргалЕзацт* вывода, . которгя Позволяет икшетвть г.з числа благсар&ттнх кабороа, вэсбходанг для получегал завода, асэ ааднвбора некоторого Слсгепргпгного. кеборн. На соковагса втоЗ дашз аогмояаа. вв -только яормзляэзцзя зквода, ко з дальнейшая тадайгавоза всздевоЗ ."внготошя" у.ечколегпя:. "ксгсуостпеаков" • взедекзэ прз ютгроешз выводов од:-:ои-ей!шх каСоров*- аояувяйий, что псэйоляэт оуцэогэзкпо сократить чесот бяагопркягкЕнг наборовг -учветвукглх а вдзодэ.

•

Моделирование метода, расщепления тохьичоск! осуществляется построением л,тточиоления задисилоапей. Структурное сходство правила расщепления *и правила исчисления чисел позволяет предложить еще одну модификации предложенного исчисления за счет моделирования аналога правила росщешюния- правила раащемвния по н&каторолу визшиапу. '

В заключении параграфа обсукдавтся возмокности метаисчислеютя' зйЕисшостеЙ и дьлается вывод о том, что построенное исчисление Может служить хорошей основой для разработки универсальной: системы автоматического доказательства теорем, в которой возмокно ' ! шделирование различных стратегий и тактик поиска вывода. V

¡' глава {'¡¡тсллеатуалъмый батрекинг (Intelligent

bicktracMng)") посвящена решению проблемы "отхода" ; ! (backtracking),. В ней ставится . задача показать возможности 1 aitiXtwrtuMscKoso подход а для решения проблеш "отхода", и обосновать тезис о совместимости существующих в TUB методов поиска "в .глубину" и "в ширину". Для этого зд">ь построено исчисление : поиска вывода - исчисление "интеллектуального бектрекинга" (на .' основе' системы поиска, предложенной И.В.Екковой17), в которомЛ , возможно сочетание этих методов. , -

: £ В первом параграфе ("Постановка проблем: <поисн в и/иршщ> и, ' <паиск в глубину>"). задается тема 'исследования, которая определяется противопоставлением существующая в теории поиска '^вывода двух стратегий поиска - методом "войска в глубину" и 'методом "поиска в ширину". Пусть нам дана формула © и. некоторое 'множество формул- мир S. СтавитЬя задача найти такую подстановку, ' 'которая превратила бы результат подстановки формулы © - в* - в формулу» выводимую из формул мира S. Если, например, дшш фэриула +;Г(х) & Q(y) & п(в,у.) >8(х,е) и некоторый мир

. • . 0(8), «(О), Q(«)i; yi... , '

r. ' : . S(b,b),B<b,b),B(b> Vh ' ■■

ЧЕикова И.Э. Автоматическое дохбэе.телъотво теорем и яоегровиив , ^фкяГ//Алтарям» в ^грвммы; '1ЭТ8. #'4.- /:

. то для шлугэтм вывода «формулы в тире необходимо, чтобй ; Кавдий коньшкшаный член формула ' О* совпадал о некоторой эледавтариой формулой из S1. Эту задачу мокло решить, например, ; составив систему уравданкЗ на термах формулы в, и мира S, и найти пересечение для значений одгашковнх переменных формула. Если его', -'пересечение для яавдой тарвиегзной формулы Ф1 не пусто, то система/ ¿»равнений ивдэт реяшиэ'я} (идея В.И.Шалака).

Использование метода "поиска а ширину" предполагает sa .каждой уровне решешя снстеш уравнепв® находить- все возмоккыа решения для каздой квротшгой. Составим систему уравнений, для , данного призера и реогм вэ методом, "поиска в ширину". Система ; уравнений выглядит так: .

1. ж = а» ъ ( дм ворного коньшшшюго члена формулы ) "' . 2. у в ъ„ о, д

3- ( D « Ь 4 у » <! )i (z-b&y*a) 4. 2 * Ъ

Найдем парэсэченш значений для кавдой переменной формул» . Благодаря пД, и.4 рвкганнем для ж яшшатся одноэлементно®, шожаство СМ, а благодаря п.З- реяешгам для s - {ь}. При анализа . П.2- п.З видао, что решением да у является двухвлементиоэ нноггагтл {о, а). Таким образом, подотанозкш {s/b, у/а, а/Ь}„ {г/Ь, у/а, z/ъ) нрезращавт формулу в формулу О*, выводам?» в tape S,, т.е. являются искомым решением.

Другш подходом к решению данной задачи, которой особеазо • оправдан при "больших" мирах S, является "повск в глубину,", суть которого заюанавтся в поиске на кздоа уроввз лиаь первого возможного реаеияя, удовлетворяет,его ^еловнш задачи. Для данной смстаки урашэнй,* на перлом уровне будет вибрато вначенна ж » а, .". на взорсч- у » ь, -что щдаедет к "яэудата" на тротгъп уровне."Тек ; юзкгкает проблема "отхода",, котсреа связано с там, что' nps испольгованхп йэтода ¡хкскз "в глубгму" евходится лаиь первое локальнее ■ ротэяав, которое ' а обдам сдучеэ ношт сказаться взвэраш, к шдяоааг и вря дзльнэёзвй пощт*

Во gî£2&!î' ("В&роришыш CôaOcxuë 6

<^зв»9ллещ/аа?шй Свщхяглкг*. itnt*}U$snt ЪасМгая&1п$)*у дается -обцоя . таеиз '"uïcxwvïryoutno'zû ' fô/ap-iariOT" {intelligent boolrtroafcirjs), 'fctoptft Шзя. прэдяотва дяя яреодолелзя иодосхаткоэ

тактики "наивного бектрекинга" ("naive baoktr king") за счот использования ажииишзского подхода к построению выводов. Основная идоя "гттвллектуалыюго бектрекинга" заключается : в анализе полученной при "неудачном" означивании информации для выяснения возможная, "причин" неудачи с целью их блокирования при следующих попьтках означивания. Для пояснсншя сути "работы" "интеллектуального . бектрекинга" предлагается конструкция двоичного дерева поиска подстановок, вершины которого соответствуют означиваемым термам, "левые" ветви * сделанным в процессе поиска подстановкам, а "правые" ветви - запретам на ту или иную подстановку. Представим в виде такого двоичного дерева процесс решения методом "поиска в глубину" ггродлокешюго примера. При атом неудачу при означипании будем помечать Р (rain©), после чего происходит "отход" сверх по дереву. Сделшшая ранее "неудачная" подстановка, которая вероятно ответственна за невозможность дальнейшего означивания запрещается (появляется соответствующее неравенство, например у/Ь при первом "отхода"), т.е. на дерева в соответствующей точке бирается правое ребро, и поиск подстановок продолкается. Успешное завершение поиска

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

случав, пои с]; швода на предложенной конструкции двоичного дерева шглядит так. В процессе означивания термов, происходит движение вниз по дереву поиска. При невозможности дальнейшего означивания, выдается сигнал неудачи и происходит "отход" назад. В тактике "наивного бектрекинга" причины неудачи но вяалиэирумтся и отход происходит на предыдущий шаг, где выбирается сдедуюцая альтернатива. Однако, если сделать анализ возможных "причин неудачи", т.о. анализ ранее сделанных подстановок, из-зп которых невозможна подстановка на атом шаге, то воомокен отход к 70Я точке дорлва, которая является возможной "причиной" неудачного означивают, блокировка ранее выбранного решении и просмотр следующей альтернативы. Такая организация процесса "отхода" позволяй'г существенно погасить эффективность систем! поиска, так как при выбор* альтернатив из рассмотрения исключаются целно куски дерева подстановок, лежащие гашз той ого. варяюш, которая является возможной "ггр'л'лшйГ ¡{Ьудачи.

В .третьей параграфе ("<Горжиъная систола ьаеяал штупльного бектрекинга") ст авится задача построения исчисления поиска вывода "интеллектуального бектрекинга" на основе языка исчисления предикатов первого порядка, который обогащается дополнительным, атноае.-ллми на гермах - отношениями равенства и неравенства. Это позволяет задать систему ограничений (отнсшина неравенства) и систему предпочтена» (система равенств) на дотшшо подстановки при поиске швода.

В первой часта 02В5ШМ1 задается логическая -истома I. в этом обогащенном язшсе исчисления предикатов. Наиболее сушрствептм является определение правилыю построенной формулы 1> а связанные с ним понятия глпрояиворечивсй прсСиси Е! ооблвсшлосяш троен. П.п.ф. Ь представляет собой варшгазжа рада ч Г С К ) I О 3 где С - является п.п.ф. ..очислени». предикатов,

Г(К) - система неравенств (рввенстп) (Г, й- розиокио постно), О - подстановка, прнмвнго/ая к цепочка ( Г С К ). Для того чтоб?! выраншмэ ( 7 С И )( О ) являлось П.п.ф. систр«» Ь »»обходимо выполнение следукз« ус.«ойяЯ:

1. Г должно быть 'ненр тияорачию, т.е. но долгою содержать протииорачивйх неравенств типа 5 / х.

2. Г н К должны быть совместимы, т.е. если <= Г» то х«а в К в'. . наоборот,если х=а.е К, то »¡в в Р.

3. О должна быть совместима с Г, т.е.результат конкретизации Г ' посрэдством 0 да должен содэркать противорачжмх неравенств типа

хз*х (конкретизация Р посредством О непротиворечива).

4. О оошестима с Г и К, т.е. при конкретизации Г в К посредством О должны Сыть совместимы.

• Тройка Г К О называется непротиворечивей, если я только веля ' Г, К, 0 удолетворяст вше сформулированным ограничениям, т.®. . если (Г С К ) ( О ] является п.п.ф. Ь.

Тройка Г1К101 совлостиа с ве1фотиворо<г»чой тройкой Г^К^О^, если и только если тройка {Г1Г^)(К1К^)(01^) непротиворечива, , где цепочка, 0^) - результат кешозшрт •

! траванств Г4 а Г^ (равенств К^, подстановок О^). , ^

, Правила вывода I являются обск&вяпом обычных правил вывода-исчисления' предикатов. Нзпридара' правило подстановки' : формулируется так; . @ ''

к" ■ --——:--обобщенное правило подотанозки

Поняпгэ ^боЗа системы Ь стандартной.

У Во".' второй: чести • параграфа формулируется ' собственно ийчиелвнив ' поиска >инг. иетусиьного б&оярвкинга, в котором. используется основная идея катода штгаюрскэнных - не большая, цт вто необходимо, уточненаость знвчэнкй термов при подстановке (понятие поаозыг&Аъного сопраюблття формул является аналогом понятия наиболее общего еапора в методе резолюций).

Определяются. правило поиска' исчисления и понятие Дерева поиска вывода, вориущфувтсй обдая 'отратогая поиска подстановок методом "глубину*/" которая сводится $ ) нахождению таких »роек ;$зРЦ0,,. .^пОй'. V ,из /¡которых непротиворечива;' в

'^июмяию^¿идущими непротиворечив»® тройками. При ^ю^рцввовц пр& ^|..,^|1яю1св'.гуваявв*ся., -'-"аулы уяцая тройка

>Д•• '**#«»' мшллещ/сиьного . Ш -Ья^ате^^ - иахаяиви'

>мйЬаве«>«»а.-:- ^^рвввиязг^**. в ююааоя»

"неравенств" при неудачах. Это наглядно представлено на предложенной ранее конструкции двоичного дереЕп, правы» ветви которого сооответствувт системе неравенств, а лепив - система равенств. Если в процессе означивания термов появляется сигнал неудачи, то .в систему неравенств (равенств) записывается новое неравенство (равэнетво), полученное в результате анализа возможных "причин неудачи", и процесс поиска продолжается с учетом накоплешюго "отрицательного" спита.

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

• тактики "интеллектуального отхода". Для решения этой проблем ыокно. использовать щдадлог®гиую конструкцию двоичного дерена поиска подстановок; которую »зоззго- рассматривать.как семантическую базу исчисления "шгголлеитуальиого бектрекинга".

в ааключвгии главы сформулированное -иочислекиз сравнивается с другими шдобшши сзств^ми, обсуздеатся вопрос вф!ективностн ярвдлояенних систем, а также устанавливается взаимосвязь предложенного . метода "интеллектуального бектрекинга" о .результатами иодафшздга языка "ПРОЛОГ" (за счет использования операторов ''out", "eaveojjp", "cutto", ■ "gat backtracking") и О реализацией идеи "заморозки" вычислений (freeze operation) идя "ленивых вычислений" (lazy evolution). Нз ссповэ проведенного енаяиза sukb.ii лютея перспективы дальне Пкзго развитая метода "интеллектуального бектрекинге",' а тажэ формулируется тезис о том, что предложенной нсчйслэ1зю понгао еоздакш использовать как' универсальную систему • попе:«, яа база ¡шторе! позтгпо сочетание •• датодеэ поиска "в глуб?шун и "я шрину". ::

1 акз-.г ксиомогамльнай xapfficrgp si дополняет содерштае пврвоЗ глвва Дйосзртгцаи. Одесь сформулирована система натурального отвода и ' сзстеш пог.ска па основа метода "чорвдоаваяя яагоз вювдо я статава" В.А.Смнрлоза. "Работа"

• csctskj пс«с:;а рззегр-лтм т прлмерэ построения гавода еекапз Гйгрса. Главков шътгхъ удакэтся обсувдэгст проблем, военикииза при 02Л'сяази.ш -псйстелтюка p.caaiwaas натурального ггоода.

В прилагают Я стгштся задача таотрсзшк всчиолзияя пеке«« с тернарной логической связкой • лобной бизштцш. Связвд. условной дяэьшкций, введ-шшя А.Чзрчем, обозначаемся (£« в» где Л» В, Я - пропозициональные фор^оглн. Это ошшсь понимается так: если эдшчонио формулы Б истинно, то вд&четае ©эрдула ¡AeBcö), совпадает со значением формула Лг в противном случеэ, т.е. süss вначзоте В лошю, • внзчокке {Д, В8 05 совпадает со внвчэниса формула С. Связна условной Низшшщш к константы t «i 1 оЗрвзувг. полную систему связок, что позволяет построить ярошзацйонаЕьвоэ ^ исчисление10. Другие пропозициональные связхн кшьткцшд-;■ даэьгакщт, импликацки, отркц&ния определяются сладуд^ал оЗразок;

• ' Л & В ; И I А, В, ЗГ 5

' ': . А v В а 1 t, а, в i

^' А.« В « . I В, Ü J ' '

1А » ' I S, А, t 1 i

Формулы праггоэнциопаяьЕого исчяокекия * предотавшиг ообой совокупность вложенных друг в друга уроек. Наирзд.ар„ вшшн утвэр- ; вдвния коисеквента р * (sj * р} вьтлядат тек: /' llpt q, р> ti« : Sto позволяет представить их в шдэ вереЗъз8 щхюя. Ишрзадар, формула 18рв q, tl6 pe исчисления прэдетавша rsxJ -

V . С • .■•::••'

(отметим, что любую концэвув пропаекщгоналъную трззжшую р а . дереве троек еозмохяо аамекнтъ на тройку (u р»

Такое представление формул позволяет продлокить процедуру проверки формул на общезначимость. Дая етого построено исчисление истока вывода - исчисления троек. Основой исчисления являются Деревья троек, сопоставленные формулам исчислааия васкоэываяий ■ о условной • дазышщвей; : : - ■

; Дшяюишв исчисления налился концевые Воредаы ц кшетантой 4.

Vе, СиОорШка Е.А. Пропозициональное исчисление* 5о условной ршьюнющзй, //ётавы логического анализа. J97?* ; •,

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

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

( Путая в дереве троек называется последовательность' вориии дерева от корня дерева к некоторой концевой ызршинв. Путь с наделении направлением обхода для каадой вередозд называется вивзлше^А пукел. )

Понятие куводз кечнелепил, соотЕотогауазэе тавтологачности исходах Формул исчисления шск&знваний, формулируется так?

DuSOÖOl ИЗБНЕОЭТСЯ дэрево, У которого ДЯХ50Я выделенный путь o&tpteг, т.е. оканчивается ехсиомсЯ.

; Праведеняоо зязэ дарэао троек является заводом исчисления, ) так как дабой пугь о? корая к кседешм литера» втого лэреза ." пакрыт (ежатам, что после взрхней. лнтзры р нельзя Еабрать путь! ; играю а конотанга t, тек как ргнэа, от корня дерева, -было шбрэно испреахапкв обхода дерева после jztTopu р влево, а я&правленкв обхода ташгз коризвой .здтари р израво охвячив&лось жагстаптой t).!'• ' ' ; • *.

Шравзло тавода йсгводлат- офор^гэровать сяедатаЗ алгоритм шнека вывода, которая является еншюгаа штода pscssamiaa:«]':,

Если поело выбора выделенного направления/ ко нэкоторой 1 переменной любой путь дерева троек бощш, то для проверки : тавтологичнэсти формула достаточно рассдатрать дерево с •' противоположным выделенным направлением го атой первдашзй.

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

В эакяючанкй Мссгэтеугет кратко {^¡«¡круэтея осеоейжз результаты работа и намачаптся дашшЕшиэ перспз!шшн равгеткя. теории поиска вывода к автоматического доказатэльстаа теорзк,

•'■ фЗазвздв по тоаа @8оозтзтеиШ'; .-•

I.'. Катрвчко С.Л. Модификация обратного кэтода "С.Э.Мэслозй У/ Материала' X Воэсошпой конфэрэкцан по дотаю

кеукж. Шнек., 1890. - 0»1 Ь.л." "' . <\

2. Кагречко С. Л. Коделировааш празшга расдаиший- г воротам : методе С.Ю.Каелоаа// Логические катоды в компьпгвршиг каукех.

М.р. 1853. - 0,6 п.л, •

i » «

3. Натрэчко С.Л. Обратный катод С.Ю.Каслэва да исчесдоейй Еь:с:гс-еываккЗ // Лопаз к коашъвтвр: и -И., (в печати)«? п.д,' '

'■■' -"с