Введение к работе
Актуальность теш'. Внедрение d широкую практику электрошго-внчислитолькнх систем поставило перед наукой ЦЭЛЦЙ комплекс нових гносеологических проблем. Применение ЭВМ измоплет ' хяракгэр информационного взаимодействия человека и природы. Видение мира человеком становится все более и более опосредопаняш машиной, и это нельзя но учитывать, как нельзя отбросить влияние микроскопа, телескопа н налагаемых геля ограничений при ииучонии' обьектов макромира, космического пространства. Применение ЭВМ налагает свои ограничения, свою сетку видения мира. Например, при использовании программных продуктов необходимо учитывать прлзщнппальную огрекиченнснзть (финвткость) ресурсов 8ВМ. Кроме тогос ыяроков распространение кшпъягеров н орэдств их программного обеспечения поровдает новые гносеологические проблеми 8 насущность рэяэкия которых выступает кис своеобразная "прпхтяка" для осмысления в "теории'' паучнах исследований. Тшс, например, появление разработок в области "искусспвеююго wcrjjusisw." (ИИ) заставило исследователей обратиться к изучеівгп способов извлечения и переработки информации, что привело к бураояу развитии комплекса canputGr science, .которйн образовался па- стеке научных дисциплин, издавна зонкмащихся проблески нналеяип, - философия, психологии, логики я эвристики.
Таким образом, современное розвитеє ЭВМ делает .актуальным мгализ нових гносеологических проблем, ветанцях перед computer воіепов, к разработку нових напрпвлзвкй исследований для рекенин
8ТПХ Проблем. . '/
D то ки врекяв следует отметить, что успеха в области програчжрованкя во многда овз'заш с укэ накоплвгалш теоретически?! багааом решения пюсеологических проблем в' пауках комплекса uosputer воівпзо. Необходимость учоfa'этого влияния "опыта" computes? воігное аа ""практику" программирования {"иехусстярниого : интеллекта*) выдвигает задачу осмысления
ДОСТЙЯЭКИЙ ТвОреТЕЧЭСКИХ ДИОЩШЙИЙ КОйШЛвКСО oor^iutep воіепов для
далькейвегт. развития шгВормацнонянзс "орудаа* человэчясгво.
Цет si аедата йссходссзікя. Дакявя работа поозадзпа вналйву одной из научных, дисциплин cocputer воіеооо -. кзарш, поиска'..:
- г -
вывода (ТПВ),, которая исследует возшкше способы решения задач в логических йстаслзгашх. Целью исследования является ответ не вопрос: как бозлохно использование лепщровнвбих сребстд От решения вайач 6 логических исчислениях? Достижение этой цели осуществляется в ходе решения следуицих задач:
построение методологической бази иссладовашш, основой которой выступает понятие иипэллошлуаАьной (логина-эвристингаюй) систем. .
анализ, истории развития теории поиске вывода с цольїз виявлення наиболее интересгаа подходов,, обвспочизавднх аффективное использование кетасредств для решеїшя задач в интеллэктуалышх системах типа исчислений поиска бавойзі
выявление возможных "точек" развития ТПВ в t данном ншіравлоіши и обоснование персгэктпвносга использования для отах целей идеи глобальной обработки информации (летода Авпюпереяеюых).
конкретная реализация некоторых из выявленных идвйшх "схем" (правде всего, связанных о идеей глобальной обработки информации.) для более аффективного использования квтауровнвша
срэдсгв в исчислениях попона вывода.
Степень Еазребота^юдта теш? іомздшаншг. С одной сторона, проблематика Ї11В таено связана' с проблематикой овййюшческого дотэаяельатва торел, и существует целый ряд исслэдовадаЭ, посвященных анализу систем автоматического доказательства теорэя, в которых в той шш иной охепэни затрагивается круг пробдан 2ІШ. Достаточно полный, обаор втих исследовании дна в работе1.
: с другой отороны, теория поиска вывода является погреначнод дшмешшшой комодако'а computes» aoienos, на стиха jgoraos, впристикэ, исахагюгет, и возшшш анализ ее проблемветіш точки зрэкия равішх "родительских" иаун. Условно водло вддадагь следуюдо направлення иооледовашШ:
I, Анализ с тачки зрения понхолога? о щель» виявлення в моделирования пенэютгичаскше кэхадаюшв решения видач ташвэкзд. Этот аспект исследований (раввития) теории понова вывода шаот
, ' Ворашсов А.А., Дегтярев 'д.й. Автоматическое докедвввдьотво гаорзм //КаОвряетдгяе, 19*36. & 3; 1987. Й4.
Сить выроетк воггросом: каковы психологические моханіпчи решения задач человеком и как возможно их моделирозатше в рамках ТПМ? Этот подход представлен в работах ггсжсологов2 и (философов3.
Z. Сложностнэй анализ достижений ТПВ, при котором главным ЕОПрОСШИ яплявтся следукюие: КОКОВЫ слогаюспше. оцешси эффективности рэзгак светом доказательства творам к накопи пакболеэ эффективные сродства повшіієния шщнисти исчислений? Донный подход представлен в появившейся на отже математики» теорія! алгоритмов я .топки новой дисциплины теории сложности,. проблематика которой тесао связало с проблематикой ТПВ. Это ваправлвпкс- исследований представлено в работах специалистов по теории сложности4 и математической логике5.
3. "Качественный" подход, при котором анализируются наиболее, интересные адейко подход, реализованные при развитии ТПВ. Центральным вопросом ксслодоввния при атом является следущия: с. кзксвн вогяотые "механизмы" реиоккя задач я квкке из ййх педдвптся моделированию в логических системах? Это направление исследования (развития) теорий поиска вывода опирается . на, достшшкия философии (пюсвологян), логики и.эвристики n uosar. быть незвано логико - эвристическим или эвристически* подходом. К базовым работам этого подхода; тою отнести работы российских логиков и фиюсофов О.О.Серэорякншова6, В.Л.Смирнова7, а топя пионера ссбствешз тэораи поиска вывода 0.0.Маелова9. Именно я втому направлению йгеслэдовзнкй относится данная работа» '; ';;
Пускпн В.!!. Эвристика- катка о <гвор<а>ском каезлэнни. M.t t967<»
3 Бриашгкга Е.Н. Логике, мшшовйв, шфзриация» Л,, 1998.'
* Cook S.A.. neohow R.A. T'lis relative efJioenoy ot propoeitional proof systems. //Journal ct sbtbolio logic. 19Yvb Тої.44, N.1.
В * ' ""
Данцин в.я. Алгош'-?'нка_ задач . ваполшчэота //Вепр. .
якбаряетаии. 19в7. Вып.13". . *;
СеребрАріадксп 0.4>. ;: ^раатячеекзгэ прзм-рігш & логячвекиэ
исчисления. Л.,!9Т0. '
т Сгстрітоз <;.Д. орыальныЯ пизод а дагячвежмя' аочиейэгзш* \k.,
Маслов СЮ. Теория двдуятийныа сиотвії я ев іпиквисідав-5-М.,
1986. -
_ 4 -
?ЕЗіская и иТОмогичвок8я осново Зсслейованмя.
Методологической основой исследования является. аппарат современно!) теории . познания, логики, эвристики и теории сложности. D частности, значимими для данной раооты являются категории анализа и синтеза (Папп4 Александрийский), которые существенны при рассмотрении процесса решения, задач в'ТПВ.
Теоретической основой исследования являются труда логинов в пионеров теории поиска вывода К.Эрбрана,' Г.Генцена, С.К.Клини, Х.Е.Кврри, Я.Хшггикки, Э.Бета, Р.Смальяна, Д.Правитца, С.Кангера, Д.Поив, О.Ф.Серобрянникова, ' В.А.СіЛирнова, ленинградской (петербургской). школы . математической логики Н.А:Шашша (Г.В.Давыдов, Г.Е.Мгащ, Г.С.цейтин и др.). Особо" необходимо отмотать работы С.Ю.Ыаслова, крторые заложим концептуальную основу теории поиска вывода. .
Автор опирался такаэ на . работы специалистов в области программирования, "искусственного интеллекта" и психологии Н.ншіьсона,'; А.Ньюэлла, Дх. Робинсона, Ван Хао; Р.Ковальского, Д.Л.Поспелова, В.К.Финна, В.Ы.Сергеева, O.K.Тихомирова.
Новизне ^ссертвцаощіого исследования. В. диссертации получены слодующие результаты, которые вшюсятся на защиту:
- введенное гдагодогагичаское понятие "интеллектуальной (лоешю-эдрисмической) систет" тазволило выделить особый тип логических исчисления - исчисления поиска вывода, и-предложить перспективное направление "интелшктуализацтГ логических " исчислений структурную отшциалиэацшо вывода,
введение понятий сяшштеакоео н оіявявтчесісого спрообаб построения выводов,, а также "стлшшчзснбвп'' и "т~ anaлtЩLчecкoгo,^ применений правил вывода позволила обосювіт тезис об ограначенноотй (неэффективности) аналишівского поОхобс к построении вывода и необходимости йспользовйшга (дл* преодоления втих ограничений) "пе-вв&яитйчеотщх". средстї йострооякя вивода, і: которым относятся, иапрйкэр, ияз-екал;шгчвс?:09" пршвнэшю правил вывода.
предложопяая їрактовкн метода пояска вывода- оаратма&і лезова. С.В.Наслова (Ш)~ позволяет существенно модифицировав дзкгаЖ.йэтей для есчксловея шсквзиваюй із рассмотреть ва Cess Of
исчисление пояска вывода - исчисление чисел о инВвксаеи, з . котором возмокко моделирование других.нзвастиых методов поиска.
- для решения проблемы "отхода" (baoktraoking) предложено
исчисление "интэллэктуашюго бектрекинге" (intelligent
baoktraoklng), полученное обогащением языка логики предикатов
первого поразка, дополнительными отношениями . на термах, что
позволило предложить новый апгорита унификации терюв, сочетающий
Идеи нетолов поиска "в глубину" и "в ширину". .','
- предложено исчисление поиска вывода! для исчисления,,
высказываний на основе использования тернарной легическоп связки
І/слодной д:ізьюнхири, что позволяет наметить линию развития TUB, [
связанную с использованием тернарных логических сьязок.
dB5?H?.S335 S?3^9I!; 25PJ3^o5!P5S заЯлг.чается в том, что представленные в ней результаты могут сыть использовали для . подготовки спецкурсов по логике, орионтированшк на компыптерное приложение, и для подготовки спецкурсов по теория поиска вывода (автоматическому доказательству теорем). Предложенные исчиояоішя покоса . вывода могут быть использована для модіїфикацшг существующих в разработки оригинальных программных, ерядств. :
*5Е95^5 2?Й1!' Дисевріаяяя.'обсуздвна и рекомендовано к Защите на заседании сектора 'логики; института фшэоофии ' PAW. ^авличныв' аспекты исследования 'излагались в докладе . на g Зсесошноя конференции по .-'логики*методологии и философии, науки ' (Уинск, 1990), в сообщениях не научно- исследовательском семинаре по логике института филосефш РАН в яеоретическок семинаре кафедры логиш философского, факультета }Л7,ш.М.В.Лсмоиооова. ,
УШКИЕЗ ffi?oepTagf«| , оСусжтлвнаЧ;-,;!ілью. н спецификой йсслэдсваюп. ^Работа coot «гг'из введений,.; трех глав, вшуяяеняа, двух прилскэнва а списка литературы. Первая глава кмеэт оолзэ концепту am-щи. характер я ". посвящена обсуядвнки проблема шюяызошш *-отауровн9ь?-х средств в интодпектуцльнях система.' Она состой? вв трех пэраз^рафов,^ іюследакй из которых; разбит на две чаотн/к вфйвченкя. Здесь/на основеанализа история развития.' теории по'асщ йгеода;выдел&нн/иаи&элеё;Пэ^ "интеллажтуализацки* исчислений Іпсист^ вывода. Вторая» третья
- б -
главы посвящены Солее конкретным вопросам использования метауровневых средств при решении задач. Во второй главе обсуздается вопрос использования метасредств для исчисления высказываний. Здесь предлоконо исчисление поиска вывода на базе обратного метода С.Ю.Маслова для классического исчисления высказываний. Она состоит из небольшого вступления, где' дается краткая историческая справка создания обратного метода, и двух параграфов. В третьей главе обсуждается Еопрос об использовании штасредств в исчислении предикатов на примере решения проблемы "отход ". Она состоит из небольшого вступлеїшя, где дается краткая историческая справка проблемы "отхода", трех параграфов к заключения. Приложение I посвящено обсуждению проблем создания 'исчислений поиска вывода на базе натуральных исчислений. В . приложении 2 предложено исчисление поиска вывода Для классической логики высказываний на базе тернарной связки условной дизьшкции.