I. Построение дерева редукций

1. Начальную секвенцию приписываем к кореню дерева:

v • → F

2. Шаг построения дерева редукций («раскрытие» вершины).

Пусть v – «самая верхняя» вершина дерева редукций, и ей приписана секвенция .

Рассмотрим возможные случаи:

1) секвенция содержит формулу вида A&B справа. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

v

•

2) секвенция содержит формулу вида A&B слева. Тогда применяем редукцию 1 рода вида:

u •

v •

3) секвенция содержит формулу вида A V B слева. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

v

•

4) секвенция содержит формулу вида A V B справа. Тогда применяем редукцию 1 рода вида:

u •

v •

5) секвенция содержит формулу вида A B слева. Тогда применяем редукцию 1 рода вида:

• •

u₁ u₂

v

•

Заметим, что к формулам, помеченным ^*, редукция 1 рода не применяется.