Например, для формулы [[p, q, t], p, t] переменная q является базовой для тройки pqt, а переменная p — для конечной тройки [pqt], p, t. Переменная p и константа t являются боковыми для тройки pqt. Формулу исчисления [pqt, p, t] представима в виде (графического) дерева троек:

P t

\ /

Q t
\ /

P

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

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

Аксиомами исчисления являются концевые вершины с константой t.

Очевидно, что если все концевые вершины дерева являются аксиомами, то формула исходного исчисления, которой сопоставлено данное дерево троек, является тавтологией. Но условия, при которых дерево троек соответствует тавтологии можно ослабить, так как не обязательно требовать наличия среди всех концевых вершин константы t (например, приведенные выше деревья тавтологичных формул содержат среди концевых вершин константу f). Поэтому вводится следующее правило обхода деревьев — правило вывода исчисления, — которое определяется смыслом связки условной дизъюнкции (а именно: если дано поддерево, соответствующее формуле [A, B, C] и известна "направленность" формулы B, то, если B "истинно", т.е. направлено "вправо" — следует A, а в случае противоположной "направленности" B (B — "ложно", т.е. направлено "влево") — следует C.):

После вершины t (f) выделенным направлением обхода является направление влево (вправо). После вершины, сопоставленной некоторой переменной возможно либо левое, либо правое направление движения по дереву (эти направления называется противоположными направлениями). Если при движении по дереву после переменной, было выбрано направление вправо (влево), то это направление обхода является выделенным по этой переменной для любого пути, содержащего эту вершину (для отрицания переменной выделяется противоположное направление). Путь с выделенным направлением обхода для каждой вершины называется выделенным путем.

(Путем в дереве троек называется такая последовательность вершин дерева, которая начинается с корня дерева и заканчивается некоторой концевой вершиной. Путь представляет собой упорядоченное множество вершин. Подпутем будем называть некоторое упорядоченное подмножество вершин пути.)

Понятие вывода исчисления, соответствующее тавтологичности исходных формул исчисления высказываний, формулируется так:

Выводом называется дерево, у которого любой выделенный путь закрыт, т.е. оканчивается аксиомой. Такие деревья будем называть закрытыми деревьями.

Очевидно, что закрытые деревья сопоставлены формулам исходного исчисления, которые являются тавтологиями. Например, приведенное выше дерево троек для формулы [pqt, p, t] является выводом исчисления, так как любой путь от корня к концевым литерам этого дерева закрыт (отметим, что после верхней литеры p нельзя выбрать путь вправо к константе f, так как ранее, от корня дерева, было выбрано направление обхода дерева после литеры p влево, а направление обхода после корневой литеры p вправо оканчивалось константой t). Поэтому задачей исчисления поиска является проверка закрытости путей дерева троек.

Правило вывода позволяет сформулировать следующий алгоритм поиска вывода, который является аналогом метода расщепления:

Если после выбора выделенного направления по некоторой переменной дерево троек закрыто, то для доказательства тавтологичности формулы достаточно проверить закрытость дерева троек с противоположным выделенным направлением по этой переменной.

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

В заключении диссертации кратко суммируются основные результаты работы и намечаются дальнейшие перспективы развития теории поиска вывода и автоматического доказательства теорем.

Публикации по теме диссертации:

(с учетом последующих публикаций)

1. Катречко С.Л. Модификация обратного метода С.Ю. Маслова //Материалы Х Всесоюзной конференции по логике, методологии и философии науки. — Минск, 1990. С.13 - 14.

2. Katretchko S. 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. p. 11.

3. Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова (обобщенная онлайновая версия в формате Word с учетом [8]) //Логические методы в компьютерных науках.