С.Л. Катречко
Исчисление поиска вывода с "условной дизъюнкцией"
Здесь ставится задача построения исчисления поиска вывода с тернарной логической связкой условной дизъюнкции <см. примечание **>. Связка условной дизъюнкции, введенная А. Черчем в [1], обозначается [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 = [f, A, t]
Связка условной дизъюнкции и константы t и f образуют полную систему связок, что позволяет построить пропозициональное исчисление S [2]. Аксиомами исчисления является стандартный набор аксиом пропозиционального исчисления, записанных в языке исчисления S. Например, аксиома A5 [2] (соответствующая закону утверждения консеквента p É (q É p) выглядит так: [[p, q, t], p, t]. Правилами вывода являются правило подстановки (в стандартной формулировке) и аналог правила modus ponens: из [A, B, C] и B следует A.
На основании смысла связки условной дизъюнкции можно сформулировать
другие производные правила. Например, очевидно, что из [A, B, C] и ØB следует C, поэтому производным правилом исчисления является
следующее правило вывода: из [A, B, C] и [f, B, t] следует C.
К таким правилам можно отнести и следующие тривиальные эквивалентности:
1.
[t, A, f], [A, B, A], [A, t, B], [B, f, A] — эквивалентны формуле A.
2.
[t, A, t], [A, f, t], [t, t, A] — эквивалентны константе t.
3.
[f, A, f], [f, f, A], [A, f, f] — эквивалентны константе f.
Формулы (подформулы) пропозиционального
исчисления представляют собой совокупность вложенных друг в друга троек. Всю
формулу будем называть конечной тройкой. Формулу (переменную), стоящую в
середине тройки, будем называть базовой формулой (переменной) тройки, другие
формулы (переменные или константы) тройки — боковыми формулами тройки
(соответственно левой и правой боковой формулой тройки). Например, для формулы [[p,
q, t], p, t] переменная q является базовой для тройки pqt, а
переменная p — для конечной тройки [pqt], p, t. Переменная p
и константа t являются боковыми для тройки pqt.
Для формулировки исчисления поиска
воспользуемся алгоритмом приведения к минимальной нормальной форме [2], который
соответствует известному в теории поиска вывода правилу (методу) расщеплений
[6]. В основе этого алгоритма лежит следующее преобразование формул: формула B
эквивалентна формуле [A, b1, C], где A (C) есть результат
подстановки t (f) вместо переменной b1 из B.
Справедливость этого утверждения следует из того, что значение формул A (C)
и B совпадают при приписывании значения "истина"
("ложь") переменной b1. Это позволяет последовательно
исключить все переменные из боковых формул, заменяя их на константы t и f.
В результате такого преобразования исходной формулы (последовательное
"расщепление" формулы с заменой некоторой ее переменной на константы t
и f) получаем формулу B в совершенной нормальной форме (если при
этом упрощать получаемые формулы используя сформулированные выше
эквивалентности, то получим минимальную нормальную форму B).
Введем исчисление поиска (исчисление
троек), где процедура расщепления реализована графически. Для этого
сопоставим каждой формуле исчисления дерево троек следующим образом. Каждой
базовой переменной сопоставляется некоторая вершина дерева троек, а базовой переменной
конечной тройки — корень дерева. Боковые формулы троек располагаются как
соответственно левый и правый верхние индексы каждой вершины дерева. Боковым
формулам, не являющимся вершинами дерева, сопоставляются концевые вершины.
Представим формулу [pqt, p, t] в виде (графического) дерева троек:
P t
\ /
\ /
P
Здесь переменным P и Q
сопоставлены вершины дерева, а переменной p и константе t -
концевые вершины.
Путем в дереве троек называется такая последовательность
вершин дерева, которая начинается с корня дерева и заканчивается некоторой
концевой вершиной. Путь представляет собой упорядоченное множество вершин. Подпутем будем называть некоторое
упорядоченное подмножество вершин пути. Для более сложных формул, например для [p,
[f, fpt, t], t], которая соответствует формуле p É
ØØp, дерево троек выглядит так:
t f
____________________________________
____________________________________
Ø P
(здесь наклонные черточки отсутствуют, так как расположение знаков (слева и справа) позволяет однозначно их восстановить.)
Множество вершин дерева, заключенных между двумя горизонтальными чертами, назовем уровнем дерева троек. Нумерация уровней начинается с корня дерева, которому присвоен нулевой уровень. Понятие пути изменится следующим образом: путем в дереве назовем последовательность вершин по одной из каждого уровня дерева троек.
На основе исходного исчисления с условной дизъюнкцией сформулируем исчисление поиска на деревьях троек (данное исчисление строится аналогично исчислениям обратного метода С. Маслова [5].
Основой исчисления являются деревья троек,
сопоставленные формулам исчисления с условной дизъюнкцией. Из этого следует,
что каждой вершине дерева сопоставлены либо переменная, либо константа
некоторой формулы исходного исчисления.
Аксиомами исчисления являются концевые вершины с константой t.
Очевидно, что если все концевые вершины дерева являются аксиомами, то
формула исходного исчисления, которой сопоставлено данное дерево троек,
является тавтологией. Но условия, при которых дерево троек соответствует
тавтологии можно ослабить, так как не обязательно требовать наличия среди всех
концевых вершин константы t (например, приведенные выше деревья
тавтологичных формул содержат среди концевых вершин константу f).
Поэтому вводится следующее правило обхода деревьев — правило вывода исчисления, — которое определяется смыслом
связки условной дизъюнкции, а именно: если дано поддерево, соответствующее
формуле [A, B, C] и известна "направленность" формулы B,
то, если B "истинно", т.е. направлено "вправо" —
следует A, а в случае противоположной "направленности" B
(B — "ложно", т.е. направлено "влево") — следует C.
После вершины t
(f) выделенным направлением обхода является направление влево (вправо).
После вершины, сопоставленной некоторой переменной возможно либо левое, либо
правое направление движения по дереву (эти направления называется
противоположными направлениями). Если при движении по дереву после переменной,
было выбрано направление вправо (влево), то это направление обхода является
выделенным по этой переменной для любого пути, содержащего эту вершину (для
отрицания переменной выделяется противоположное направление). Путь с выделенным
направлением обхода для каждой вершины называется выделенным путем.
Понятие вывода
исчисления, соответствующее тавтологичности исходных формул исчисления
высказываний, формулируется так:
Выводом называется дерево, у которого любой
выделенный путь закрыт, т.е. оканчивается аксиомой. Такие деревья будем
называть закрытыми деревьями.
Очевидно, что
закрытые деревья сопоставлены формулам исходного исчисления, которые являются
тавтологиями. Например, приведенное выше дерево троек для формулы [pqt, p,
t] является выводом исчисления, так как любой путь от корня к концевым
литерам этого дерева закрыт (отметим, что после верхней литеры p нельзя
выбрать путь вправо к константе f, так как ранее, от корня дерева, было
выбрано направление обхода дерева после литеры p влево, а направление
обхода после корневой литеры p вправо оканчивалось константой t).
Поэтому задачей исчисления поиска является проверка закрытости путей дерева
троек.
Правило вывода позволяет сформулировать следующий алгоритм поиска
вывода, который является аналогом метода расщепления:
Если после выбора выделенного направления по некоторой переменной дерево троек закрыто, то для доказательства тавтологичности формулы достаточно проверить закрытость дерева троек с противоположным выделенным направлением по этой переменной.
Рассмотрим "доказательство"
тавтологичности формулы p É ØØ p. Пусть дано следующее дерево троек:
t f
____________________________________
____________________________________
Ø P
Если мы от корня дерева (на нулевом уровне) выбираем направление влево по ØØ p, то после константы f путь закрыт, поэтому проверяем выделенное направление по ØØ p "вправо" (соответственно для p выделенным направлением является направление "влево"). Так как этот путь также закрыт, то дерево закрыто — формула p É ØØp тавтологична (в данном случае была использована тактика поиска "снизу вверх", однако возможно использование и других тактик поиска).
Укажем
также на тесную связь предложенного исчисления с использованием в
программировании оператора условного перехода "если, то...,
иначе...", учет которой может предложить ряд других модификаций
предложенного исчисления поиска.
ПРИМЕЧАНИЕ:
<**> — исчисления поиска вывода относятся к особому классу логических систем, называемых логико-эвристическими системами, в которых помимо "логической" компоненты можно выделить и "эвристическую" компоненту [3, 4]. Для более четкого разделения "логической" и "эвристической" компоненты логических систем возможен следующий подход, предложенный в [5]. Для любого исчисления 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.