double arrow

Редукции 1 рода применяем до тех пор, пока можно.

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

Пусть v – одна из таких вершин.

а) если секвенция, приписанная v, содержит одинаковую переменную и слева и справа, то v больше не раскрывается и помечается значком «+».

б) иначе если в секвенции, приписанной v, k=0, то v больше не раскрывается и помечается значком «-».

в) иначе если секвенция, приписанная v, уже приписана некоторой вершине w, располагающейся в дереве редукций ниже v, то v больше не раскрывается и помечается значком <-, w>.

г) иначе к вершине v применяется редукция 2 рода следующего вида:

… …. …

и т.д.

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


Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:  



Сейчас читают про: