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 рода не применяется.