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

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

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

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

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

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

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

— для решения проблемы "отхода" (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 из списка публикаций).

ОСНОВНОЕ СОДЕРЖАНИЕ ДИССЕРТАЦИИ
Во введении обосновывается актуальность избранной темы.