С.Л. Катречко

ЛОГИЧЕСКИЙ АНАЛИЗ ИНТЕЛЛЕКТУАЛЬНЫХ СИСТЕМ С МЕТАПРОЦЕДУРАМИ

(автореферат диссертации на соискание ученой степени кандидата философских наук по специальности 09.00.07 — «логика») <**>

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

Актуальность темы

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

Таким образом, современное развитие ЭВМ делает актуальным анализ новых гносеологических проблем, встающих перед computer science, и разработку новых направлений исследований для решения этих проблем.

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

Цели и задачи исследования

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

— построение методологической базы исследования, основой которой выступает понятие интеллектуальной (логико-эвристической) системы.

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

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

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

Степень разработанности темы исследования

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

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

1. Анализ с точки зрения психологии с целью выявления и моделирования психологических механизмов решения задач человеком. Этот аспект исследований (развития) теории поиска вывода может быть выражен вопросом: каковы психологические механизмы решения задач человеком и как возможно их моделирование в рамках ТПВ? Этот подход представлен в работах психологов [2] и философов [3].

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

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

Теоретическая и методологическая основа исследования

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

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

Автор опирался также на работы специалистов в области программирования, "искусственного интеллекта" и психологии Н. Нильсона, А. Ньюэлла, Дж. Робинсона, Ван Хао, Р. Ковальского, Д.А. Поспелова, В.К. Финна, В.М. Сергеева, О.К. Тихомирова.

Новизна диссертационного исследования

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

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

—           введение понятий аналитического и синтетического способов построения выводов, а также "аналитического" и "не-аналитического" применений правил вывода позволило обосновать тезис об ограниченности (неэффективности) аналитического подхода к построению вывода и необходимости использования (для преодоления этих ограничений) "не-аналитических" средств построения вывода, к которым относятся, например, "не-аналитическое" применение правил вывода.

—           предложенная трактовка метода поиска вывода — обратного метода С. Маслова (ОМ) — позволяет существенно модифицировать данный метод для исчисления высказываний и рассмотреть на базе ОМ исчисление чисел с индексами, в котором возможно моделирование других известных методов поиска.

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

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

Практическая значимость исследования

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

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

Диссертация обсуждена и рекомендована к защите на заседании сектора логики Института философии РАН. Различные аспекты исследования излагались в докладе на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), в сообщениях на научно — исследовательском семинаре по логике Института философии РАН и теоретическом семинаре кафедры логики философского факультета МГУ им. М.В. Ломоносова.

Структура диссертации

Обусловлена целью и спецификой исследования. Работа состоит из введения, трех глав, заключения, двух приложений и списка литературы. Первая глава имеет более концептуальный характер и посвящена обсуждению проблемы использования метауровневых средств в интеллектуальных системах. Она состоит из трех параграфов, последний из которых разбит на две части, и заключения. Здесь на основе анализа истории развития теории поиска вывода выделены наиболее перспективные направления "интеллектуализации" исчислений поиска вывода (по этой теме см. также приведенный в конце реферата список публикаций NN 2, 5, 7, 8, 10, 11, 12, 13, 15, 16, 17, 19, 20). Вторая и третья главы посвящены более конкретным вопросам использования метауровневых средств при решении задач. Во второй главе обсуждается вопрос использования метасредств для исчисления высказываний. Здесь предложено исчисление поиска вывода на базе обратного метода С.Ю. Маслова для классического исчисления высказываний. Она состоит из небольшого вступления, где дается краткая историческая справка создания обратного метода, и двух параграфов (по этой теме см. NN 1, 3, 8, 14, 18, 20 из списка публикаций). В третьей главе обсуждается вопрос об использовании метасредств в исчислении предикатов на примере решения проблемы "отхода". Она состоит из небольшого вступления, где дается краткая историческая справка проблемы "отхода", трех параграфов и заключения (по этой теме см. NN 9, 20 из списка публикаций). Приложение 1 посвящено обсуждению проблем создания исчислений поиска вывода на базе натуральных исчислений (по этой теме см. NN 16, 21, 22 из списка публикаций). В приложении 2 предложено исчисление поиска вывода для классической логики высказываний на базе тернарной связки условной дизъюнкции (по этой теме см. N 6 из списка публикаций).

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

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

—  разработки стратегии и тактики доказательств в логических исчислениях;

—  управления процессом построения вывода при решении задач с помощью ЭВМ;

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

В первом параграфе ("Понятие интеллектуальной системы") на основе анализа понятия логической системы обосновывается необходимость развития "эвристической" компоненты логических систем для задачи поиска (построения) вывода и формулируется задача исследования: как возможно построение вывода в логических системах? Вводится базовое методологическое понятие интеллектуальной (логико-эвристической) системы, и выделяется тип интеллектуальных систем, в которых предусмотрены особые средства для организации процесса построения вывода, — исчисления поиска вывода. Формулируется, что изучение этих исчислений и составляет "предмет" новой научной дисциплины — теории поиска вывода. Введенное понятие логико-эвристической системы сравнивается с другими подходами к определению интеллектуальных систем и показывается его совместимость с подходами И.С. Ладенко, В.М. Сергеева, В.К. Финна.

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

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

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

В первой части параграфа ("Идея глобальной обработки информации в ТПВ") проводится исследование использования идеи глобальной обработки информации в ТПВ. Для этого выделяются два возможных направления реализации идеи глобальной обработки информации. Одно из них связано с дальнейшим анализом структуры вывода, что уже было намечено в рамках логических исчислений типа систем натурального вывода и секвенциальных исчислений. Например, при "глобальной" обработке секвенциального дерева вывода возможно извлечение информации о "расщеплении" некоторой формулы, что позволяет не производить "расщепление" такой же формулы в других ветвях дерева поиска. Во-вторых, возможно и более радикальное использование идеи глобальной обработки информации в виде построения специальных логических исчислений, более полно учитывающих информацию (структуру) испытуемых на выводимость формул, — исчислений поиска вывода. Далее анализируются конкретные системы поиска вывода, в которых идея глобальной обработки информации нашла свою реализацию. Это в основном работы, выполненные в ленинградской (петербургской) школе математической логики Н.А. Шанина: Н. Шанин и др. [9], Г. Давыдов [10], Г. Цейтин [11], П. Суворов [12], Е. Данцин [13].

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

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

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

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

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

Во второй главе ("Обратный метод С.Ю. Маслова") ставится задача построения на базе обратного метода С.Ю. Маслова [14] исчисления поиска вывода — исчисления чисел с индексами с целью моделирования на его основе разных тактик поиска вывода.

Первый параграф ("Общая схема обратного метода") посвящен построению некоторой конкретизации обратного метода для исчисления высказываний. Пусть нам дана формула F в дизъюнктивной нормальной форме: a Ú ~a&b Ú a&~b Ú ~a&~b и секвенциальное исчисление G без структурных правил и с допустимым правилом сечения:

АКСИОМАМИ данного исчисления являются секвенции вида ®  A, X, ~X, B, которые содержат контрарную пару литер.

ПРАВИЛА ВЫВОДА исчисления следующие:

n – кратное                    ® B, A1, C; ® B, A2, C; … ® B, An, C;

правило ® &                     ® B, A1 & A2 & … & An, C

n – кратное                     ® B, A1, A2,       …,        An, C

правило ® Ú                 ® B, A1 Ú A2 Ú … Ú An, C

ВЫВОДОМ формулы F называется дерево, полученное применением правил вывода, в концевых вершинах которого стоят аксиомы, а в корне дерева — формула F.

Построим дерево поиска вывода F, в котором знак “Ú” по правилу ®Ú предварительно заменен на "," ):

                                             Ä                                   Ä

                           ® a, ~a, a&~b, ~b    ® a, b, a&~b, ~b

                                            [4]                             [5]

                                                 \                         /

                                                      \               /

                                                           \      /

              Ä                                              !

® a, ~a&b, a&~b, ~a          ® a, ~a&b, a&~b, ~b

               [2]                                    [3]

                   \                                    /

                         \                        /

                               \           /

                                     !

            ®a, ~a&b, a&~b, ~a&~b

                                   [1]

Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком Ä), т.е. содержат контрарную пару литер: a и ~a — в секвенциях 2 и 4, b и ~b — в секвенции 5. Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции могут быть удалены — "прополоты". Сформулируем алгоритм "прополки" [9], на основании которого преобразуем полученное дерево вывода формулы F. "Избыточными" для 2 секвенции являются формулы a & ~b и ~a & b, для секвенции 4— формула a & ~b и литера ~b, для секвенции 5 — формула a & ~b и литера a. На основании произведенной "прополки" концевых секвенций ветвей "прополем" нижележащие секвенции данной ветви, из которых удаляются литеры и боковые формулы секвенции, не встречающиеся в верхних секвенциях данной ветви. Так как формула a & ~b не встречается в секвенциях 4 — 5 и 2, то она может быть сначала удалена из секвенции 3, и затем, из корневой секвенции 1. "Прополотое" дерево вывода F выглядит так:

                   ® a, ~a                    ® b, ~b

                               \                           /

                                   \                   /

                                         \         /

® a, ~a                ® a, ~a&b, ~b

            \                             /

                \                    /

                      \         /

          ®a, ~a&b, ~a&~b

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

Формула F будет выглядеть так: 1₀  Ú  2₁ & 2₂  Ú  3₁ & 3₂  Ú  4₁ & 4₂. "Прополотое" дерево вывода будет выглядеть так:

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

                   ® 1₀,  2₁                    ® 2₂, 4₂

                               \                           /

                                   \                   /

                                         \         /

® 1₀,  4₁                ® [1₀ 4₂], 2₁ & 2₂

            \                             /

                \                    /

                      \         /

® , 1₀, 2₁ & 2₂, 4₁ & 4₂

Кодировка формул является существенной чертой исчислений на базе обратного метода и позволяет дать такое представление формул исчисления высказываний, в котором выразима дополнительная структурная информация о формуле, а именно: "зацепленность" литер данной формулы (состав контрарных пар).

Введем исчисление чисел с индексами явным образом. Исходное понятие исчисления — понятие набора, который представляет собой множество чисел с индексами. Аксиомами исчисления являются все такие пары чисел с индексами, которые соответствуют контрарным парам литер исходной формулы — исходные благоприятные наборы. Концевые вершины "прополотого" дерева вывода, а также наборы: [2₁ 3₁], [3₁ 4₁], [2₂ 3₂] образуют аксиомы исчисления поиска для формулы F. Единственное правило вывода исчисления позволяет получать новые благоприятные наборы объединением нескольких благоприятных наборов, при котором возможно удаление тех чисел с индексами, которые образуют полную совокупность литер некоторого дизъюнкта. В "прополотом" дереве вывода формулы F вновь полученные благоприятные наборы при движении по дереву "сверху вниз" заключены в квадратные скобки. Например, при применении правила вывода к исходным благоприятным наборам [1₀ 2₁] и [2₂ 4₂] в результате получим новый благоприятный набор [1₀ 4₂], так как числа 2₁ и 2₂ образуют полную совокупность литер второго (2) дизъюнкта F, а из благоприятного набора [1₀ 4₂] получается благоприятный набор [4₂] исключением первого (1) однолитерного дизъюнкта F. Т.е. правило вывода исчисления является "механизмом" перехода по секвенциальному дереву "сверху вниз" от концевых секвенций к корневой секвенции, который позволяет исключать из состава наборов дизъюнкты исходной формулы. Именно с этим изменением направления поиска по сравнению с направлением поиска "снизу вверх" в секвенциальных исчислениях и связано название обратного метода. Получение пустого благоприятного набора  означает построение вывода исчисления. Например, следующая последовательность наборов является выводом исчисления чисел, построенного для исходной формулы F:

1. [1₀ 2₁]                                     4. [1₀ 4₁]

2. [2₂ 4₂]                                     5. [1₀]                из 3, 4

3. [1₀ 4₂]             из 1, 2            6.                        из 5

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

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

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

правило вывода Б исчисления                      правило сечения

      ®  A, X          ®  B, Y                                                  ®  A, C            ®  B, ~C

          ®  A, B, X & Y                                                                      ®  A, B, C & ~C

             ®  A, B (F)                                                                          ®  A, B

Здесь X & Y можно исключить правилу          Здесь C & ~C можно исключить по правилу

вывода исчисления, при условии, что             сечения, так как C& ~C — противоречие и его

X & Y образуют формулы Ф.                             удаление не нарушает выводимости ®  A, B

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

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

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

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

Третья глава ("Интеллектуальный бектрекинг (intelligent backtracking)") посвящена решению проблемы "отхода" (backtracking). В ней ставится задача показать возможности аналитического подхода для решения проблемы "отхода" и обосновать тезис о совместимости существующих в ТПВ методов поиска "в глубину" и "в ширину". Для этого здесь построено исчисление поиска вывода — исчисление "интеллектуального бектрекинга" (на основе системы поиска, предложенной И.В. Ежковой [15]), в котором возможно сочетание этих методов.

В первом параграфе ("Постановка проблемы: <поиск в ширину> и <поиск в глубину>") задается тема исследования, которая определяется противопоставлением существующих в теории поиска вывода двух стратегий поиска — методом "поиска в глубину" и методом "поиска в ширину". Пусть нам дана формула Ф и некоторое множество формул — мир S. Ставится задача найти такую подстановку, которая превратила бы результат подстановки формулы Ф — Ф* — в формулу, выводимую из формул мира S. Если, например, даны формула Ф₁: P(x) & Q(y) & R(z,y) & S(x,a) и некоторый мир S₁:

P(a), P(b),

Q(a), Q(c), Q(d),

R(b,c), R(b,d),

S(b,b),S(b,a),S(b),

то для получения вывода формулы Ф₁* в мире S₁ необходимо, чтобы каждый конъюнктивный член формулы Ф₁* совпадал с некоторой элементарной формулой из S_1.. Эту задачу можно решить, например, составив систему уравнений на термах формулы Ф₁* и мира S₁ и найти пересечение для значений одинаковых переменных формулы. Если это пересечение для каждой переменной формулы Ф₁* не пусто, то система уравнений имеет решение(я).

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

1. x = a, b( для первого конъюнктивного члена формулы )

2. y = b, c, d

3. ( z = b & y = c ), ( z = b & y = d )

4. x = b

Найдем пересечение значений для каждой переменной формулы Ф₁*. Из п.1  и п. 4 видно, что решением для x является одноэлементное множество {b}, из п.3 — решением для z также является {b}. При анализе пп.2 — 3 видно, что решением для y является двухэлементное множество {c, d}. Таким образом, подстановки {x/b, y/c, z/b} и {x/b, y/d, z/b} превращают формулу Ф₁ в формулу Ф₁*, выводимую в мире S₁, т.е. являются искомым решением.

Другим подходом к решению данной задачи, который особенно оправдан при "больших" мирах S, является "поиск в глубину", суть которого заключается в поиске на каждом уровне лишь первого возможного решения, удовлетворяющего условиям задачи. Для данной системы уравнений, на первом уровне будет выбрано значение x = a, на втором — y = b, что приводит к "неудаче" на третьем уровне. Так возникает проблема "отхода", которая связана с тем, что при использовании метода поиска "в глубину" находится лишь первое локальное решение, которое в общем случае может оказаться неверным, и подлежит пересмотру и при дальнейшем поиске.

Во втором параграфе ("Неформальное введение в "интеллектуальный бектрекинг" (intelligent backtracking)") дается общая схема "интеллектуального бектрекинга" (intelligent backtracking), который был предложен для преодоления недостатков тактики "наивного бектрекинга" ("naive backtracking") за счет использования аналитического подхода к построению выводов. Основная идея "интеллектуального бектрекинга" заключается в анализе полученной при "неудачном" означивании информации для выяснения возможных "причин" неудачи с целью их блокирования при следующих попытках означивания. Для пояснения сути работы "интеллектуального бектрекинга" (без учета совпадения предикатных букв и местности предикатов) предлагается конструкция двоичного дерева поиска подстановок (см. рисунок ниже), вершины которого соответствуют означиваемым термам; «левые» ветви — сделанным в процессе поиска подстановкам (подстановки обозначены знаком «/», например x/a); "правые" ветви — запретам на ту или иную подстановку (запрет обозначается с помощью знака «╪», например x ╪ a):

                       X                 

                     /  \                

                x╪a/      \x/a            

               Y /          \ Y          

            y╪d/  \y/d  y╪d/  \y/d       

           Z /      \  Y /      \        

        z╪c/  \z/c  y╪b/  \y/b           

       W /      \    /      \ Z          

    w╪c/  \w/c          z╪c/  \z/c        

   U /      \            /      \ W      

u╪a/  \u/a                  w╪c/  \w/c   

 /      \                  W /      \    

 

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

Представим в виде такого двоичного дерева процесс решения методом "поиска в глубину" предложенного примера. При этом неудачу при означивании будем помечать F (false), после чего происходит "отход" вверх по дереву. Сделанная ранее "неудачная" подстановка, которая вероятно ответственна за невозможность дальнейшего означивания запрещается (появляется соответствующее неравенство, например y╪b при первом "отходе"), т.е. на дереве в соответствующей точке выбирается правое ребро, и поиск подстановок продолжается. Успешное завершение поиска обозначим Tr (true).

                                          

                    P(x) ¬──────────────┐

                   /   \                 │

              x╪a/      \ x/a            │

               /    Q(y) \ ¬─────────┐  │

             /          / \           │  │

      P(x) /      y╪b /    \ y/b      │  │

           \ x/b    /       \         │  │

       Q(y) \     / Q(y)     \ R(z,y) │  │

           /      \           \       │  │

     y╪b /         \ y/c       \      │  │

       /            \            F1───┘  │

Q(y) /               \ R(z,y)            │

     \ y/c            \                  │

      \                \ z/b             │

R(z,y) \                \                │

        \ z/b            \ S(x,a)        │

         \                \              │

   S(x,a) \                F2────────────┘

           \                              

            Tr                            

 

В случае intelligent backtracking при неудаче производится анализ возможной причины неудачи и отход осуществлялся на тот узел дерева, в котором была сделана неверная подстановка. В нашем примере таких отходов было два. В первом случае, intelligent backtracking не отличается от стандартного, так как отход производится на ближайшую точку ветвления. Но во-втором случае, анализ неудачи показывает, что необходимо вернуться в первый узел дерева поиска (означивание переменной x) и запретить подстановку x/a. При этом, полезную информацию о запрете подстановки y/b, полученную при первом "бектрекинге" также можно сохранить и использовать для дальнейшего поиска вывода.

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

В первой части параграфа задается логическая система L в этом обогащенном языке исчисления предикатов. Наиболее существенным является определение правильно построенной формулы L и связанные с ним понятия непротиворечивой тройки и совместимости троек. п. п. ф. L представляет собой выражение вида (Г С К) [О], где:

С — является п. п. ф. исчисления предикатов,

Г (К) — система неравенств (равенств) (Г, К — возможно пустые),

О — подстановка, применяемая к цепочке (Г С К).

Для того чтобы выражение (Г С К) [О] являлось п. п. ф. системы L необходимо выполнение следующих условий:

1. Г должно быть непротиворечиво, т.е. не должно содержать противоречивых неравенств типа х ╪ х.

2. Г и К должны быть совместимы, т.е. если х ╪ a Î Г, то х ╪ a Î К и наоборот.

3. О должна быть совместима с Г, т.е. результат конкретизации Г посредством О не должен содержать противоречивых неравенств типа х ╪ a (конкретизация Г посредством О непротиворечива).

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

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

Тройка Г_iК_iО_i совместима с непротиворечивой тройкой Г_jК_jО_j, если и только если тройка (Г_i Г_j) (К_i К_j) (О_i О_j) непротиворечива, где цепочки Г_i Г_j  (К_i К_j, О_i О_j) — результат композиции неравенств Г_i и Г_j (равенств К_i К_j , подстановок О_i О_j).

Правила вывода L являются обобщением обычных правил вывода исчисления предикатов. Например, правило подстановки формулируется так:

       Ф               (обобщенное правило подстановки)

(Г_i Ф К_i )[О_i]

Понятие вывода в системе L стандартное.

Во второй части параграфа формулируется собственно исчисление поиска интеллектуального бектрекинга, в котором используется основная идея метода метапеременных — не большая, чем это необходимо, уточненность значений термов при подстановке (понятие положительного сопоставления формул является аналогом понятия наиболее общего унификатора в методе резолюций). Определяются правила поиска исчисления и понятие дерева поиска вывода. Формулируется общая стратегия поиска подстановок методом в "глубину", которая сводится к нахождению таких троек Г₁К₂О₃ ,..., Г_n К_nО_n, каждая из которых непротиворечива и совместима с предыдущими непротиворечивыми тройками. При завершении процесса поиска выдается результирующая тройка (Г₁ ... Г_n) (К₁ ... К_n) (О₁ ... О_n). Тактика интеллектуального бектрекинга определяет механизм взаимной "перекачки" термов из множества "равенств" в множество "неравенств" при неудачах. Это наглядно представлено на предложенной ранее конструкции двоичного дерева, правые ветви которого соответствуют системе неравенств, а левые — системе равенств. Если в процессе означивания термов появляется сигнал неудачи, то в систему неравенств (равенств) записывается новое неравенство (равенство), полученное в результате анализа возможных "причин неудачи", и процесс поиска продолжается с учетом накопленного "отрицательного" опыта.

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

В заключении главы сформулированное исчисление сравнивается с другими подобными системами, обсуждается вопрос эффективности предложенных систем, а также устанавливается взаимосвязь предложенного метода "интеллектуального бектрекинга" с результатами модификации языка "ПРОЛОГ" (за счет использования операторов "cut", "savecp", "cutto", "get backtracking") и с реализацией идеи "заморозки" вычислений (freeze operation) или "ленивых вычислений" (lazy evalution). На основе проведенного анализа выявляются перспективы дальнейшего развития метода "интеллектуального бектрекинга", а также формулируется тезис о том, что предложенное исчисление поиска возможно использовать как универсальную систему поиска, на базе которой возможно сочетание методов поиска "в глубину" и "в ширину".

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

В приложении 2 ставится задача построения исчисления поиска вывода с тернарной логической связкой условной дизъюнкции. Связка условной дизъюнкции, введенная А. Черчем [16], обозначается [A, B, C], где A, B, C — пропозициональные формулы. Это запись понимается так: если значение формулы B истинно, то значение формулы [A, B, C] совпадает со значением формулы A, в противном случае, т.е. если значение B ложно, значение [A, B, C] совпадает со значением формулы C. Другие пропозициональные связки конъюнкции, дизъюнкции, импликации, отрицания определяются следующим образом:

A & B   =   [A, B, f]

A Ú B   =   [t, A, B]

A É B   =   [B, A, t]

Ø A       =   [f, A, t]

Связка условной дизъюнкции и константы t и f образуют полную систему связок, что позволяет построить пропозициональное исчисление S [17]. Аксиомами исчисления является стандартный набор аксиом пропозиционального исчисления, записанных в языке исчисления S. Например, аксиома A5 [17] (соответствующая закону утверждения консеквента p É (q É p) выглядит так: [[p, q, t], p, t]. Правилами вывода являются правило подстановки (в стандартной формулировке) и аналог правила modus ponens: из [A, B, C] и B следует A.

Формулы (подформулы) пропозиционального исчисления представляют собой совокупность вложенных друг в друга троек. Всю формулу будем называть конечной тройкой. Формулу (переменную), стоящую в середине тройки, будем называть базовой формулой (переменной) тройки, другие формулы (переменные или константы) тройки — боковыми формулами тройки (соответственно левой и правой боковой формулой тройки). Например, для формулы [[p, q, t], p, t] переменная q является базовой для тройки pqt, а переменная p — для конечной тройки [pqt], p, t. Переменная p и константа t являются боковыми для тройки pqt. Формулу исчисления [pqt, p, t] представима в виде (графического) дерева троек:

 P          t

    \       /

Q         t

   \       /

      P

Здесь переменным P и Q сопоставлены вершины дерева, а переменной p и константе t — концевые вершины.

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

Аксиомами исчисления являются концевые вершины с константой t.

Очевидно, что если все концевые вершины дерева являются аксиомами, то формула исходного исчисления, которой сопоставлено данное дерево троек, является тавтологией. Но условия, при которых дерево троек соответствует тавтологии можно ослабить, так как не обязательно требовать наличия среди всех концевых вершин константы t (например, приведенные выше деревья тавтологичных формул содержат среди концевых вершин константу f). Поэтому вводится следующее правило обхода деревьев — правило вывода исчисления, — которое определяется смыслом связки условной дизъюнкции (а именно: если дано поддерево, соответствующее формуле [A, B, C] и известна "направленность" формулы B, то, если B "истинно", т.е. направлено "вправо" — следует A, а в случае противоположной "направленности" B (B — "ложно", т.е. направлено "влево") — следует C.):

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

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

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

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

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

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

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

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

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

Публикации по теме диссертации:

(с учетом последующих публикаций)

1.        Катречко С.Л. Модификация обратного метода С.Ю. Маслова //Материалы Х Всесоюзной конференции по логике, методологии и философии науки. — Минск, 1990. С.13 - 14.

2.        Katretchko S. Frege's system and proof-search theory //Abstacts of Russian conference «Frege's and Hilbert's heritage in the XX-th centure: logic, philosophy and mathematics». Kaliningrad, 1992. p. 11.

3.        Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова (обобщенная онлайновая версия в формате Word с учетом [8]) //Логические методы в компьютерных науках. М., ИФ РАН. 1992. С.125 - 141.

4.         Катречко С.Л. Введение в логику (программа курса). — М., МГУ. 1993.

5.        Катречко С.Л. От логических исчислений к интеллектуальным системам: введение в теорию поиска вывода (программа курса). — М., МГУ. 1994.

6.        Катречко С.Л. Исчисления поиска вывода с «условной дизъюнкцией» //Материалы XI Международной конференции "Логика, методология, философия науки, Москва - Обнинск. 1995. Т.2.

7.        Катречко С.Л. Логика и теория поиска вывода //Наука и философия на рубеже тысячелетий: перспективы и горизонты (тезисы док. и выс. Всерос. научн. конф.). Курск, 1995.

8.        Катречко С.Л. Обратный метод С.Ю. Маслова (обобщенная онлайновая версия в формате Word с учетом [3]) //Логика и компьютер 2: логические языки, содержательные рассуждения и методы поиска доказательства. — М., Наука. 1995.

9.         Катречко С.Л. Интеллектуальный бектрекинг //Логические исследования, вып.3. — М., Наука. 1995.

10.    Катречко С.Л. Искусственный интеллект versus моделирование сознания //Статья подготовлена на основании доклада 20.05.96 на семинаре "Искусственный и естественный интеллект" факультета информатики РГГУ

11.    Катречко С.Л. (в соавт.) Использование интеллектуальных систем при принятии решений //Проблемы управления в контексте гуманитарной культуры. — М., «Университетский гуманитарный лицей», 1997.

12.    Katretchko S. Between logic and computer heuristic //Proceedings ICI & C’ 97, June 9 - 13

13.    Катречко С.Л. Бесконечность и теория поиска вывода //Бесконечность в математике: философские и исторические аспекты. — М., «Янус-К», 1997.

14.    Царьков Д.В., Катречко С.Л. Об одном алгоритме приведения пропозициональных формул к д. ф. н. //Международная конференция «Смирновские чтения». — М., 1997.

15.    Катречко С.Л. Обратный метод С.Ю.Маслова и моделирование сознания //Международная конференция (1-ые) «Смирновские чтения». — М., 1997.

16.    Катречко С.Л. От логики к теории поиска вывода //Международная конференция «Развитие логики в России: итоги и перспективы». Тезисы докладов и сообщений. — М.: «Логос», 1997

17.    Катречко С.Л. К методологии построения интеллектуальных систем //Логическое кантоведение - 4: Тезисы докладов Международного семинара. — Калининград, 1997.

18.    Катречко С.Л. Интеллектуальные системы на базе обратного метода С.Ю. Маслова //Человек — Философия — Гуманизм: Тезисы докладов и выступлений 1 Российского философского конгресса (4 — 7 июня 1997); секция «логика и философская логика».

19.    Katretchko S. Between Logic and Heuristic //Proceedings 20th World Congress of Philosophy August, 1998.

20.    Катречко С.Л. От логических исчислений к интеллектуальным системам (на базе обратного метода С. Маслова) //Итоговый отчет по гранту РГНФ (10 декабря 1997).

21.    Катречко С.Л. От логики к теории поиска вывода //2–е «Смирновские чтения», Международная конференция. — М., Изд-во ИФ РАН, 1999.

22.    Katretchko S. From logic to proof-search theory //Proceedings XI LMPS’ 99. — Cracow, 1999.

ПРИМЕЧАНИЕ:

<**> — диссертация выполнена в секторе логике Института философии РАН и защищена на заседании специализированного Ученого совета Д. 002. 29-03 Института философии РАН 12 ноября 1992. Научный руководитель — доктор философских наук, профессор Смирнов В.А., оппоненты — д. филос. н. Бочаров В.А., к. филос. н. Шалак В.И.

ЦИТИРУЕМАЯ ЛИТЕРАТУРА:

1. Воронков А.А., Дегтярев А.Н. Автоматическое доказательство теорем //Кибернетика. 1986, N 3; 1987, N 4

2. Пушкин В.Н. Эвристика — наука о творческом мышлении. — М., 1967.

3. Брюшинкин В.Н. Логика, мышление, информация. — Л. (СПб)., 1988.

4. Cook S.A., Rechow R.A. The relative efficency of propositional proof systems. //Journal of symbolic logic. 1979. Vol.44, N.1

5.  Данцин Е.Я. Алгоритмика задач выполнимости //Вопросы кибернетики. 1987. Вып.131. С.7 - 30.

6.  Серебрянников О.Ф. Эвристические принципы и логические исчисления. — Л СПб).,1970.

7. Смирнов В.А. Формальный вывод и логические исчисления. — М., 1972.

8. Маслов С.Ю. Теория дедуктивных систем и ее применения.— М.: Радио и связь, 1986.

9. Шанин Н.А. и др. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. М- Л., 1965.

10. Давыдов Г.В. Синтез метода резолюций и обратного метода //Записки научных семинаров ЛОМИ АН СССР. 1971.Т.20.

11.Цейтин Г.С. О сложности вывода в исчислении высказываний //Записки научных семинаров ЛОМИ АН СССР. 1968. Т.8.

12. Суворов П.Ю. О распознавании тавтологичности пропозициональных формул //Записки научных семинаров ЛОМИ АН СССР. 1976. Т.60.

13. Данцин Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки семинаров ЛОМИ АН СССР. 1981. Т.105.

14.  Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР. 1968. Т.98.

15. Ежкова И.В. Автоматическое доказательство теорем и построение планов //Алгоритмы и программы. 1978. N 4.

16. Черч А. Введение в математическую логику. — М.: ИЛ., 1960.

17. Сидоренко Е.А. Пропозициональное исчисление с условной дизъюнкцией //Методы логического анализа. — М.: Наука, 1977.