В.А. Стеклова АН СССР. 1968. Т.98.

15. Ежкова И.В. Автоматическое доказательство теорем и построение планов //Алгоритмы и программы. 1978. N 4.

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

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

Исчисление поиска вывода с "условной дизъюнкцией"

Здесь ставится задача построения исчисления поиска вывода с тернарной логической связкой условной дизъюнкции . Связка условной дизъюнкции, введенная А. Черчем в [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 Й B = [B, A, t]
Ш 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

\ /

Q t
\ /

P

Здесь переменным P и Q сопоставлены вершины дерева, а переменной p и константе t - концевые вершины.

Путем в дереве троек называется такая последовательность вершин дерева, которая начинается с корня дерева и заканчивается некоторой концевой вершиной. Путь представляет собой упорядоченное множество вершин. Подпутем будем называть некоторое упорядоченное подмножество вершин пути. Для более сложных формул, например для [p, [f, fpt, t], t], которая соответствует формуле p Й ШШp, дерево троек выглядит так:

t f

P t
____________________________________

f t
____________________________________

Ш P

(здесь наклонные черточки отсутствуют, так как расположение знаков (слева и справа) позволяет однозначно их восстановить.