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

® A, X ® B, Y ® A, C ® B, ШC

___________________ ______________________



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

__________________ _____________________



® A, B (F) ® A, B

правило Б обратного метода правило резолюций

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

ЛИТЕРАТУРА:

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

Фрегевские системы и теория поиска вывода

Логика исследует, прежде всего, "ЧТО ЕСТЬ ВЫВОД?", отвлекаясь от вопроса "КАК СТРОИТЬ ВЫВОД?". Логические системы при истинности посылок гарантируют истинность заключений. Одной из первой такая логическая система была построена Г. Фреге в 1879 г. [1]. Позднее на основе этой системы появились системы ГИЛЬБЕРТОВСКОГО ТИПА.

Возникновение теории поиска вывода связано с появлением более "эвристичных" систем НАТУРАЛЬНОГО ВЫВОДА и СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЙ [2], в которых возможно построение вывода аналитическим методом "сведения задачи к подзадачам". Это предполагает изменение понятия вывода, в котором существенную роль начинают играть структурные свойства. Вместо понятия вывода как некоторой последовательности формул в гильбертовских исчислениях, в натуральных исчислениях вводится понятие субординатного вывода, а в секвенциальных исчислениях — понятие дерева вывода. Использование аналитических процедур позволило "механизировать" процесс построения вывода в системах автоматического доказательства теорем, однако в теории сложности выявились принципиальные ограничения чисто аналитических процедур поиска вывода [3]. Более того, была доказана взаимной моделируемости выводов в гильбертовских, натуральных и секвенциальных системах [4].

Это заставляет вернуться к гильбертовским исчислениям и использовать возможности мощного СИНТЕТИЧЕСКОГО правила ПОДСТАНОВКИ. Но не более ли целесообразно возвращение к фрегевским системам, так как здесь возможно использование не только правила подстановки, но и "пространственное" (структурное) представление вывода в этих системах?

ЛИТЕРАТУРА:

1. G. Frege Begriffsschrift und andere Aufsatze. Zweite Auflage, Darmstadt, 1971

2. Г. Генцен Исследование логических выводов //Математическая теория логического вывода (ред. А. Идельсона, Г. Минца). — Москва, 1967

3. Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. — Москва, 1982 (M.R. Garey, D.S. Johnson "Computers and intractiility: a guide to the theory of NP - completness", 1979)

4. S.A. Cook, R.A. Rechow The relative efficency of propositional proof systems // The journal of simbolic logic, V. 44, n.1, p.36 - 50, 1979
С.Л. Катречко

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

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

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
Актуальность темы

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