Для любого исчисления B любой метод поиска в нем может быть представлен как способ построения по каждому испытуемому на выводимость объекту S специального метаисчисления над B и S — исчисления поиска B S, — выводимость в котором объекта Д эквивалентна выводимости S в исходном исчислении B.

ЛИТЕРАТУРА:

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

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

3. Katrechko S.L. 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.

4. Катречко С.Л. Логический анализ интеллектуальных систем с метапроцедурами //Автореферат диссертации ... к. филос. н. — М., ИФ РАН, 1992.

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

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

ЛОГИКА И ТЕОРИЯ ПОИСКА ВЫВОДА

При исследовании процесса решения задач можно выделить две задачи. С одной стороны, необходимо выявить правильные (надежные) способы рассуждений. Этой задачей, которую можно сформулировать в виде вопроса "что есть правильное рассуждение (вывод)?", занимается логика. Для ответа на этот вопрос логика опирается на понятие логической формы, для "работы" с которой в логике используются синтаксические процедуры построения логических исчислений, которые при истинности посылок гарантируют истинность заключений. Именно на этом свойстве "сохранения истинности" основывается критерий правильности (надежности) рассуждений. Но при этом логика отвлекается от реального процесса построения вывода, от вопросов о методах поиска вывода, о соотношении разных методов по их "мощности", о конструировании или выборе наиболее эффективных средств построения вывода. Для логических систем достаточно процедур полного перебора, например алгоритма Британского музея.

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

Областью пересечений этих двух подходов является теория поиска вывода (ТПВ), которая исследует возможные способы решения задач (т.е. как строить вывод) в каком-либо исчислении. Более точно проблематику ТПВ можно определить так: "выявление по исчислению и объекту в языке этого исчисления структуры возможных выводов этого объекта, причем выводов интересных в каком - либо отношении" [1].

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

Поясним вышесказанное на примере установления общезначимости формулы F:

((p1 & ... & pn) Й Q) Й ((ШQ Й Ш (p1 & ... & pn)).

Во-первых, можно воспользоваться методом истинностных таблиц, т.е. осуществить полный перебор всех возможных сочетаний истинностных значений переменных p1, ..., pn, Q, входящих в F. Это метод полного перебора.

Во-вторых, перебор можно существенно сократить на основе использования смысла связки «Й», например методом семантических таблиц. В этом случае, первоначально предполагается ложность формулы F. Последующий анализ связки «Й» показывает, что это может иметь место, только если антецедент формулы F — «P Й Q») (здесь P обозначает p1 & ... & pn) истинен, а консеквент F — «ШQ Й Ш (p1 & ... & pn)» — ложен; и т.д. Дальнейший анализ формулы показывает невозможность предположения о ложности F и делается заключение об общезначимости исходной формулы. (Заметим, что в данном случае нет необходимости анализировать структуру подформулы P = p1 & ... & pn, так как достаточно анализа "внешней структуры формулы F: ((P Й Q) Й (ШQ Й ШP)) (Аналогом этого подхода является использование производного правила контрапозиции, в силу которого данная формула общезначима, так как формула имеет вид ((A Й B) Й (ШB Й ШA)).

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