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

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

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

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

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

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

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

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

((p₁ & ... & p_n) É Q) É ((ØQ É Ø (p₁ & ... & p_n)).

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

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

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

Продемонстрируем этот подход. Для этого представим формулу дизъюнктивной нормальной формой: (P &ØQ) Ú Q Ú ØP. Для установления общезначимости F необходимо использовать не только информацию о составе и количестве дизъюнктов, но и дополнительную информацию о составе контрарных пар литер данной формулы. Если представить данную формулу диаграммой (см. ниже), то сам “вид” диаграммы — как показано в [2] — указывает на общезначимость F.

\ /

----- p ---------- ØQ -----

| | ДИАГРАММА F

| |

----- Øp ------------ Q ------

/ \

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

1. метод глобальной обработки информации

2. метод временных переменных (метод метапеременных)

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

Примерами построения таких исчислений поиска вывода являются: исчисление чисел с индексами [3], в котором на базе обратного метода С.Ю.Маслова возможно моделирование известных в ТПВ методов резолюции и расщепления; исчисление "интеллектуального бектрекинга" [4], в котором предложен новый алгоритм унификации, сочетающий идеи методов поиска "в глубину" и "в ширину"; "исчисление поиска вывода с условной дизъюнкцией" [5], позволяющее реализовать различные варианты метода расщепления.

ЛИТЕРАТУРА:

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

2. Давыдов Г.В. Синтез метода резолюций и обратного метода //Записки научных семинаров ЛОМИ, 1971. — Т.20. — С.24 - 35.

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

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

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